Pseudorandom generators: games and concrete security

Attack Game 3.1 of [BS23] compares a deterministic generator applied to a uniform seed with a uniform output. Adversaries are randomized Boolean tests. Security is relative to a caller-supplied predicate Admissible, with an explicit advantage bound. No computational model or efficiency assumption is built into the generator or the tests.

Generator.IsExpanding records the cardinality condition separately from security. In particular, a generator need not expand, and an expanding generator need not be secure.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 3.1.

structure Cslib.Crypto.PRG.Generator (Seed : Type u_1) (Output : Type u_2) : Type (max u_1 u_2)

A deterministic generator with seed space Seed and output space Output. Efficiency, expansion, and security are separate properties.

• toFun : Seed → Output

  Generate an output from a seed.

theorem Cslib.Crypto.PRG.Generator.ext {Seed : Type u_1} {Output : Type u_2} {x y : Generator Seed Output} (toFun : x.toFun = y.toFun) : x = y

theorem Cslib.Crypto.PRG.Generator.ext_iff {Seed : Type u_1} {Output : Type u_2} {x y : Generator Seed Output} : x = y ↔ x.toFun = y.toFun

@[reducible, inline]

abbrev Cslib.Crypto.PRG.Adversary (Output : Type u_1) : Type u_1

A randomized statistical test on the output space.

Equations

• Cslib.Crypto.PRG.Adversary Output = (Output → PMF Bool)

@[instance_reducible]

instance Cslib.Crypto.PRG.Generator.instFunLike {Seed : Type u_1} {Output : Type u_2} : FunLike (Generator Seed Output) Seed Output

Equations

• Cslib.Crypto.PRG.Generator.instFunLike = { coe := fun (G : Cslib.Crypto.PRG.Generator Seed Output) => G.toFun, coe_injective := ⋯ }

@[simp]

theorem Cslib.Crypto.PRG.Generator.coe_mk {Seed : Type u_1} {Output : Type u_2} (f : Seed → Output) : ⇑{ toFun := f } = f

def Cslib.Crypto.PRG.Generator.IsExpanding {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Fintype Output] (_G : Generator Seed Output) : Prop

A generator expands when its output space is strictly larger than its seed space.

Equations

• _G.IsExpanding = (Fintype.card Seed < Fintype.card Output)

noncomputable def Cslib.Crypto.PRG.Generator.outputDist {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] (G : Generator Seed Output) : PMF Output

The distribution obtained by applying the generator to a uniform seed.

Equations

• G.outputDist = PMF.map (⇑G) (Cslib.Probability.PMF.uniformOfFintype Seed)

noncomputable def Cslib.Crypto.PRG.Generator.realExperiment {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] (G : Generator Seed Output) (adversary : Adversary Output) : PMF Bool

Experiment 0 of Attack Game 3.1: give the adversary a generated output.

Equations

• G.realExperiment adversary = G.outputDist.bind adversary

noncomputable def Cslib.Crypto.PRG.Generator.idealExperiment {Output : Type u_2} [Fintype Output] [Nonempty Output] (adversary : Adversary Output) : PMF Bool

Experiment 1 of Attack Game 3.1: give the adversary a uniform output.

Equations

• Cslib.Crypto.PRG.Generator.idealExperiment adversary = (Cslib.Probability.PMF.uniformOfFintype Output).bind adversary

noncomputable def Cslib.Crypto.PRG.Generator.advantage {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : Generator Seed Output) (adversary : Adversary Output) : ℝ

The absolute difference of the probabilities of outputting true in the two experiments, as in Attack Game 3.1 of [BS23].

Equations

• G.advantage adversary = |((G.realExperiment adversary) true).toReal - ((Cslib.Crypto.PRG.Generator.idealExperiment adversary) true).toReal|

def Cslib.Crypto.PRG.Generator.Secure {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : Generator Seed Output) (Admissible : Adversary Output → Prop) (ε : NNReal) : Prop

Concrete security against admissible adversaries. The predicate is supplied by the caller, for example to restrict tests to a chosen computational resource bound. Taking Admissible := fun _ => True allows arbitrary adversaries.

Equations

• G.Secure Admissible ε = ∀ (adversary : Cslib.Crypto.PRG.Adversary Output), Admissible adversary → G.advantage adversary ≤ ↑ε