Finite PRGs in the common game calculus

The pinned finite PRG API measures advantage in the reals. The shared game API uses the same quantity in the nonnegative reals. These bridges identify their concrete and asymptotic security notions without changing the generator or introducing another definition of PRG security.

Main results

• Cslib.Crypto.PRG.Generator.advantage_eq_game: identical advantage conventions.
• Cslib.Crypto.PRG.Family.secure_iff_indistinguishable: identical asymptotic security.

References

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

theorem Cslib.Crypto.PRG.Generator.advantage_eq_game {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 = ↑(Game.advantage (G.realExperiment adversary) (idealExperiment adversary))

Finite PRGs and Boolean security games use the same distinguishing advantage.

theorem Cslib.Crypto.PRG.Family.secure_iff_indistinguishable {Seed : ℕ → Type u_1} {Output : ℕ → Type u_2} [(n : ℕ) → Fintype (Seed n)] [∀ (n : ℕ), Nonempty (Seed n)] [(n : ℕ) → Fintype (Output n)] [∀ (n : ℕ), Nonempty (Output n)] (G : Family Seed Output) (Admissible : ((n : ℕ) → Adversary (Output n)) → Prop) : G.Secure Admissible ↔ Game.Indistinguishable (fun (adversary : (n : ℕ) → Adversary (Output n)) (n : ℕ) => (G n).realExperiment (adversary n)) (fun (adversary : (n : ℕ) → Adversary (Output n)) (n : ℕ) => Generator.idealExperiment (adversary n)) Admissible

Finite-family PRG security is indistinguishability of its real and ideal games.

theorem Cslib.Crypto.PRG.Family.secureWithError_iff_indistinguishableWithError {Seed : ℕ → Type u_1} {Output : ℕ → Type u_2} [(n : ℕ) → Fintype (Seed n)] [∀ (n : ℕ), Nonempty (Seed n)] [(n : ℕ) → Fintype (Output n)] [∀ (n : ℕ), Nonempty (Output n)] (G : Family Seed Output) (Admissible : ((n : ℕ) → Adversary (Output n)) → Prop) (ε : ℕ → NNReal) : G.SecureWithError Admissible ε ↔ Game.IndistinguishableWithError (fun (adversary : (n : ℕ) → Adversary (Output n)) (n : ℕ) => (G n).realExperiment (adversary n)) (fun (adversary : (n : ℕ) → Adversary (Output n)) (n : ℕ) => Generator.idealExperiment (adversary n)) Admissible ε

Concrete finite-family PRG security is the same common game advantage bound.