Pseudorandom generators against arbitrary adversaries

The range-membership test accepts every generated output, whereas it accepts a uniform output with probability |range G| / |Output|. Its advantage is therefore at least 1 - |Seed| / |Output|. This proves that an expanding generator cannot have zero advantage against arbitrary adversaries, and gives a quantitative obstruction for every smaller error bound. No injectivity assumption on the generator is needed.

theorem Cslib.Crypto.PRG.Generator.advantage_nonneg {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : Generator Seed Output) (adversary : Adversary Output) : 0 ≤ G.advantage adversary

Advantage is nonnegative.

theorem Cslib.Crypto.PRG.Generator.advantage_le_one {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : Generator Seed Output) (adversary : Adversary Output) : G.advantage adversary ≤ 1

Advantage is at most one, with the normalization of Attack Game 3.1.

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

Error one imposes no restriction on a generator.

@[simp]

theorem Cslib.Crypto.PRG.Generator.advantage_const {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : Generator Seed Output) (p : PMF Bool) : (G.advantage fun (x : Output) => p) = 0

A test whose output distribution is independent of its input has zero advantage.

theorem Cslib.Crypto.PRG.Generator.secure_zero_of_outputDist_eq {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : Generator Seed Output) (hG : G.outputDist = Probability.PMF.uniformOfFintype Output) (Admissible : Adversary Output → Prop) : G.Secure Admissible 0

A generator with exactly uniform output is secure with zero error against any tests.

theorem Cslib.Crypto.PRG.Generator.secure_zero_iff_outputDist_eq_uniform {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : Generator Seed Output) : G.Secure (fun (x : Adversary Output) => True) 0 ↔ G.outputDist = Probability.PMF.uniformOfFintype Output

Zero-error security against arbitrary tests is equivalent to exactly uniform output.

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

Enlarging the allowed advantage preserves security.

theorem Cslib.Crypto.PRG.Generator.Secure.of_admissible {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] {G : Generator Seed Output} {Admissible Restricted : Adversary Output → Prop} {ε : NNReal} (h : G.Secure Admissible ε) (hsub : ∀ (adversary : Adversary Output), Restricted adversary → Admissible adversary) : G.Secure Restricted ε

Security against a larger class of adversaries implies security against a smaller class.

def Cslib.Crypto.PRG.Generator.rangeTest {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [DecidableEq Output] (G : Generator Seed Output) (output : Output) : Bool

Decide range membership by finite seed enumeration and output comparison.

noncomputable def Cslib.Crypto.PRG.Generator.rangeAdversary {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [DecidableEq Output] (G : Generator Seed Output) : Adversary Output

The deterministic adversary that tests membership in the generator's range.

@[simp]

theorem Cslib.Crypto.PRG.Generator.realExperiment_rangeAdversary {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [DecidableEq Output] (G : Generator Seed Output) : G.realExperiment G.rangeAdversary = PMF.pure true

The range test always accepts a generated output.

theorem Cslib.Crypto.PRG.Generator.idealExperiment_rangeAdversary {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Fintype Output] [Nonempty Output] [DecidableEq Output] (G : Generator Seed Output) : ((idealExperiment G.rangeAdversary) true).toReal = ↑(Nat.card ↑(Set.range ⇑G)) / ↑(Fintype.card Output)

The range test's acceptance probability under uniform sampling is the fraction of outputs in the range.

theorem Cslib.Crypto.PRG.Generator.advantage_rangeAdversary {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] [DecidableEq Output] (G : Generator Seed Output) : G.advantage G.rangeAdversary = 1 - ↑(Nat.card ↑(Set.range ⇑G)) / ↑(Fintype.card Output)

The exact advantage of the range-membership adversary.

theorem Cslib.Crypto.PRG.Generator.one_sub_card_div_le_advantage_rangeAdversary {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] [DecidableEq Output] (G : Generator Seed Output) : 1 - ↑(Fintype.card Seed) / ↑(Fintype.card Output) ≤ G.advantage G.rangeAdversary

Every generator has an unbounded distinguisher with advantage at least 1 - |Seed| / |Output|. Collisions can only improve this attack.

theorem Cslib.Crypto.PRG.Generator.not_secure_of_rangeAdversary {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] [DecidableEq Output] (G : Generator Seed Output) {Admissible : Adversary Output → Prop} {ε : NNReal} (ha : Admissible G.rangeAdversary) (hε : ↑ε < 1 - ↑(Fintype.card Seed) / ↑(Fintype.card Output)) : ¬G.Secure Admissible ε

Security is impossible below the range-test bound whenever that test is admissible.

theorem Cslib.Crypto.PRG.Generator.not_secure_zero_of_isExpanding {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : Generator Seed Output) (hG : G.IsExpanding) : ¬G.Secure (fun (x : Adversary Output) => True) 0

An expanding generator cannot be perfectly secure against arbitrary adversaries.

theorem Cslib.Crypto.PRG.Generator.not_exists_isExpanding_secure_zero {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] : ¬∃ (G : Generator Seed Output), G.IsExpanding ∧ G.Secure (fun (x : Adversary Output) => True) 0

There is no expanding, perfectly secure generator against arbitrary adversaries.

def Cslib.Crypto.PRG.Generator.prod {Seed : Type u_1} {Output : Type u_2} (G : Generator Seed Output) : Generator (Seed × Seed) (Output × Output)

Apply G separately to each component of a pair of seeds.

theorem Cslib.Crypto.PRG.Generator.outputDist_prod {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] (G : Generator Seed Output) : G.prod.outputDist = G.outputDist.bind fun (y₁ : Output) => PMF.map (fun (y₂ : Output) => (y₁, y₂)) G.outputDist

The output distribution of G.prod is two independent draws from G.outputDist.

noncomputable def Cslib.Crypto.PRG.Generator.leftReduction {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] (G : Generator Seed Output) (A : Adversary (Output × Output)) : Adversary Output

First hybrid distinguisher: given y₁, sample y₂ ← G.outputDist and run A (y₁, y₂).

noncomputable def Cslib.Crypto.PRG.Generator.rightReduction {Output : Type u_2} [Fintype Output] [Nonempty Output] (A : Adversary (Output × Output)) : Adversary Output

Second hybrid distinguisher: given y₂, sample u₁ ←$ Output and run A (u₁, y₂).

theorem Cslib.Crypto.PRG.Generator.realExperiment_prod {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] (G : Generator Seed Output) (A : Adversary (Output × Output)) : G.prod.realExperiment A = G.realExperiment (G.leftReduction A)

Real experiment for G.prod equals the real experiment for G against leftReduction.

theorem Cslib.Crypto.PRG.Generator.idealExperiment_leftReduction {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : Generator Seed Output) (A : Adversary (Output × Output)) : idealExperiment (G.leftReduction A) = G.realExperiment (rightReduction A)

Ideal experiment against leftReduction equals the real experiment against rightReduction (both equal the hybrid distribution (u₁, G(x₂))).

theorem Cslib.Crypto.PRG.Generator.idealExperiment_rightReduction {Output : Type u_2} [Fintype Output] [Nonempty Output] (A : Adversary (Output × Output)) : idealExperiment (rightReduction A) = idealExperiment A

Ideal experiment against rightReduction equals the ideal experiment for G.prod.

theorem Cslib.Crypto.PRG.Generator.advantage_prod_le {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : Generator Seed Output) (A : Adversary (Output × Output)) : G.prod.advantage A ≤ G.advantage (G.leftReduction A) + G.advantage (rightReduction A)

Hybrid advantage bound: Adv(G.prod, A) ≤ Adv(G, leftReduction) + Adv(G, rightReduction).

theorem Cslib.Crypto.PRG.Generator.Secure.prod {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] {G : Generator Seed Output} {Admissible₁ : Adversary Output → Prop} {Admissible₂ : Adversary (Output × Output) → Prop} {ε : NNReal} (hG : G.Secure Admissible₁ ε) (hLeft : ∀ (A : Adversary (Output × Output)), Admissible₂ A → Admissible₁ (G.leftReduction A)) (hRight : ∀ (A : Adversary (Output × Output)), Admissible₂ A → Admissible₁ (rightReduction A)) : G.prod.Secure Admissible₂ (2 * ε)

Concrete security of H(x₁, x₂) = (G(x₁), G(x₂)) via a two-step hybrid argument.