Entropy Smoothing #
This file defines the entropy-smoothing distinguishing game used by hashed ElGamal-style
constructions: the adversary distinguishes a real hash output hash hk (z • g) from an
independent uniform element of the output space.
def
EntropySmoothing.realExp
(F : Type)
[Field F]
[SampleableType F]
{G : Type}
[AddCommGroup G]
[Module F G]
{HK : Type}
[SampleableType HK]
{M : Type}
(g : G)
(hash : HK → G → M)
(adversary : HK × M → ProbComp Bool)
:
Real entropy-smoothing experiment. The adversary sees (hk, hash hk (z • g))
for uniform hk and z, and tries to distinguish this from the ideal experiment.
Instances For
def
EntropySmoothing.idealExp
{HK : Type}
[SampleableType HK]
{M : Type}
[SampleableType M]
(adversary : HK × M → ProbComp Bool)
:
Ideal entropy-smoothing experiment. The adversary sees (hk, h) for independent
uniform hk and uniform h : M.
Instances For
noncomputable def
EntropySmoothing.advantage
(F : Type)
[Field F]
[SampleableType F]
{G : Type}
[AddCommGroup G]
[Module F G]
{HK : Type}
[SampleableType HK]
{M : Type}
[SampleableType M]
(g : G)
(hash : HK → G → M)
(adversary : HK × M → ProbComp Bool)
:
Entropy-smoothing distinguishing advantage.