The general forking lemma

An algorithm A gets coins s, drawn from a distribution, and q answers h : Fin q → H, drawn independently and uniformly from a finite set H, and outputs an optional index j : Fin q together with a result. The forking algorithm runs A once; if it outputs an index j, it runs A again on the same coins and the same answers before j, with fresh answers from j on (splice). It succeeds when the second run outputs the same index j and the two answers at j differ, and it returns both results.

The general forking lemma of Bellare and Neven ([BN06], Lemma 1) bounds the success probability frk of forking by the acceptance probability acc of one run: acc ^ 2 / q - acc / |H| ≤ frk (sq_div_sub_le_fork), and consequently acc ≤ q / |H| + √(q · frk) (le_add_sqrt_fork). For each index j this is the rewinding lemma (Rewinding.sq_sub_le_twice), with the coins and the answers before j as the first stage, the answer at j as the challenge and the answers after j as fresh randomness of the second stage; summing over j loses the factor q by the Cauchy–Schwarz inequality. Boneh and Shoup prove the same bound for r-impersonation adversaries ([BS23], Lemma 19.8).

The algorithm is deterministic given its coins and answers, which is the form forking needs: the second run reuses the coins. The statements are exact; no efficiency is involved.

Main definitions

• Cslib.Probability.Forking.splice: answers from one vector before an index, another from it on.
• Cslib.Probability.Forking.accept: run once and accept when an index is output.
• Cslib.Probability.Forking.fork: the forking algorithm.

Main results

• Cslib.Probability.Forking.sq_div_sub_le_fork: acc ^ 2 / q - acc / |H| ≤ frk.
• Cslib.Probability.Forking.le_add_sqrt_fork: acc ≤ q / |H| + √(q · frk).
• Cslib.Probability.Forking.mem_support_fork: what a successful fork returns.

References

• M. Bellare, G. Neven, Multi-Signatures in the Plain Public-Key Model and a General Forking Lemma, Lemma 1.
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Lemma 19.8.

def Cslib.Probability.Forking.splice {H : Type} {q : ℕ} (j : Fin q) (h h' : Fin q → H) : Fin q → H

The answers of h before the index j and those of h' from j on.

noncomputable def Cslib.Probability.Forking.accept {S H β : Type} {q : ℕ} [Fintype H] [Nonempty H] (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) : PMF Bool

One run: draw coins and uniform answers, and accept when A outputs an index.

noncomputable def Cslib.Probability.Forking.fork {S H β : Type} {q : ℕ} [Fintype H] [Nonempty H] [DecidableEq H] (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) : PMF (Option (Fin q × β × β))

The forking algorithm ([BN06]): run A on coins s and answers h; if it outputs an index j, rerun it on s and on splice j h h' for fresh answers h', and succeed with both results when the rerun outputs j too and h j ≠ h' j.

Splitting the answers at an index

One index

Summing over the indices

The forking lemma

theorem Cslib.Probability.Forking.sq_div_sub_le_fork {S H β : Type} {q : ℕ} [Fintype H] [Nonempty H] [DecidableEq H] (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) : ((accept first A) true).toReal ^ 2 / ↑q - ((accept first A) true).toReal / ↑(Fintype.card H) ≤ ((PMF.map Option.isSome (fork first A)) true).toReal

The general forking lemma ([BN06], Lemma 1): forking succeeds with probability at least acc ^ 2 / q - acc / |H|, where acc is the probability that one run outputs an index.

theorem Cslib.Probability.Forking.le_add_sqrt_fork {S H β : Type} {q : ℕ} [Fintype H] [Nonempty H] [DecidableEq H] (first : PMF S) (A : S → (Fin q → H) → Option (Fin q) × β) : ((accept first A) true).toReal ≤ ↑q / ↑(Fintype.card H) + √(↑q * ((PMF.map Option.isSome (fork first A)) true).toReal)

The forking lemma solved for the acceptance probability: acc ≤ q / |H| + √(q · frk).

theorem Cslib.Probability.Forking.mem_support_fork {S H β : Type} {q : ℕ} [Fintype H] [Nonempty H] [DecidableEq H] {first : PMF S} {A : S → (Fin q → H) → Option (Fin q) × β} {j : Fin q} {out out' : β} (hfork : some (j, out, out') ∈ (fork first A).support) : ∃ s ∈ first.support, ∃ (h : Fin q → H) (h' : Fin q → H), (∀ i < j, h i = h' i) ∧ h j ≠ h' j ∧ A s h = (some j, out) ∧ A s h' = (some j, out')

A successful fork comes from one coin sample and two answer vectors that agree before the returned index j and differ at it, on both of which A outputs j.