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

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.