Asymptotic pseudorandom generator security

Security for families of generators means negligible advantage for each admissible adversary family, following [BS23], Definition 3.1. Negligibility uses Mathlib's Asymptotics.SuperpolynomialDecay. Admissibility is a predicate on the whole adversary family, so a downstream computational model can express a uniform resource restriction. This model has a natural-number security parameter and no sampled public system parameters. Efficiency of generation and sampling is not asserted by these semantic definitions.

SecureWithError bounds every admissible family's advantage at parameter n by ε n. A negligible bound implies Secure.

A non-negligible lower bound on the fraction of outputs outside the image rules out security when the range-test family is admissible. In particular, a bitstring family that eventually stretches by at least one bit is insecure against any class admitting its range test.

@[reducible, inline]

abbrev Cslib.Crypto.PRG.Family (Seed : ℕ → Type u_1) (Output : ℕ → Type u_2) : Type (max u_2 u_1)

A security-parameter-indexed collection of deterministic generators.

Equations

• Cslib.Crypto.PRG.Family Seed Output = ((n : ℕ) → Cslib.Crypto.PRG.Generator (Seed n) (Output n))

def Cslib.Crypto.PRG.Family.Secure {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) : Prop

Every admissible adversary family has negligible distinguishing advantage. The predicate can encode computational restrictions; fun _ => True permits all families.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Crypto.PRG.Family.Secure.of_admissible {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 Restricted : ((n : ℕ) → Adversary (Output n)) → Prop} (h : G.Secure Admissible) (hsub : ∀ (adversary_family : (n : ℕ) → Adversary (Output n)), Restricted adversary_family → Admissible adversary_family) : G.Secure Restricted

Restricting the admissible adversary families preserves asymptotic security.

def Cslib.Crypto.PRG.Family.SecureWithError {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) : Prop

Every admissible adversary family has advantage at most ε n at each parameter n.

Equations

• G.SecureWithError Admissible ε = ∀ (adversary_family : (n : ℕ) → Cslib.Crypto.PRG.Adversary (Output n)), Admissible adversary_family → ∀ (n : ℕ), (G n).advantage (adversary_family n) ≤ ↑(ε n)

theorem Cslib.Crypto.PRG.Family.SecureWithError.secure {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} (h : G.SecureWithError Admissible ε) (hε : Asymptotics.SuperpolynomialDecay Filter.atTop (fun (n : ℕ) => ↑n) fun (n : ℕ) => ↑(ε n)) : G.Secure Admissible

A negligible error bound implies asymptotic security.

theorem Cslib.Crypto.PRG.Family.not_secure_of_rangeAdversary {Seed : ℕ → Type u_1} {Output : ℕ → Type u_2} [(n : ℕ) → Fintype (Seed n)] [∀ (n : ℕ), Nonempty (Seed n)] [(n : ℕ) → Fintype (Output n)] [∀ (n : ℕ), Nonempty (Output n)] [(n : ℕ) → DecidableEq (Output n)] (G : Family Seed Output) {Admissible : ((n : ℕ) → Adversary (Output n)) → Prop} (ha : Admissible fun (n : ℕ) => (G n).rangeAdversary) {δ : ℕ → NNReal} (hδ : ¬Asymptotics.SuperpolynomialDecay Filter.atTop (fun (n : ℕ) => ↑n) fun (n : ℕ) => ↑(δ n)) (hgap : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(δ n) ≤ 1 - ↑(Nat.card ↑(Set.range ⇑(G n))) / ↑(Fintype.card (Output n))) : ¬G.Secure Admissible

A non-negligible lower bound on the fraction of outputs outside the image rules out security whenever exhaustive range testing is admissible.

theorem Cslib.Crypto.PRG.Family.not_secure_of_two_mul_card_le {Seed : ℕ → Type u_1} {Output : ℕ → Type u_2} [(n : ℕ) → Fintype (Seed n)] [∀ (n : ℕ), Nonempty (Seed n)] [(n : ℕ) → Fintype (Output n)] [∀ (n : ℕ), Nonempty (Output n)] [(n : ℕ) → DecidableEq (Output n)] (G : Family Seed Output) {Admissible : ((n : ℕ) → Adversary (Output n)) → Prop} (ha : Admissible fun (n : ℕ) => (G n).rangeAdversary) (hsize : ∀ᶠ (n : ℕ) in Filter.atTop, 2 * Fintype.card (Seed n) ≤ Fintype.card (Output n)) : ¬G.Secure Admissible

If outputs eventually outnumber seeds by a factor of two, admissibility of exhaustive seed enumeration and output comparison suffices to rule out security.

theorem Cslib.Crypto.PRG.Family.not_secure_of_bitstring_stretch {seedLength outputLength : ℕ → ℕ} (G : Family (fun (n : ℕ) => Fin (seedLength n) → Bool) fun (n : ℕ) => Fin (outputLength n) → Bool) {Admissible : ((n : ℕ) → Adversary (Fin (outputLength n) → Bool)) → Prop} (ha : Admissible fun (n : ℕ) => (G n).rangeAdversary) (hstretch : ∀ᶠ (n : ℕ) in Filter.atTop, seedLength n < outputLength n) : ¬G.Secure Admissible

A bitstring generator that eventually stretches by at least one bit is insecure against any class admitting its range-test family.

theorem Cslib.Crypto.PRG.Family.not_exists_secure_bitstring_stretch {seedLength outputLength : ℕ → ℕ} (hstretch : ∀ᶠ (n : ℕ) in Filter.atTop, seedLength n < outputLength n) : ¬∃ (G : Family (fun (n : ℕ) => Fin (seedLength n) → Bool) fun (n : ℕ) => Fin (outputLength n) → Bool), G.Secure fun (x : (n : ℕ) → Adversary (Fin (outputLength n) → Bool)) => True

No bitstring generator family that eventually stretches by at least one bit is secure against all adversary families.

theorem Cslib.Crypto.PRG.Family.not_secure_of_bitVec_stretch {seedLength outputLength : ℕ → ℕ} (G : Family (fun (n : ℕ) => BitVec (seedLength n)) fun (n : ℕ) => BitVec (outputLength n)) {Admissible : ((n : ℕ) → Adversary (BitVec (outputLength n))) → Prop} (ha : Admissible fun (n : ℕ) => (G n).rangeAdversary) (hstretch : ∀ᶠ (n : ℕ) in Filter.atTop, seedLength n < outputLength n) : ¬G.Secure Admissible

A BitVec generator that eventually stretches by at least one bit is insecure against any class admitting its range-test family.

theorem Cslib.Crypto.PRG.Family.not_exists_secure_bitVec_stretch {seedLength outputLength : ℕ → ℕ} (hstretch : ∀ᶠ (n : ℕ) in Filter.atTop, seedLength n < outputLength n) : ¬∃ (G : Family (fun (n : ℕ) => BitVec (seedLength n)) fun (n : ℕ) => BitVec (outputLength n)), G.Secure fun (x : (n : ℕ) → Adversary (BitVec (outputLength n))) => True

No BitVec generator family that eventually stretches by at least one bit is secure against all adversary families.