Uniform computational pseudorandom generators

A generator is ordinary functional code on lists of bits. Its finite family uses the existing PRG.Generator API on BitString n and BitString (length n). The output-length condition makes this representation exact: no padding or truncation enters the real experiment. Admissible finite tests must be realized by one uniform PPT program on every parameter and valid output word.

Security is the existing PRG.Family.Secure, with the seed length supplied as the parameter in both experiments. Its equivalence to computational indistinguishability lets reductions use list programs without manipulating dependent finite types. The real and ideal experiments below are executable fair-bit programs; their efficiency follows from the generator and length routine.

Main definitions

• Cslib.Crypto.PRG.wordFamily: the finite family represented by a word function.
• Cslib.Crypto.IsPPTBitStringTest: uniform realization of finite tests on valid words.
• Cslib.Crypto.PseudorandomGenerator: efficient generation, exact length, stretch and security.

Main results

• Cslib.Crypto.PRG.wordFamily_secure_iff: equivalence to word-ensemble indistinguishability.
• Cslib.Crypto.PseudorandomGenerator.of_indistinguishable: prove security with word programs.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 9.2.3.

Adapted from Crypto/Computational/PseudorandomGenerator.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, retaining the pinned finite PRG API.

noncomputable def Cslib.Crypto.generatorEnsemble (generator : List Bool → List Bool) (n : ℕ) : PMF (List Bool)

The output distribution of a word function on a uniform seed.

theorem Cslib.Crypto.generatorEnsemble_postprocess (generator : List Bool → List Bool) (f : ℕ → List Bool → List Bool) (n : ℕ) : generatorEnsemble (fun (seed : List Bool) => f seed.length (generator seed)) n = PMF.map (f n) (generatorEnsemble generator n)

Length-dependent postprocessing can use the sampled seed length as its parameter.

def Cslib.Crypto.PRG.wordFamily (generator : List Bool → List Bool) (length : ℕ → ℕ) : Family BitString fun (n : ℕ) => BitString (length n)

The finite family represented by a word function. An exact output-length hypothesis is required by the experiment and security bridges below.

def Cslib.Crypto.IsPPTBitStringTest {length : ℕ → ℕ} (test : (n : ℕ) → PRG.Adversary (BitString (length n))) : Prop

One uniform program realizes the entire finite test family on its valid output words. Its behavior on other word lengths is unrestricted, but its machine clock bounds every input.

theorem Cslib.Crypto.generatorEnsemble_eq_outputDist {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (word : List Bool), (generator word).length = length word.length) (n : ℕ) : generatorEnsemble generator n = PMF.map List.ofFn (PRG.wordFamily generator length n).outputDist

Exact output lengths identify finite generated samples with the original word distribution.

theorem Cslib.Crypto.PRG.wordFamily_realExperiment {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (word : List Bool), (generator word).length = length word.length) (adversary : Distinguisher) (n : ℕ) : ((wordFamily generator length n).realExperiment fun (bits : (fun (n : ℕ) => BitString (length n)) n) => (adversary n (List.ofFn bits)).eval) = distinguishingGame (generatorEnsemble generator n) (adversary n)

The finite and word experiments coincide for every uniformly realized test.

theorem Cslib.Crypto.PRG.wordFamily_idealExperiment (length : ℕ → ℕ) (adversary : Distinguisher) (n : ℕ) : (Generator.idealExperiment fun (bits : BitString (length n)) => (adversary n (List.ofFn bits)).eval) = distinguishingGame (BitString.uniformList (length n)) (adversary n)

The ideal finite test sees exactly the uniform word of the declared output length.

theorem Cslib.Crypto.PRG.wordFamily_secure_iff {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (word : List Bool), (generator word).length = length word.length) : (wordFamily generator length).Secure IsPPTBitStringTest ↔ ComputationallyIndistinguishable (generatorEnsemble generator) fun (n : ℕ) => BitString.uniformList (length n)

Finite-family security against uniformly realizable tests is exactly computational indistinguishability of the generated and uniform word ensembles.

noncomputable def Cslib.Crypto.prgRealGame (generator : List Bool → List Bool) (adversary : Distinguisher) (n : ℕ) : ProbComp Bool

Sample a uniform seed, evaluate the generator, and run the distinguisher.

noncomputable def Cslib.Crypto.prgIdealGame (length : ℕ → ℕ) (adversary : Distinguisher) (n : ℕ) : ProbComp Bool

Sample a uniform word at the declared length and run the distinguisher.

@[simp]

theorem Cslib.Crypto.eval_prgRealGame (generator : List Bool → List Bool) (adversary : Distinguisher) (n : ℕ) : (prgRealGame generator adversary n).eval = distinguishingGame (generatorEnsemble generator n) (adversary n)

The real program denotes the generated-word experiment.

@[simp]

theorem Cslib.Crypto.eval_prgIdealGame (length : ℕ → ℕ) (adversary : Distinguisher) (n : ℕ) : (prgIdealGame length adversary n).eval = distinguishingGame (BitString.uniformList (length n)) (adversary n)

The ideal program denotes the uniform-word experiment.

theorem Cslib.Crypto.isPPTOn_prgRealGame {generator : List Bool → List Bool} {adversary : Distinguisher} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (ha : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (prgRealGame generator adversary)

The real experiment is an efficient program when its generator and distinguisher are.

theorem Cslib.Crypto.isPPTOn_prgIdealGame {length : ℕ → ℕ} {adversary : Distinguisher} (hl : Turing.MultiTapeTM.ComputableTidilyInPolyTime length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (ha : Probability.IsPPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (prgIdealGame length adversary)

The ideal experiment is efficient when its length routine and distinguisher are.

structure Cslib.Crypto.PseudorandomGenerator (generator : List Bool → List Bool) (length : ℕ → ℕ) : Prop

A plain polynomial-time stretching generator, secure in the existing finite-family API.

• polyTime : Turing.MultiTapeTM.ComputableInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

  One deterministic polynomial-time machine evaluates the generator.

• length_eq (word : List Bool) : (generator word).length = length word.length

  The output length depends only on the seed length.

• stretch (n : ℕ) : n < length n

  Every seed length is strictly expanded.

• secure : (PRG.wordFamily generator length).Secure IsPPTBitStringTest

  The finite family is secure against uniformly realizable PPT tests.

theorem Cslib.Crypto.pseudorandomGenerator_iff_tidy {generator : List Bool → List Bool} {length : ℕ → ℕ} : PseudorandomGenerator generator length ↔ Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits ∧ (∀ (word : List Bool), (generator word).length = length word.length) ∧ (∀ (n : ℕ), n < length n) ∧ (PRG.wordFamily generator length).Secure IsPPTBitStringTest

Recover the tidy presentation for proofs without changing the security contract.

theorem Cslib.Crypto.PseudorandomGenerator.of_indistinguishable {generator : List Bool → List Bool} {length : ℕ → ℕ} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hlen : ∀ (word : List Bool), (generator word).length = length word.length) (hstretch : ∀ (n : ℕ), n < length n) (hsecure : ComputationallyIndistinguishable (generatorEnsemble generator) fun (n : ℕ) => BitString.uniformList (length n)) : PseudorandomGenerator generator length

Establish a uniform PRG with an ordinary word-ensemble security argument.

theorem Cslib.Crypto.PseudorandomGenerator.indistinguishable {generator : List Bool → List Bool} {length : ℕ → ℕ} (h : PseudorandomGenerator generator length) : ComputationallyIndistinguishable (generatorEnsemble generator) fun (n : ℕ) => BitString.uniformList (length n)

The generated words are computationally indistinguishable from uniform words.

theorem Cslib.Crypto.PRG.polyTime_length {generator : List Bool → List Bool} {length : ℕ → ℕ} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hlen : ∀ (word : List Bool), (generator word).length = length word.length) : Turing.MultiTapeTM.ComputableTidilyInPolyTime length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

Compute the expansion length by evaluating the generator on a canonical seed. No separate efficiency or security assumption on the length function is needed.

theorem Cslib.Crypto.PseudorandomGenerator.polyTime_length {generator : List Bool → List Bool} {length : ℕ → ℕ} (h : PseudorandomGenerator generator length) : Turing.MultiTapeTM.ComputableTidilyInPolyTime length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

A secure generator has an efficient unary expansion-length routine.

theorem Cslib.Crypto.PseudorandomGenerator.length_le {generator : List Bool → List Bool} {length : ℕ → ℕ} (h : PseudorandomGenerator generator length) : ∃ (c : ℕ) (d : ℕ), ∀ (n : ℕ), length n ≤ c * (n + 1) ^ d

The declared expansion is bounded by a polynomial in the seed length.