Forking Lemma

This file provides a general forking lemma for adversaries in the Random Oracle Model (ROM) with a single oracle query (q = 1).

Overview

The forking lemma (Bellare-Neven 2006, Pointcheval-Stern 2000) is a key tool for security reductions of signature schemes in the ROM. It shows that if an adversary succeeds with probability acc, then running the adversary twice with the same randomness but different oracle responses produces two accepting transcripts with probability at least acc² - acc/|R|.

Model

We decompose the adversary into two phases:

1. Commit phase (coins): Probabilistic; produces a commitment c using internal randomness. This models everything the adversary does before the oracle query.
2. Response phase (respond): Deterministic; given the commitment c and oracle response e, produces the final output y. This models the adversary's computation after receiving the oracle response.

The forking algorithm:

1. Run coins once to get commitment c
2. Sample two independent oracle responses e₁, e₂ ← uniform R
3. Compute y₁ = respond(x, c, e₁) and y₂ = respond(x, c, e₂)
4. Succeed if both accept(y₁) and accept(y₂) and e₁ ≠ e₂

Since the commit phase is shared, both runs produce the same commitment, enabling special soundness extraction from the two accepting transcripts.

Main results

• ForkableAdversary - Two-phase adversary structure
• forkAlg - The forking algorithm
• jensen_sub_pmf_sq - Jensen's inequality: E[f²] ≥ (E[f])² for sub-PMF weights
• fork_success_ge - Forking lemma: fork success probability ≥ acc² - acc/|R|

References

• [Bellare, Neven, Multi-signatures in the plain public-key model]
• [Pointcheval, Stern, Security arguments for digital signatures and blind signatures]
• [Firsov, Unruh, Reflection, rewinding, and coin-toss in EasyCrypt]

Forkable Adversary Model

structure CatCrypt.Crypto.ForkingLemma.ForkableAdversary (X C R Y : Type) : Type

Two-phase adversary for the ROM forking lemma (q = 1 oracle query).

The adversary is decomposed into:

• coins: Probabilistic commitment phase (uses internal randomness)
• respond: Deterministic response phase (given commitment and oracle response)

This decomposition enables forking: replay the adversary with the same commitment but a different oracle response.

• coins : X → Core.SPComp C

  Phase 1: Probabilistic commitment. Given input x, produce commitment c.

• respond : X → C → R → Y

  Phase 2: Deterministic response. Given input x, commitment c, and oracle response r, produce output y.

noncomputable def CatCrypt.Crypto.ForkingLemma.ForkableAdversary.run {X C R Y : Type} [Fintype R] [Nonempty R] (A : ForkableAdversary X C R Y) (x : X) : Core.SPComp Y

Run the adversary: commit then respond with a uniform oracle sample.

Equations

• A.run x = do let c ← A.coins x let e ← CatCrypt.Core.SPComp.sample R CatCrypt.Core.SPComp.pure (A.respond x c e)

noncomputable def CatCrypt.Crypto.ForkingLemma.acceptProb {X C R Y : Type} [Fintype R] [Nonempty R] (A : ForkableAdversary X C R Y) (x : X) (accept : Y → Bool) : ENNReal

Acceptance probability of the adversary.

Equations

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

noncomputable def CatCrypt.Crypto.ForkingLemma.forkAlg {X C R Y : Type} [Fintype R] [Nonempty R] (A : ForkableAdversary X C R Y) (x : X) : Core.SPComp (C × R × Y × R × Y)

The forking algorithm: run the adversary twice with shared commitment but independent oracle responses.

Equations

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

noncomputable def CatCrypt.Crypto.ForkingLemma.forkSuccProb {X C R Y : Type} [Fintype R] [Nonempty R] [DecidableEq R] (A : ForkableAdversary X C R Y) (x : X) (accept : Y → Bool) : ENNReal

Fork success probability: both runs accept and oracle responses differ.

Equations

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

Jensen's Inequality for ENNReal

The key mathematical ingredient for the forking lemma is Jensen's inequality for the convex function x² under sub-probability weights: (∑ w(i) * f(i))² ≤ ∑ w(i) * f(i)² when ∑ w(i) ≤ 1 and f(i) ≤ 1.

The proof uses the AM-GM inequality pointwise.

theorem CatCrypt.Crypto.ForkingLemma.ennreal_two_mul_le_add_sq (a b : ENNReal) : 2 * a * b ≤ a ^ 2 + b ^ 2

AM-GM inequality for ENNReal: 2 * a * b ≤ a² + b².

theorem CatCrypt.Crypto.ForkingLemma.jensen_sub_pmf_sq {ι : Type} (w f : ι → ENNReal) (hw_sum : ∑' (i : ι), w i ≤ 1) (hf : ∀ (i : ι), f i ≤ 1) : (∑' (i : ι), w i * f i) ^ 2 ≤ ∑' (i : ι), w i * f i ^ 2

Jensen's inequality for squaring under sub-PMF weights.

For weights w with ∑ w ≤ 1 and bounded function f ≤ 1: (∑ w(i) * f(i))² ≤ ∑ w(i) * f(i)²

Proof: By AM-GM, 2 * f(i) * μ ≤ f(i)² + μ². Multiply by w(i) and sum: 2μ² ≤ E[f²] + (∑ w) * μ² ≤ E[f²] + μ² Cancel μ² (finite since μ ≤ 1) to get μ² ≤ E[f²].

Representation Lemmas

theorem CatCrypt.Crypto.ForkingLemma.prTrue_bind_eq_weighted {α : Type} (c : Core.SPComp α) (k : α → Core.SPComp Bool) (h₀ : Core.Heap) : prTrue (c.bind k) h₀ = ∑' (p : Option (α × Core.Heap)), (c h₀) p * match p with | some (a, h') => prTrue (k a) h' | none => 0

prTrue of a bind decomposes as a weighted sum over the PMF of the first computation.

theorem CatCrypt.Crypto.ForkingLemma.prTrue_pure_bool (b : Bool) (h₀ : Core.Heap) : prTrue (Core.SPComp.pure b) h₀ = if b = true then 1 else 0

prTrue of a pure Boolean.

theorem CatCrypt.Crypto.ForkingLemma.prTrue_sample_pure_bool {R : Type} [Fintype R] [Nonempty R] (g : R → Bool) (h₀ : Core.Heap) : prTrue ((Core.SPComp.sample R).bind fun (e : R) => Core.SPComp.pure (g e)) h₀ = ↑{e : R | g e = true}.card / ↑(Fintype.card R)

prTrue of sampling from R then applying a pure Boolean function.

Monotonicity Lemmas for prTrue

theorem CatCrypt.Crypto.ForkingLemma.prTrue_pure_decide_mono {Q R : Prop} [Decidable Q] [Decidable R] (h : Q → R) (h₀ : Core.Heap) : prTrue (Core.SPComp.pure (decide Q)) h₀ ≤ prTrue (Core.SPComp.pure (decide R)) h₀

If Q → R, then prTrue(pure(decide Q)) ≤ prTrue(pure(decide R)).

theorem CatCrypt.Crypto.ForkingLemma.prTrue_bind_mono {α : Type} (c : Core.SPComp α) (k₁ k₂ : α → Core.SPComp Bool) (h₀ : Core.Heap) (hk : ∀ (a : α) (h' : Core.Heap), prTrue (k₁ a) h' ≤ prTrue (k₂ a) h') : prTrue (c.bind k₁) h₀ ≤ prTrue (c.bind k₂) h₀

Monotonicity of prTrue under bind: if k₁ is pointwise ≤ k₂, then bind c k₁ ≤ bind c k₂.

theorem CatCrypt.Crypto.ForkingLemma.prTrue_bind_mono_const {α : Type} (c : ENNReal) (comp : Core.SPComp α) (k₁ k₂ : α → Core.SPComp Bool) (h₀ : Core.Heap) (hk : ∀ (a : α) (h' : Core.Heap), prTrue (k₁ a) h' ≤ c * prTrue (k₂ a) h') : prTrue (comp.bind k₁) h₀ ≤ c * prTrue (comp.bind k₂) h₀

Scaled monotonicity: if prTrue(k₁ a) ≤ c * prTrue(k₂ a) pointwise, then prTrue(bind comp k₁) ≤ c * prTrue(bind comp k₂).

theorem CatCrypt.Crypto.ForkingLemma.prTrue_sample_bind_ge {R : Type} [Fintype R] [Nonempty R] (k : R → Core.SPComp Bool) (a₀ : R) (h₀ : Core.Heap) : (↑(Fintype.card R))⁻¹ * prTrue (k a₀) h₀ ≤ prTrue ((Core.SPComp.sample R).bind k) h₀

Lower bound: sampling then testing has probability ≥ 1/|R| times any witness's probability.

Forking Lemma

noncomputable def CatCrypt.Crypto.ForkingLemma.condAccProb {X C R Y : Type} [Fintype R] [Nonempty R] (A : ForkableAdversary X C R Y) (x : X) (accept : Y → Bool) (c : C) (h₀ : Core.Heap) : ENNReal

Conditional acceptance probability for a fixed commitment c.

Equations

• CatCrypt.Crypto.ForkingLemma.condAccProb A x accept c h₀ = CatCrypt.Crypto.prTrue ((CatCrypt.Core.SPComp.sample R).bind fun (e : R) => CatCrypt.Core.SPComp.pure (accept (A.respond x c e))) h₀

noncomputable def CatCrypt.Crypto.ForkingLemma.condForkProb {X C R Y : Type} [Fintype R] [Nonempty R] [DecidableEq R] (A : ForkableAdversary X C R Y) (x : X) (accept : Y → Bool) (c : C) (h₀ : Core.Heap) : ENNReal

Conditional fork success probability for a fixed commitment c.

Equations

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

theorem CatCrypt.Crypto.ForkingLemma.prTrue_double_sample_pure_bool {R : Type} [Fintype R] [Nonempty R] (f : R → R → Bool) (h₀ : Core.Heap) : prTrue ((Core.SPComp.sample R).bind fun (e₁ : R) => (Core.SPComp.sample R).bind fun (e₂ : R) => Core.SPComp.pure (f e₁ e₂)) h₀ = ↑{p ∈ Finset.univ ×ˢ Finset.univ | f p.1 p.2 = true}.card / ↑(Fintype.card R) ^ 2

prTrue of two independent samples from R then applying a pure Boolean function. The result counts accepting pairs divided by N².

theorem CatCrypt.Crypto.ForkingLemma.condForkProb_eq {X C R Y : Type} [Fintype R] [Nonempty R] [DecidableEq R] (A : ForkableAdversary X C R Y) (x : X) (accept : Y → Bool) (c : C) (h₀ : Core.Heap) : condForkProb A x accept c h₀ = condAccProb A x accept c h₀ ^ 2 - condAccProb A x accept c h₀ / ↑(Fintype.card R)

The conditional fork probability equals acc_c² - acc_c/|R| (exact counting).

theorem CatCrypt.Crypto.ForkingLemma.acceptProb_decompose {X C R Y : Type} [Fintype R] [Nonempty R] (A : ForkableAdversary X C R Y) (x : X) (accept : Y → Bool) : acceptProb A x accept = ∑' (p : Option (C × Core.Heap)), (A.coins x Core.Heap.empty) p * match p with | some (c, h') => condAccProb A x accept c h' | none => 0

Acceptance probability decomposes over commitments.

theorem CatCrypt.Crypto.ForkingLemma.forkSuccProb_decompose {X C R Y : Type} [Fintype R] [Nonempty R] [DecidableEq R] (A : ForkableAdversary X C R Y) (x : X) (accept : Y → Bool) : forkSuccProb A x accept = ∑' (p : Option (C × Core.Heap)), (A.coins x Core.Heap.empty) p * match p with | some (c, h') => condForkProb A x accept c h' | none => 0

Fork success probability decomposes over commitments.

theorem CatCrypt.Crypto.ForkingLemma.fork_success_ge {X C R Y : Type} [Fintype R] [Nonempty R] [DecidableEq R] (A : ForkableAdversary X C R Y) (x : X) (accept : Y → Bool) : forkSuccProb A x accept ≥ acceptProb A x accept ^ 2 - acceptProb A x accept / ↑(Fintype.card R)

Main forking lemma (q = 1): the fork success probability is at least acc² - acc/|R|.

This is the Bellare-Neven bound specialized to a single oracle query: Pr[fork succeeds] ≥ acc · (acc - 1/|R|) = acc² - acc/|R|

where acc is the adversary's acceptance probability and |R| is the size of the oracle response space.