Pseudorandom functions from one-way functions

Combine the general OWF-to-PRG theorem with the GGM construction. The conclusion includes an efficient deterministic evaluator and security against uniform adaptive oracle PPT adversaries. Existence of the one-way function is the sole cryptographic assumption.

Main results

• Cslib.Crypto.OneWay.exists_pseudorandomFunction: every uniform OWF implies an adaptive PRF.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions, Sections 4–5.
• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions, Sections 3.2–3.3.

Adapted from Crypto/Computational/OneWayToPRF.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed machine certificates and the nonnegative game API.

theorem Cslib.Crypto.OneWay.exists_pseudorandomFunction {f : List Bool → List Bool} (hf : OneWay f) : ∃ (family : List Bool → List Bool → List Bool), PseudorandomFunction family

Every uniform one-way function implies a uniform pseudorandom function secure against adaptive, strict polynomial-time oracle adversaries.