Adaptive PRF and PRP games and the PRP/PRF switching lemma

The adversary is an OracleAdv D R Bool asking adaptive queries in D and receiving answers in R. The real game samples a key k once and answers with F k. The ideal PRF game answers with a lazily sampled random function and the ideal PRP game with a lazily sampled random injection (sampling without replacement, a random permutation when D = R); both keep the table of answered queries as oracle state. Each game is an SPComp Bool that leaves the heap unchanged, and the advantages are Advantage on these games.

Main definitions

• rfOracle, rpOracle — lazily sampled random function and random injection
• realGame F A, rfGame A, rpGame A — the real, PRF-ideal and PRP-ideal games
• PRF_q_Advantage F A, PRP_q_Advantage P A, RF_RP_Advantage A — the adaptive PRF, PRP and random-function/random-injection advantages

Main results

• RF_RP_Advantage_le — for an adversary with query bound q, RF_RP_Advantage A ≤ q(q-1)/2 / |R|
• PRF_q_Advantage_le — for an adversary with query bound q, PRF_q_Advantage P A ≤ PRP_q_Advantage P A + q(q-1)/2 / |R|
• PRF_q_Advantage_of_isQueryBound_zero, PRP_q_Advantage_of_isQueryBound_zero, RF_RP_Advantage_of_isQueryBound_zero — all advantages vanish without queries
• switching_bound_le_one — the bound is at most one when q(q-1) ≤ 2|R|

Proof

The random injection is written in resampling form (rpFlagOracle): a fresh query samples a uniform answer and, when the answer repeats a recorded one, resamples from the unused answers (uniform_bind_resample). Both oracles carry a flag set on such a repetition. The flagged oracles agree on every transition that leaves the flag cleared, so their runs agree on every outcome with the flag cleared (OracleAdv.run_apply_flag_false_eq). The flag is set with probability at most q(q-1)/2 / |R| (run_rfFlagOracle_flag_le). The flagged games write the final flag to the heap location flagLoc, which is the form consumed by SwitchingLemma.switching_from_birthday.

def CatCrypt.Crypto.PRPPRF.usedAnswers {D R : Type} [DecidableEq R] (t : List (D × R)) : Finset R

The answers recorded in a lazy-sampling table.

Equations

• CatCrypt.Crypto.PRPPRF.usedAnswers t = (List.map Prod.snd t).toFinset

theorem CatCrypt.Crypto.PRPPRF.card_usedAnswers_le {D R : Type} [DecidableEq R] (t : List (D × R)) : (usedAnswers t).card ≤ t.length

noncomputable def CatCrypt.Crypto.PRPPRF.freshDist {R : Type} [DecidableEq R] [Fintype R] [Nonempty R] (u : Finset R) : PMF R

Uniform distribution on the complement of u, and on all of R when the complement is empty.

Equations

• CatCrypt.Crypto.PRPPRF.freshDist u = if h : uᶜ.Nonempty then PMF.uniformOfFinset uᶜ h else PMF.uniformOfFintype R

theorem CatCrypt.Crypto.PRPPRF.uniform_bind_resample {R : Type} [DecidableEq R] [Fintype R] [Nonempty R] (u : Finset R) : ((PMF.uniformOfFintype R).bind fun (r : R) => if r ∈ u then freshDist u else PMF.pure r) = freshDist u

Sampling uniformly from R and resampling from the complement of u when the sample lies in u is sampling from freshDist u.

Lazily sampled oracles

noncomputable def CatCrypt.Crypto.PRPPRF.rfOracle {D R : Type} [DecidableEq D] [Fintype R] [Nonempty R] (t : List (D × R)) (d : D) : PMF (R × List (D × R))

Lazily sampled random function with the table as state: a recorded query returns its recorded answer; a fresh query samples a uniform answer and records it.

Equations

• CatCrypt.Crypto.PRPPRF.rfOracle t d = match List.lookup d t with | some r => PMF.pure (r, t) | none => PMF.map (fun (r : R) => (r, (d, r) :: t)) (PMF.uniformOfFintype R)

noncomputable def CatCrypt.Crypto.PRPPRF.rpOracle {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (t : List (D × R)) (d : D) : PMF (R × List (D × R))

Lazily sampled random injection (a random permutation when D = R) with the table as state: a recorded query returns its recorded answer; a fresh query samples uniformly without replacement from the answers not yet recorded, and records it.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCrypt.Crypto.PRPPRF.rfFlagOracle {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (s : List (D × R) × Bool) (d : D) : PMF (R × List (D × R) × Bool)

rfOracle with a flag, set when a fresh answer repeats a recorded answer.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCrypt.Crypto.PRPPRF.rpFlagOracle {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (s : List (D × R) × Bool) (d : D) : PMF (R × List (D × R) × Bool)

rpOracle in resampling form with a flag: a fresh query samples a uniform answer; when it repeats a recorded answer the flag is set and the answer is resampled from freshDist.

Equations

• One or more equations did not get rendered due to their size.

theorem CatCrypt.Crypto.PRPPRF.rfFlagOracle_map {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (s : List (D × R) × Bool) (d : D) : PMF.map (Prod.map id Prod.fst) (rfFlagOracle s d) = rfOracle s.1 d

theorem CatCrypt.Crypto.PRPPRF.rpFlagOracle_map {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (s : List (D × R) × Bool) (d : D) : PMF.map (Prod.map id Prod.fst) (rpFlagOracle s d) = rpOracle s.1 d

theorem CatCrypt.Crypto.PRPPRF.rfFlagOracle_apply_true_false {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (t : List (D × R)) (d : D) (r : R) (t' : List (D × R)) : (rfFlagOracle (t, true) d) (r, t', false) = 0

theorem CatCrypt.Crypto.PRPPRF.rpFlagOracle_apply_true_false {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (t : List (D × R)) (d : D) (r : R) (t' : List (D × R)) : (rpFlagOracle (t, true) d) (r, t', false) = 0

theorem CatCrypt.Crypto.PRPPRF.rfFlagOracle_apply_false_eq {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (s : List (D × R) × Bool) (d : D) (r : R) (t' : List (D × R)) : (rfFlagOracle s d) (r, t', false) = (rpFlagOracle s d) (r, t', false)

The collision probability

theorem CatCrypt.Crypto.PRPPRF.run_rfFlagOracle_flag_le {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] {α : Type} (A : OracleAdv D R α) (n : ℕ) (hA : A.IsQueryBound n) (t : List (D × R)) : (OracleAdv.run rfFlagOracle A (t, false)).toOuterMeasure {x : α × List (D × R) × Bool | x.2.2 = true} ≤ ↑(∑ i ∈ Finset.range n, (t.length + i)) / ↑(Fintype.card R)

Birthday bound for the flagged random function: from a table with m entries and the flag cleared, an adversary asking at most n queries sets the flag with probability at most (∑ i < n, (m + i)) / |R|.

Games

noncomputable def CatCrypt.Crypto.PRPPRF.pmfGame (p : PMF Bool) : Core.SPComp Bool

The heap-independent game returning a sample of p and leaving the heap unchanged.

Equations

• CatCrypt.Crypto.PRPPRF.pmfGame p h = PMF.map (fun (b : Bool) => some (b, h)) p

noncomputable def CatCrypt.Crypto.PRPPRF.keyedOracle {D R K : Type} (F : K → D → R) (k : K) : Unit → D → PMF (R × Unit)

The keyed oracle F k with no state.

Equations

• CatCrypt.Crypto.PRPPRF.keyedOracle F k x✝ d = PMF.pure (F k d, ())

noncomputable def CatCrypt.Crypto.PRPPRF.realGame {D R K : Type} [Fintype K] [Nonempty K] (F : K → D → R) (A : OracleAdv D R Bool) : Core.SPComp Bool

Real game: sample a key once, then run A against F k.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCrypt.Crypto.PRPPRF.rfGame {D R : Type} [DecidableEq D] [Fintype R] [Nonempty R] (A : OracleAdv D R Bool) : Core.SPComp Bool

Ideal PRF game: run A against the lazily sampled random function.

Equations

• CatCrypt.Crypto.PRPPRF.rfGame A = CatCrypt.Crypto.PRPPRF.pmfGame (PMF.map Prod.fst (CatCrypt.Crypto.OracleAdv.run CatCrypt.Crypto.PRPPRF.rfOracle A []))

noncomputable def CatCrypt.Crypto.PRPPRF.rpGame {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (A : OracleAdv D R Bool) : Core.SPComp Bool

Ideal PRP game: run A against the lazily sampled random injection (sampling without replacement).

Equations

• CatCrypt.Crypto.PRPPRF.rpGame A = CatCrypt.Crypto.PRPPRF.pmfGame (PMF.map Prod.fst (CatCrypt.Crypto.OracleAdv.run CatCrypt.Crypto.PRPPRF.rpOracle A []))

noncomputable def CatCrypt.Crypto.PRPPRF.PRF_q_Advantage {D R : Type} [DecidableEq D] [Fintype R] [Nonempty R] {K : Type} [Fintype K] [Nonempty K] (F : K → D → R) (A : OracleAdv D R Bool) : ENNReal

Adaptive PRF advantage of A against the keyed function F.

Equations

• CatCrypt.Crypto.PRPPRF.PRF_q_Advantage F A = CatCrypt.Crypto.Advantage (CatCrypt.Crypto.PRPPRF.realGame F A) (CatCrypt.Crypto.PRPPRF.rfGame A)

noncomputable def CatCrypt.Crypto.PRPPRF.PRP_q_Advantage {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] {K : Type} [Fintype K] [Nonempty K] (P : K → D → R) (A : OracleAdv D R Bool) : ENNReal

Adaptive PRP advantage of A against the keyed function P.

Equations

• CatCrypt.Crypto.PRPPRF.PRP_q_Advantage P A = CatCrypt.Crypto.Advantage (CatCrypt.Crypto.PRPPRF.realGame P A) (CatCrypt.Crypto.PRPPRF.rpGame A)

noncomputable def CatCrypt.Crypto.PRPPRF.RF_RP_Advantage {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (A : OracleAdv D R Bool) : ENNReal

Advantage of A in distinguishing the lazy random function from the lazy random injection.

Equations

• CatCrypt.Crypto.PRPPRF.RF_RP_Advantage A = CatCrypt.Crypto.Advantage (CatCrypt.Crypto.PRPPRF.rfGame A) (CatCrypt.Crypto.PRPPRF.rpGame A)

Flagged games

@[reducible, inline]

abbrev CatCrypt.Crypto.PRPPRF.flagLoc : Core.Location

The heap location recording the collision flag at the end of a flagged game.

Equations

• CatCrypt.Crypto.PRPPRF.flagLoc = { id := 0, ty := Bool, fintype := Bool.fintype, inhabited := instInhabitedBool }

noncomputable def CatCrypt.Crypto.PRPPRF.flagGame {D R : Type} (O : List (D × R) × Bool → D → PMF (R × List (D × R) × Bool)) (A : OracleAdv D R Bool) : Core.SPComp Bool

Run A against a flagged oracle from the empty table and write the final flag to flagLoc.

Equations

• CatCrypt.Crypto.PRPPRF.flagGame O A h = PMF.map (fun (x : Bool × List (D × R) × Bool) => some (x.1, h.set CatCrypt.Crypto.PRPPRF.flagLoc x.2.2)) (CatCrypt.Crypto.OracleAdv.run O A ([], false))

theorem CatCrypt.Crypto.PRPPRF.tsum_ite_map_some {β γ : Type} (p : PMF β) (f : β → γ) (P : γ → Prop) : (∑' (y : γ), if P y then (PMF.map (fun (x : β) => some (f x)) p) (some y) else 0) = p.toOuterMeasure {x : β | P (f x)}

Summing a pushforward along some ∘ f over the outcomes satisfying P is the probability of the preimage.

theorem CatCrypt.Crypto.PRPPRF.prTrue_pmfGame_map {β : Type} (p : PMF β) (g : β → Bool) (h₀ : Core.Heap) : prTrue (pmfGame (PMF.map g p)) h₀ = p.toOuterMeasure {x : β | g x = true}

theorem CatCrypt.Crypto.PRPPRF.prTrue_flagGame {D R : Type} (O : List (D × R) × Bool → D → PMF (R × List (D × R) × Bool)) (A : OracleAdv D R Bool) (h₀ : Core.Heap) : prTrue (flagGame O A) h₀ = (OracleAdv.run O A ([], false)).toOuterMeasure {x : Bool × List (D × R) × Bool | x.1 = true}

theorem CatCrypt.Crypto.PRPPRF.prEventComp_flagGame {D R : Type} (O : List (D × R) × Bool → D → PMF (R × List (D × R) × Bool)) (A : OracleAdv D R Bool) : (Unary.prEventComp (flagGame O A) Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => h'.get flagLoc = true) = (OracleAdv.run O A ([], false)).toOuterMeasure {x : Bool × List (D × R) × Bool | x.2.2 = true}

theorem CatCrypt.Crypto.PRPPRF.rfGame_eq {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (A : OracleAdv D R Bool) : prTrue (rfGame A) Core.Heap.empty = prTrue (flagGame rfFlagOracle A) Core.Heap.empty

theorem CatCrypt.Crypto.PRPPRF.rpGame_eq {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (A : OracleAdv D R Bool) : prTrue (rpGame A) Core.Heap.empty = prTrue (flagGame rpFlagOracle A) Core.Heap.empty

theorem CatCrypt.Crypto.PRPPRF.isLossless_flagGame {D R : Type} (O : List (D × R) × Bool → D → PMF (R × List (D × R) × Bool)) (A : OracleAdv D R Bool) : Unary.isLossless (flagGame O A)

theorem CatCrypt.Crypto.PRPPRF.RF_RP_Advantage_eq_flagGame {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (A : OracleAdv D R Bool) : RF_RP_Advantage A = Advantage (flagGame rfFlagOracle A) (flagGame rpFlagOracle A)

The switching lemma

theorem CatCrypt.Crypto.PRPPRF.RF_RP_Advantage_le {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] (A : OracleAdv D R Bool) (q : ℕ) (hA : A.IsQueryBound q) : RF_RP_Advantage A ≤ ↑(q * (q - 1) / 2) / ↑(Fintype.card R)

PRP/PRF switching lemma. An adversary asking at most q adaptive queries distinguishes the lazy random function from the lazy random injection with advantage at most q(q-1)/2 / |R|.

theorem CatCrypt.Crypto.PRPPRF.PRF_q_Advantage_le {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] {K : Type} [Fintype K] [Nonempty K] (P : K → D → R) (A : OracleAdv D R Bool) (q : ℕ) (hA : A.IsQueryBound q) : PRF_q_Advantage P A ≤ PRP_q_Advantage P A + ↑(q * (q - 1) / 2) / ↑(Fintype.card R)

PRF advantage from PRP advantage. For every adversary asking at most q adaptive queries, the PRF advantage of a keyed function is at most its PRP advantage plus q(q-1)/2 / |R|.

Sanity facts

theorem CatCrypt.Crypto.PRPPRF.realGame_eq_of_isQueryBound_zero {D R K : Type} [Fintype K] [Nonempty K] {S : Type} (F : K → D → R) (O : S → D → PMF (R × S)) (s : S) {A : OracleAdv D R Bool} (hA : A.IsQueryBound 0) : realGame F A = pmfGame (PMF.map Prod.fst (OracleAdv.run O A s))

Without queries, the real game and any ideal game over a table oracle have the same output distribution.

theorem CatCrypt.Crypto.PRPPRF.PRF_q_Advantage_of_isQueryBound_zero {D R : Type} [DecidableEq D] [Fintype R] [Nonempty R] {K : Type} [Fintype K] [Nonempty K] (F : K → D → R) {A : OracleAdv D R Bool} (hA : A.IsQueryBound 0) : PRF_q_Advantage F A = 0

With no queries, the PRF advantage is zero.

theorem CatCrypt.Crypto.PRPPRF.PRP_q_Advantage_of_isQueryBound_zero {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] {K : Type} [Fintype K] [Nonempty K] (P : K → D → R) {A : OracleAdv D R Bool} (hA : A.IsQueryBound 0) : PRP_q_Advantage P A = 0

With no queries, the PRP advantage is zero.

theorem CatCrypt.Crypto.PRPPRF.RF_RP_Advantage_of_isQueryBound_zero {D R : Type} [DecidableEq D] [DecidableEq R] [Fintype R] [Nonempty R] {A : OracleAdv D R Bool} (hA : A.IsQueryBound 0) : RF_RP_Advantage A = 0

With no queries, the random function and the random injection are indistinguishable.

theorem CatCrypt.Crypto.PRPPRF.isQueryBound_two_query {D R : Type} (d₁ d₂ : D) (g : R → R → Bool) : (OracleAdv.query d₁ fun (r₁ : R) => OracleAdv.query d₂ fun (r₂ : R) => OracleAdv.ret (g r₁ r₂)).IsQueryBound 2

The two-query adversary that queries d₁ and d₂ and outputs whether the answers coincide asks at most two queries.

theorem CatCrypt.Crypto.PRPPRF.switching_bound_le_one {R : Type} [Fintype R] (q : ℕ) (hq : q * (q - 1) ≤ 2 * Fintype.card R) : ↑(q * (q - 1) / 2) / ↑(Fintype.card R) ≤ 1

The switching bound is at most one when q(q-1) ≤ 2|R|.