Uniform computational pseudorandom functions

Keys, valid queries and answers have length n. An adversary receives the unary security parameter, independent private randomness and adaptive access to one word channel. The real game samples one key; the ideal game samples one whole function and reuses it across calls. Both games invoke the adversary with empty auxiliary input and reject malformed queries with the empty word. The table is a semantic specification; RandomOracle certifies a lazy realization of the same law for oracle-PPT adversaries.

The keyed evaluator has a uniform deterministic TM certificate on the encoded key/query pair. Admissible adversaries satisfy IsOraclePPT, charging ordinary computation and request writing, with one machine and polynomial for all parameters and auxiliary inputs.

Main definitions

• Cslib.Crypto.OracleDistinguisher: a parameterized randomized adaptive oracle test.
• Cslib.Crypto.prfRealGame, .prfIdealGame: the keyed and random-function experiments.
• Cslib.Crypto.PseudorandomFunction: efficient evaluation, length and adaptive security.

Main results

• Cslib.Crypto.interpret_randomFunctionQuery: correctness of the finite-domain adapter.
• Cslib.Crypto.prfIdealGame_eq_lazy: an exact lazy implementation of the ideal experiment.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Chapter 4.
• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions.

Adapted from Crypto/Computational/PseudorandomFunction.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared typed interpreter and word channel.

@[reducible, inline]

abbrev Cslib.Crypto.OracleDistinguisher : Type

An adaptive test with a unary parameter, an auxiliary word and one external word channel.

def Cslib.Crypto.prfOracle (family : List Bool → List Bool → List Bool) (n : ℕ) (key query : List Bool) : List Bool

A keyed oracle rejects queries outside the declared domain.

def Cslib.Crypto.randomFunctionOracle (n : ℕ) (table : BitString n → BitString n) (query : List Bool) : List Bool

Read a fixed random table, rejecting malformed words before interpreting their bits.

def Cslib.Crypto.randomFunctionQuery (n : ℕ) (query : List Bool) : ProbOracleComp (fun (x : BitString n) => BitString n) (List Bool)

Adapt a valid word to the finite domain. Malformed words make no external call.

theorem Cslib.Crypto.interpret_randomFunctionQuery {m : Type → Type u_1} [Monad m] [LawfulMonad m] (random : (n : ℕ) → m (Fin (n + 1))) (n : ℕ) (table : BitString n → BitString n) (query : List Bool) : OracleComp.interpret (ProbOracleComp.handler random fun (bits : BitString n) => pure (table bits)) (randomFunctionQuery n query) = pure (randomFunctionOracle n table query)

The finite query adapter preserves the word-valued table interface in every lawful monad.

noncomputable def Cslib.Crypto.lazyRandomFunctionOracle (n : ℕ) (query : List Bool) : StateT (RandomOracle.Cache fun (x : BitString n) => BitString n) PMF (List Bool)

A semantic random-function cache, retaining only the finite-domain answers already used.

noncomputable def Cslib.Crypto.prfRealGame (family : List Bool → List Bool → List Bool) (adversary : OracleDistinguisher) (n : ℕ) : ProbComp Bool

Sample one key and reuse it across every adaptive call.

noncomputable def Cslib.Crypto.prfIdealGame (adversary : OracleDistinguisher) (n : ℕ) : ProbComp Bool

Sample one whole random function, independently of the adversary's private samples.

theorem Cslib.Crypto.prfIdealGame_eq_lazy (adversary : OracleDistinguisher) (n : ℕ) : (prfIdealGame adversary n).eval = PMF.map Prod.fst ((OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifOracle k)) fun (request : Unit × List Bool) => lazyRandomFunctionOracle n request.2) (adversary n [])).run fun (x : BitString n) => none)

The ideal game admits consistent lazy answers to adaptive queries, with private randomness independent of the table and the same rejection convention for malformed inputs.

structure Cslib.Crypto.PseudorandomFunction (family : List Bool → List Bool → List Bool) : Prop

A keyed family evaluated in plain polynomial time, secure against every uniform adaptive oracle test.

• polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

  One deterministic machine evaluates the family from the encoded key and query.

• length_eq (key query : List Bool) : query.length = key.length → (family key query).length = key.length

  Valid queries receive answers of the declared width.

• secure : Game.Indistinguishable (fun (adversary : OracleDistinguisher) (n : ℕ) => (prfRealGame family adversary n).eval) (fun (adversary : OracleDistinguisher) (n : ℕ) => (prfIdealGame adversary n).eval) (Probability.IsOraclePPT Turing.MultiTapeTM.encBool)

  The real and ideal experiments use the common game-security calculus.

theorem Cslib.Crypto.pseudorandomFunction_iff_tidy {family : List Bool → List Bool → List Bool} : PseudorandomFunction family ↔ Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits ∧ (∀ (key query : List Bool), query.length = key.length → (family key query).length = key.length) ∧ Game.Indistinguishable (fun (adversary : OracleDistinguisher) (n : ℕ) => (prfRealGame family adversary n).eval) (fun (adversary : OracleDistinguisher) (n : ℕ) => (prfIdealGame adversary n).eval) (Probability.IsOraclePPT Turing.MultiTapeTM.encBool)

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