Adaptive GGM security from pseudorandom generators

The tree evaluator is a pseudorandom function whenever its two-child expansion is efficient and pseudorandom. Each strict oracle-PPT adversary has one polynomial query budget. The single uniform reduction loses the product of the level-selection and sample-selection ranges, which is polynomial in the security parameter. The bound may depend on the fixed adversary.

Surplus generator bits are truncated to two labels. This preserves both security and tree evaluation, accommodating the strict PRG convention at seed length zero.

Main results

• Cslib.Crypto.GGM.pseudorandomFunction_of_indistinguishable: adaptive GGM security for efficient pseudorandom two-child expansions.
• Cslib.Crypto.PseudorandomGenerator.ggm: a generator supplying at least two labels gives a PRF.
• Cslib.Crypto.PseudorandomGenerator.exists_pseudorandomFunction: every uniform PRG gives a uniform PRF, using the existing polynomial-stretch construction.

References

• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions, Sections 3.2–3.3, construction and Theorem 3.

Adapted from Crypto/Computational/GGM/Security.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared typed oracle and game calculus.

theorem Cslib.Crypto.GGM.pseudorandomFunction_of_indistinguishable {generator : List Bool → List Bool} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hlength : ∀ (seed : List Bool), (generator seed).length = 2 * seed.length) (hsecure : ComputationallyIndistinguishable (generatorEnsemble generator) fun (n : ℕ) => BitString.uniformList (2 * n)) : PseudorandomFunction (eval generator)

The GGM tree of an efficient pseudorandom two-child expansion is secure against every uniform strict polynomial-time adaptive oracle adversary with independent private randomness.

theorem Cslib.Crypto.PseudorandomGenerator.ggm {generator : List Bool → List Bool} {length : ℕ → ℕ} (hgenerator : PseudorandomGenerator generator length) (hdouble : ∀ (n : ℕ), 2 * n ≤ length n) : PseudorandomFunction (GGM.eval generator)

A secure generator providing at least two full labels gives the GGM pseudorandom function. Surplus bits are ignored; the hypothesis accommodates seed length zero.

theorem Cslib.Crypto.PseudorandomGenerator.exists_pseudorandomFunction {generator : List Bool → List Bool} {length : ℕ → ℕ} (hgenerator : PseudorandomGenerator generator length) : ∃ (family : List Bool → List Bool → List Bool), PseudorandomFunction family

Every uniform pseudorandom generator yields a uniform adaptive pseudorandom function. Truncate to one extra bit, amplify to two labels plus one bit, and apply GGM.