Pseudorandom Functions (PRFs)

This file defines pseudorandom functions and their security game.

A PRF adversary gets oracle access to uniform sampling plus a function D → R and tries to distinguish the real function PRF.eval k (for a random key k) from a truly random function (modeled as a lazy random oracle with consistent responses).

Main Definitions

• PRFScheme K D R — a PRF with key space K, domain D, and range R.
• PRFAdversary D R — a distinguisher with oracle access to D →ₒ R.
• prfRealExp — the real experiment (adversary queries PRF.eval k).
• prfIdealExp — the ideal experiment (adversary queries a random oracle).
• prfAdvantage — distinguishing advantage.

structure PRFScheme (K D R : Type) : Type

A pseudorandom function with key space K, domain D, and range R. Key generation is probabilistic; evaluation is deterministic given a key.

• keygen : ProbComp K
• eval : K → D → R

@[reducible]

def PRFScheme.PRFOracleSpec (_D R : Type) : OracleSpec (ℕ ⊕ _D)

Oracle interface for PRF distinguishers: unrestricted access to uniform sampling plus oracle access to the candidate function.

@[reducible, inline]

abbrev PRFScheme.PRFAdversary (D R : Type) : Type

A PRF adversary gets oracle access to uniform sampling and a function D → R, and outputs a boolean guess (true = "real PRF", false = "random function").

def PRFScheme.UniformKey {K D R : Type} [SampleableType K] (prf : PRFScheme K D R) : Prop

A PRF has uniform key generation when its keygen algorithm is exactly uniform sampling.

def PRFScheme.prfRealQueryImpl {K D R : Type} (prf : PRFScheme K D R) (k : K) : QueryImpl (PRFOracleSpec D R) ProbComp

Query implementation for the real PRF experiment. Uniform-sampling queries are handled by the ambient unifSpec; function queries are answered by prf.eval k.

def PRFScheme.prfIdealQueryImpl {D R : Type} [DecidableEq D] [SampleableType R] : QueryImpl (PRFOracleSpec D R) (StateT (OracleSpec.ofFn fun (x : D) => R).QueryCache ProbComp)

Query implementation for the ideal PRF experiment. Uniform-sampling queries are handled by the ambient unifSpec; function queries are answered by a lazy random oracle.

def PRFScheme.prfRealExp {K D R : Type} (prf : PRFScheme K D R) (adversary : PRFAdversary D R) : ProbComp Bool

Real PRF experiment: sample a key, let the adversary query prf.eval k.

def PRFScheme.prfIdealExp {D R : Type} [DecidableEq D] [SampleableType R] (adversary : PRFAdversary D R) : ProbComp Bool

Ideal PRF experiment: let the adversary query a lazy random oracle (consistent random function). The oracle caches responses so that the same input always yields the same output.

noncomputable def PRFScheme.prfAdvantage {K D R : Type} [DecidableEq D] [SampleableType R] (prf : PRFScheme K D R) (adversary : PRFAdversary D R) : ℝ

PRF advantage: how well the adversary distinguishes the real PRF from a random function.

Forwarding lemmas for the PRF query implementations

How prfRealQueryImpl/prfIdealQueryImpl act on a computation lifted in from the ambient unifSpec (their identity-handled left summand) and on a function (Sum.inr) query. These are the facts a PRF distinguisher reduction needs when it forwards its own uniform sampling / oracle access through the PRF experiment: the unifSpec side is transparent, and an inr query is exactly the candidate function (real: prf.eval k; ideal: the lazy random oracle).

@[simp]

theorem PRFScheme.simulateQ_prfRealQueryImpl_liftComp {K D R : Type} (prf : PRFScheme K D R) (k : K) {β : Type} (ob : OracleComp unifSpec β) : simulateQ (prf.prfRealQueryImpl k) (ob.liftComp (PRFOracleSpec D R)) = ob

The real PRF handler is transparent on a computation lifted in from unifSpec: its unifSpec side is the identity handler and the function oracle is never consulted.

@[simp]

theorem PRFScheme.simulateQ_prfIdealQueryImpl_liftComp {D R : Type} [DecidableEq D] [SampleableType R] {β : Type} (ob : OracleComp unifSpec β) : simulateQ prfIdealQueryImpl (ob.liftComp (PRFOracleSpec D R)) = liftM ob

The ideal (lazy random oracle) PRF handler is transparent on a computation lifted in from unifSpec, threading the cache: the result is just ob lifted into the cache state monad.

@[simp]

theorem PRFScheme.simulateQ_prfRealQueryImpl_inr {K D R : Type} (prf : PRFScheme K D R) (k : K) (d : D) : simulateQ (prf.prfRealQueryImpl k) (liftM (OracleSpec.query (Sum.inr d))) = pure (prf.eval k d)

A function query (Sum.inr) under the real PRF handler evaluates the PRF.

@[simp]

theorem PRFScheme.simulateQ_prfIdealQueryImpl_inr {D R : Type} [DecidableEq D] [SampleableType R] (q : D) : simulateQ prfIdealQueryImpl (liftM (OracleSpec.query (Sum.inr q))) = OracleSpec.randomOracle q

A function query (Sum.inr) under the ideal PRF handler is the lazy random oracle at that point.