General Forking Lemma (q-query)

Generalizes the forking lemma from ForkingLemma.lean (q = 1) to adversaries making q >= 1 oracle queries, following Bellare-Neven (CCS 2006, Lemma 1).

Model

A q-query adversary decomposes into:

1. Coins phase: probabilistic, produces commitment c
2. Respond phase: deterministic, given c and all q oracle responses (modeled as Fin q -> R), produces (j, y) where j identifies the relevant query

Reduction

For each guess I : Fin q, we build a 1-query ForkableAdversary that absorbs all q oracle responses into its coins phase and uses Function.update to replace the I-th response with the single oracle challenge. The key distribution lemma (sample_update_eq_sample) shows this replacement preserves the uniform distribution.

Results

• qFork_success_ge_simple -- simple bound: average fork >= acc^2 - acc/|R|
• bellare_neven_aggregation -- abstract Cauchy-Schwarz aggregation step
• sum_acceptAtGuess_eq -- partition of probability: sum accI = acc
• qFork_success_ge -- Bellare-Neven: sum of indexed forks >= acc^2/q - acc/|R|

References

• [Bellare, Neven, Multi-signatures in the plain public-key model, CCS 2006]

q-Query Adversary Model

structure CatCrypt.Crypto.GeneralForkingLemma.QForkableAdversary (X C R Y : Type) (q : ℕ) : Type

A q-query adversary for the ROM forking lemma.

• coins : X → Core.SPComp C

  Probabilistic commitment phase.

• respond : X → C → (Fin q → R) → Fin q × Y

  Deterministic response: given all q oracle responses, produce (index, output).

noncomputable def CatCrypt.Crypto.GeneralForkingLemma.qAcceptProb {X C R Y : Type} {q : ℕ} [Fintype R] [Nonempty R] [Fintype (Fin q → R)] [Nonempty (Fin q → R)] (A : QForkableAdversary X C R Y q) (x : X) (accept : Fin q × Y → Bool) : ENNReal

Acceptance probability of a q-query adversary.

Equations

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

Swap-at-j Equivalence

def CatCrypt.Crypto.GeneralForkingLemma.swapAt {R : Type} {q : ℕ} [DecidableEq (Fin q)] (j : Fin q) : (Fin q → R) × R → (Fin q → R) × R

The swap-at-j involution: (f, e) ↦ (Function.update f j e, f j).

Equations

• CatCrypt.Crypto.GeneralForkingLemma.swapAt j (f, e) = (Function.update f j e, f j)

theorem CatCrypt.Crypto.GeneralForkingLemma.swapAt_involutive {R : Type} {q : ℕ} [DecidableEq (Fin q)] (j : Fin q) : Function.Involutive (swapAt j)

noncomputable def CatCrypt.Crypto.GeneralForkingLemma.swapAtEquiv {R : Type} {q : ℕ} [DecidableEq (Fin q)] (j : Fin q) : (Fin q → R) × R ≃ (Fin q → R) × R

Equations

• CatCrypt.Crypto.GeneralForkingLemma.swapAtEquiv j = Function.Involutive.toPerm (CatCrypt.Crypto.GeneralForkingLemma.swapAt j) ⋯

@[simp]

theorem CatCrypt.Crypto.GeneralForkingLemma.swapAtEquiv_apply {R : Type} {q : ℕ} [DecidableEq (Fin q)] (j : Fin q) (p : (Fin q → R) × R) : (swapAtEquiv j) p = swapAt j p

Sample-Update Distribution Lemma

theorem CatCrypt.Crypto.GeneralForkingLemma.sample_update_eq_sample {R : Type} {q : ℕ} [Fintype R] [Nonempty R] [DecidableEq (Fin q)] [Fintype (Fin q → R)] [Nonempty (Fin q → R)] (j : Fin q) {β : Type} (k : (Fin q → R) → Core.SPComp β) : ((Core.SPComp.sample (Fin q → R)).bind fun (f : Fin q → R) => (Core.SPComp.sample R).bind fun (e : R) => k (Function.update f j e)) = (Core.SPComp.sample (Fin q → R)).bind k

Sampling f : Fin q → R and e : R uniformly, then applying Function.update f j e, gives the same distribution as sampling g : Fin q → R uniformly.

Guess Reduction

noncomputable def CatCrypt.Crypto.GeneralForkingLemma.guessReduction {X C R Y : Type} {q : ℕ} [Fintype R] [Nonempty R] [DecidableEq (Fin q)] [Fintype (Fin q → R)] [Nonempty (Fin q → R)] (A : QForkableAdversary X C R Y q) (I : Fin q) : ForkingLemma.ForkableAdversary X (C × (Fin q → R)) R (Fin q × Y)

Given guess I, create a 1-query adversary by absorbing all q oracle responses into the coins phase and using Function.update at position I.

Equations

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

def CatCrypt.Crypto.GeneralForkingLemma.acceptAtGuess {Y : Type} {q : ℕ} (accept : Fin q × Y → Bool) (I : Fin q) : Fin q × Y → Bool

Acceptance restricted to outputs whose index matches the guess.

Equations

• CatCrypt.Crypto.GeneralForkingLemma.acceptAtGuess accept I (j, y) = (decide (j = I) && accept (j, y))

theorem CatCrypt.Crypto.GeneralForkingLemma.acceptProb_guessReduction {X C R Y : Type} {q : ℕ} [Fintype R] [Nonempty R] [DecidableEq (Fin q)] [DecidableEq R] [Fintype (Fin q → R)] [Nonempty (Fin q → R)] (A : QForkableAdversary X C R Y q) (x : X) (I : Fin q) (accept : Fin q × Y → Bool) : ForkingLemma.acceptProb (guessReduction A I) x accept = qAcceptProb A x accept

Each reduced adversary (full accept) has the same acceptance probability as the q-query adversary, by sample_update_eq_sample.

Simple q-Forking Bound (Non-Indexed)

noncomputable def CatCrypt.Crypto.GeneralForkingLemma.qForkSuccProbSimple {X C R Y : Type} {q : ℕ} [Fintype R] [Nonempty R] [DecidableEq (Fin q)] [DecidableEq R] [Fintype (Fin q → R)] [Nonempty (Fin q → R)] (A : QForkableAdversary X C R Y q) (x : X) (accept : Fin q × Y → Bool) (_hq : 0 < q) : ENNReal

Equations

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

theorem CatCrypt.Crypto.GeneralForkingLemma.qFork_success_ge_simple {X C R Y : Type} {q : ℕ} [Fintype R] [Nonempty R] [DecidableEq (Fin q)] [DecidableEq R] [Fintype (Fin q → R)] [Nonempty (Fin q → R)] (A : QForkableAdversary X C R Y q) (x : X) (accept : Fin q × Y → Bool) (hq : 0 < q) : qForkSuccProbSimple A x accept hq ≥ qAcceptProb A x accept ^ 2 - qAcceptProb A x accept / ↑(Fintype.card R)

Simple bound: average fork success >= acc^2 - acc/|R|.

theorem CatCrypt.Crypto.GeneralForkingLemma.qFork_success_ge_existential {X C R Y : Type} {q : ℕ} [Fintype R] [Nonempty R] [DecidableEq (Fin q)] [DecidableEq R] [Fintype (Fin q → R)] [Nonempty (Fin q → R)] (A : QForkableAdversary X C R Y q) (x : X) (accept : Fin q × Y → Bool) (I : Fin q) : ForkingLemma.forkSuccProb (guessReduction A I) x accept ≥ qAcceptProb A x accept ^ 2 - qAcceptProb A x accept / ↑(Fintype.card R)

For every guess I, fork success >= acc^2 - acc/|R|.

Bellare-Neven Aggregation (Abstract)

theorem CatCrypt.Crypto.GeneralForkingLemma.bellare_neven_aggregation {q : ℕ} (hq : 0 < q) (a f : Fin q → ENNReal) (N : ENNReal) (h_per_j : ∀ (j : Fin q), f j ≥ a j ^ 2 - a j / N) : ∑ j : Fin q, f j ≥ (∑ j : Fin q, a j) ^ 2 / ↑q - (∑ j : Fin q, a j) / N

Bellare-Neven aggregation (Cauchy-Schwarz step).

Indexed Forking: Partition + Main Theorem

theorem CatCrypt.Crypto.GeneralForkingLemma.sum_acceptAtGuess_eq {X C R Y : Type} {q : ℕ} [Fintype R] [Nonempty R] [DecidableEq (Fin q)] [DecidableEq R] [Fintype (Fin q → R)] [Nonempty (Fin q → R)] (A : QForkableAdversary X C R Y q) (x : X) (accept : Fin q × Y → Bool) : ∑ I : Fin q, ForkingLemma.acceptProb (guessReduction A I) x (acceptAtGuess accept I) = qAcceptProb A x accept

Partition of probability: sum_I Pr[idx=I and accept] = Pr[accept].

noncomputable def CatCrypt.Crypto.GeneralForkingLemma.qForkSuccProb {X C R Y : Type} {q : ℕ} [Fintype R] [Nonempty R] [DecidableEq (Fin q)] [DecidableEq R] [Fintype (Fin q → R)] [Nonempty (Fin q → R)] (A : QForkableAdversary X C R Y q) (x : X) (accept : Fin q × Y → Bool) : ENNReal

Indexed q-forking success probability (sum over all guesses).

Equations

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

theorem CatCrypt.Crypto.GeneralForkingLemma.qFork_success_ge {X C R Y : Type} {q : ℕ} [Fintype R] [Nonempty R] [DecidableEq (Fin q)] [DecidableEq R] [Fintype (Fin q → R)] [Nonempty (Fin q → R)] (A : QForkableAdversary X C R Y q) (x : X) (accept : Fin q × Y → Bool) (hq : 0 < q) : qForkSuccProb A x accept ≥ qAcceptProb A x accept ^ 2 / ↑q - qAcceptProb A x accept / ↑(Fintype.card R)

General Forking Lemma (Bellare-Neven 2006): qForkSuccProb >= acc^2/q - acc/|R|.

Embedding q = 1

def CatCrypt.Crypto.GeneralForkingLemma.toQForkable {X C R Y : Type} (A : ForkingLemma.ForkableAdversary X C R Y) : QForkableAdversary X C R Y 1

Convert a 1-query adversary to q=1 form.

Equations

• CatCrypt.Crypto.GeneralForkingLemma.toQForkable A = { coins := A.coins, respond := fun (x : X) (c : C) (es : Fin 1 → R) => (0, A.respond x c (es 0)) }

theorem CatCrypt.Crypto.GeneralForkingLemma.q1_simplification (S N : ENNReal) : S ^ 2 / 1 - S / N = S ^ 2 - S / N

When q = 1, the bound simplifies to the original forking lemma bound.