Tree-forking lemma for multi-round public-coin interactions

This file states and proves the tree-extraction lemma of (k₁,…,k_μ)-special soundness for μ-round public-coin interactions over SPComp, with the knowledge error of Attema–Cramer–Kohl.

Model

A round (Round) has a finite nonempty challenge set C, a prover message type M and an arity k. A deterministic prover strategy (Strategy Y rs) for the round list rs sends a message at each round and, after the last challenge, an output Y. A probabilistic prover is P : SPComp (Strategy Y rs): a distribution over strategies, which is the random-tape view of a prover that the rewinding extractor controls. The verifier is a predicate V : Transcript rs → Y → Bool on the full transcript and the final output.

A transcript tree (Tree Y rs) of arity (k₁,…,k_μ) stores, at a node of round i, the prover message and kᵢ children labelled by challenges. It is accepting (Tree.Accepting) when sibling challenges are pairwise distinct and every leaf satisfies V on its root-to-leaf transcript, and it is consistent with a strategy (Tree.Consistent) when every message and output is the strategy's response to the challenges on its path.

Extractor

extract is the rewinding extractor on a strategy: at a node of round i it rewinds the prover once for each challenge in Cᵢ (at most |Cᵢ| rewinds per node, so at most ∏ |Cᵢ| prover runs in total), keeps the challenges whose subtree extraction succeeds, and returns a node built from the first kᵢ of them when there are at least kᵢ. treeExtractor P runs it on a strategy drawn from P. Every output tree is accepting and consistent (extract_sound).

Main results

• knowledgeError rs = 1 − ∏ᵢ (1 − (kᵢ − 1)/|Cᵢ|).
• runAccept_le — for a deterministic strategy, the acceptance probability over uniform challenges is at most κ + (1 − κ)·[extract succeeds].
• acceptProb_le — for a probabilistic prover accepted with probability ε, ε ≤ κ + (1 − κ)·Pr[treeExtractor outputs a tree].
• acceptProb_sub_le_mul / acceptProb_sub_le — ε − κ ≤ (1 − κ)·Pr[tree] ≤ Pr[tree].
• knowledgeError_lt_one — κ < 1 when every kᵢ ≤ |Cᵢ|; extractProb_const_accept — a prover accepted on every challenge yields a tree with probability at least 1 − κ.
• forkSuccProb_le_extractProb — for μ = 1 and k = 2, the two-branch forking experiment ForkingLemma.forkSuccProb succeeds with probability at most the tree extractor's, so fork_success_ge gives a second lower bound acc² − acc/|R| on the same extraction probability (single_round_extract_ge).

References

• [Attema, Cramer, Kohl, A Compressed Σ-Protocol Theory for Lattices, CRYPTO 2021]
• [Attema, Fehr, Klooß, Fiat–Shamir Transformation of Multi-Round Interactive Proofs, TCC 2022]
• [Bootle, Cerulli, Chaidos, Groth, Petit, Efficient Zero-Knowledge Arguments for Arithmetic Circuits in the Discrete Log Setting, EUROCRYPT 2016]

Rounds, transcripts, strategies and trees

structure CatCrypt.Crypto.TreeForking.Round : Type 1

One round of a public-coin interaction: the prover sends a message of type M, the verifier answers with a uniform challenge from the finite nonempty set C, and special soundness asks for k distinct challenges at this round.

• C : Type

  Challenge set.

• M : Type

  Prover message type.

• k : ℕ

  Arity of the transcript tree at this round.

• fintype : Fintype self.C
• nonempty : Nonempty self.C

def CatCrypt.Crypto.TreeForking.Transcript : List Round → Type

Full transcript of the rounds rs: one message and one challenge per round.

Equations

• CatCrypt.Crypto.TreeForking.Transcript [] = Unit
• CatCrypt.Crypto.TreeForking.Transcript (r :: rs) = (r.M × r.C × CatCrypt.Crypto.TreeForking.Transcript rs)

def CatCrypt.Crypto.TreeForking.Strategy (Y : Type) : List Round → Type

Deterministic prover strategy for the rounds rs with final output Y: a message at each round and a continuation per challenge.

Equations

• CatCrypt.Crypto.TreeForking.Strategy Y [] = Y
• CatCrypt.Crypto.TreeForking.Strategy Y (r :: rs) = (r.M × (r.C → CatCrypt.Crypto.TreeForking.Strategy Y rs))

def CatCrypt.Crypto.TreeForking.Tree (Y : Type) : List Round → Type

Transcript tree of arity (k₁,…,k_μ): a node of round r holds the prover message and r.k children, each labelled by a challenge.

Equations

• CatCrypt.Crypto.TreeForking.Tree Y [] = Y
• CatCrypt.Crypto.TreeForking.Tree Y (r :: rs) = (r.M × (Fin r.k → r.C × CatCrypt.Crypto.TreeForking.Tree Y rs))

def CatCrypt.Crypto.TreeForking.Tree.Accepting {Y : Type} (rs : List Round) : (Transcript rs → Y → Bool) → Tree Y rs → Prop

Acceptance of a transcript tree under the verifier V: sibling challenges are pairwise distinct and every leaf output is accepted on its root-to-leaf transcript.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Crypto.TreeForking.Tree.Accepting [] V T = (V () T = true)

def CatCrypt.Crypto.TreeForking.Tree.Consistent {Y : Type} (rs : List Round) : Tree Y rs → Strategy Y rs → Prop

Consistency of a transcript tree with a strategy: each message and output in the tree is the strategy's response to the challenges on its path.

Equations

• CatCrypt.Crypto.TreeForking.Tree.Consistent [] T s = (T = s)
• CatCrypt.Crypto.TreeForking.Tree.Consistent (head :: rs) T s = (T.1 = s.1 ∧ ∀ (j : Fin head.k), CatCrypt.Crypto.TreeForking.Tree.Consistent rs (T.2 j).2 (s.2 (T.2 j).1))

The honest run and the extractor

noncomputable def CatCrypt.Crypto.TreeForking.runAccept {Y : Type} (rs : List Round) : (Transcript rs → Y → Bool) → Strategy Y rs → Core.SPComp Bool

One run of the interaction between a deterministic strategy and the verifier: uniform challenges at each round, then the output of V on the transcript.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Crypto.TreeForking.runAccept [] V s = CatCrypt.Core.SPComp.pure (V () s)

noncomputable def CatCrypt.Crypto.TreeForking.extract {Y : Type} (rs : List Round) : (Transcript rs → Y → Bool) → Strategy Y rs → Option (Tree Y rs)

The rewinding tree extractor on a deterministic strategy. At a node of round r it runs the sub-extractor once for every challenge in r.C, and succeeds with the first r.k challenges (in the order of Finset.equivFin) whose sub-extraction succeeds, when there are at least r.k of them.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Crypto.TreeForking.extract [] V s = if V () s = true then some s else none

theorem CatCrypt.Crypto.TreeForking.extract_nil_isSome {Y : Type} (V : Transcript [] → Y → Bool) (s : Strategy Y []) : (extract [] V s).isSome = V () s

Extraction at a leaf succeeds exactly when V accepts.

theorem CatCrypt.Crypto.TreeForking.extract_cons_isSome {Y : Type} (r : Round) (rs : List Round) (V : Transcript (r :: rs) → Y → Bool) (s : Strategy Y (r :: rs)) : (extract (r :: rs) V s).isSome = true ↔ r.k ≤ {c : r.C | (extract rs (fun (t : Transcript rs) (y : Y) => V (s.1, c, t) y) (s.2 c)).isSome = true}.card

Extraction at a node succeeds exactly when at least r.k challenges have a successful sub-extraction.

theorem CatCrypt.Crypto.TreeForking.extract_sound {Y : Type} (rs : List Round) (V : Transcript rs → Y → Bool) (s : Strategy Y rs) (T : Tree Y rs) : extract rs V s = some T → Tree.Accepting rs V T ∧ Tree.Consistent rs T s

Every tree output by the extractor is accepting and consistent with the strategy.

Knowledge error

noncomputable def CatCrypt.Crypto.TreeForking.Round.survival (r : Round) : ENNReal

Per-round survival factor 1 − (k − 1)/|C|.

Equations

• r.survival = 1 - ↑(r.k - 1) / ↑(Fintype.card r.C)

noncomputable def CatCrypt.Crypto.TreeForking.survival (rs : List Round) : ENNReal

The product ∏ᵢ (1 − (kᵢ − 1)/|Cᵢ|).

Equations

• CatCrypt.Crypto.TreeForking.survival rs = (List.map CatCrypt.Crypto.TreeForking.Round.survival rs).prod

noncomputable def CatCrypt.Crypto.TreeForking.knowledgeError (rs : List Round) : ENNReal

The Attema–Cramer–Kohl knowledge error κ = 1 − ∏ᵢ (1 − (kᵢ − 1)/|Cᵢ|).

Equations

• CatCrypt.Crypto.TreeForking.knowledgeError rs = 1 - CatCrypt.Crypto.TreeForking.survival rs

theorem CatCrypt.Crypto.TreeForking.Round.survival_le_one (r : Round) : r.survival ≤ 1

theorem CatCrypt.Crypto.TreeForking.survival_nil : survival [] = 1

theorem CatCrypt.Crypto.TreeForking.survival_cons (r : Round) (rs : List Round) : survival (r :: rs) = r.survival * survival rs

theorem CatCrypt.Crypto.TreeForking.survival_le_one (rs : List Round) : survival rs ≤ 1

theorem CatCrypt.Crypto.TreeForking.knowledgeError_add_survival (rs : List Round) : knowledgeError rs + survival rs = 1

theorem CatCrypt.Crypto.TreeForking.knowledgeError_le_one (rs : List Round) : knowledgeError rs ≤ 1

theorem CatCrypt.Crypto.TreeForking.knowledgeError_lt_one (rs : List Round) (hk : ∀ r ∈ rs, r.k ≤ Fintype.card r.C) : knowledgeError rs < 1

κ < 1 when every arity is at most the size of its challenge set.

theorem CatCrypt.Crypto.TreeForking.knowledgeError_single_two (C : Type) [Fintype C] [Nonempty C] (M : Type) : knowledgeError [{ C := C, M := M, k := 2, fintype := inst✝, nonempty := inst✝¹ }] = (↑(Fintype.card C))⁻¹

For a single round of arity 2 the knowledge error is 1/|C|.

The deterministic bound

theorem CatCrypt.Crypto.TreeForking.sum_inv_mul_indicator (C : Type) [Fintype C] [Nonempty C] (p : C → Bool) : (∑ c : C, (↑(Fintype.card C))⁻¹ * if p c = true then 1 else 0) = ↑{c : C | p c = true}.card / ↑(Fintype.card C)

Averaging a bound over a uniform challenge: ∑_c |C|⁻¹ · [c ∈ S] = |S|/|C|.

theorem CatCrypt.Crypto.TreeForking.runAccept_le {Y : Type} (rs : List Round) (V : Transcript rs → Y → Bool) (s : Strategy Y rs) (h₀ : Core.Heap) : prTrue (runAccept rs V s) h₀ ≤ knowledgeError rs + survival rs * if (extract rs V s).isSome = true then 1 else 0

Deterministic tree-extraction bound. For every strategy, the probability that V accepts over uniform challenges is at most κ + (1 − κ) · [extract succeeds].

The probabilistic bound

theorem CatCrypt.Crypto.TreeForking.prTrue_bind_le_affine {α : Type} (c : Core.SPComp α) (k₁ k₂ : α → Core.SPComp Bool) (κ σ : ENNReal) (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₀

Affine monotonicity of prTrue under bind: a pointwise bound prTrue (k₁ a) ≤ κ + σ · prTrue (k₂ a) averages over the first computation.

noncomputable def CatCrypt.Crypto.TreeForking.acceptProb {Y : Type} (rs : List Round) (P : Core.SPComp (Strategy Y rs)) (V : Transcript rs → Y → Bool) (h₀ : Core.Heap) : ENNReal

Acceptance probability of a probabilistic prover P (a distribution over strategies) against the verifier V.

Equations

• CatCrypt.Crypto.TreeForking.acceptProb rs P V h₀ = CatCrypt.Crypto.prTrue (P.bind (CatCrypt.Crypto.TreeForking.runAccept rs V)) h₀

noncomputable def CatCrypt.Crypto.TreeForking.treeExtractor {Y : Type} (rs : List Round) (P : Core.SPComp (Strategy Y rs)) (V : Transcript rs → Y → Bool) : Core.SPComp (Option (Tree Y rs))

The tree extractor for a probabilistic prover: draw a strategy from P and run the rewinding extractor extract on it.

Equations

• CatCrypt.Crypto.TreeForking.treeExtractor rs P V = P.bind fun (s : CatCrypt.Crypto.TreeForking.Strategy Y rs) => CatCrypt.Core.SPComp.pure (CatCrypt.Crypto.TreeForking.extract rs V s)

noncomputable def CatCrypt.Crypto.TreeForking.extractProb {Y : Type} (rs : List Round) (P : Core.SPComp (Strategy Y rs)) (V : Transcript rs → Y → Bool) (h₀ : Core.Heap) : ENNReal

Probability that the tree extractor outputs a tree.

Equations

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

theorem CatCrypt.Crypto.TreeForking.extractProb_eq {Y : Type} (rs : List Round) (P : Core.SPComp (Strategy Y rs)) (V : Transcript rs → Y → Bool) (h₀ : Core.Heap) : extractProb rs P V h₀ = prTrue (P.bind fun (s : Strategy Y rs) => Core.SPComp.pure (extract rs V s).isSome) h₀

theorem CatCrypt.Crypto.TreeForking.acceptProb_le {Y : Type} (rs : List Round) (P : Core.SPComp (Strategy Y rs)) (V : Transcript rs → Y → Bool) (h₀ : Core.Heap) : acceptProb rs P V h₀ ≤ knowledgeError rs + survival rs * extractProb rs P V h₀

Tree-forking lemma. A prover accepted with probability ε yields, through the rewinding extractor, an accepting (k₁,…,k_μ)-tree consistent with its strategy with probability p satisfying ε ≤ κ + (1 − κ) · p, where κ = knowledgeError rs and 1 − κ = survival rs.

theorem CatCrypt.Crypto.TreeForking.acceptProb_sub_le_mul {Y : Type} (rs : List Round) (P : Core.SPComp (Strategy Y rs)) (V : Transcript rs → Y → Bool) (h₀ : Core.Heap) : acceptProb rs P V h₀ - knowledgeError rs ≤ survival rs * extractProb rs P V h₀

ε − κ ≤ (1 − κ) · Pr[tree extracted].

theorem CatCrypt.Crypto.TreeForking.acceptProb_sub_le {Y : Type} (rs : List Round) (P : Core.SPComp (Strategy Y rs)) (V : Transcript rs → Y → Bool) (h₀ : Core.Heap) : acceptProb rs P V h₀ - knowledgeError rs ≤ extractProb rs P V h₀

ε − κ ≤ Pr[tree extracted].

Satisfiability

theorem CatCrypt.Crypto.TreeForking.runAccept_const_true {Y : Type} (rs : List Round) (s : Strategy Y rs) (h₀ : Core.Heap) : prTrue (runAccept rs (fun (x : Transcript rs) (x_1 : Y) => true) s) h₀ = 1

A run against the verifier that accepts every transcript succeeds with probability 1.

theorem CatCrypt.Crypto.TreeForking.one_sub_knowledgeError_le_extractProb {Y : Type} (rs : List Round) (P : Core.SPComp (Strategy Y rs)) (V : Transcript rs → Y → Bool) (h₀ : Core.Heap) (hacc : acceptProb rs P V h₀ = 1) : 1 - knowledgeError rs ≤ extractProb rs P V h₀

A prover accepted with probability 1 yields a tree with probability at least 1 − κ.

theorem CatCrypt.Crypto.TreeForking.extractProb_const_accept {Y : Type} (rs : List Round) (s : Strategy Y rs) (h₀ : Core.Heap) : 1 - knowledgeError rs ≤ extractProb rs (Core.SPComp.pure s) (fun (x : Transcript rs) (x_1 : Y) => true) h₀

A deterministic prover run against the always-accepting verifier yields a tree with probability at least 1 − κ, which is positive when every kᵢ ≤ |Cᵢ|.

theorem CatCrypt.Crypto.TreeForking.extractProb_const_accept_pos {Y : Type} (rs : List Round) (s : Strategy Y rs) (h₀ : Core.Heap) (hk : ∀ r ∈ rs, r.k ≤ Fintype.card r.C) : 0 < extractProb rs (Core.SPComp.pure s) (fun (x : Transcript rs) (x_1 : Y) => true) h₀

The single-round, arity-2 case

def CatCrypt.Crypto.TreeForking.forkRound (R : Type) [Fintype R] [Nonempty R] : Round

The single round of the two-branch forking lemma: challenge set R, no prover message (the commitment is part of the strategy draw), arity 2.

Equations

• CatCrypt.Crypto.TreeForking.forkRound R = { C := R, M := Unit, k := 2, fintype := inst✝¹, nonempty := inst✝ }

theorem CatCrypt.Crypto.TreeForking.knowledgeError_forkRound {R : Type} [Fintype R] [Nonempty R] : knowledgeError [forkRound R] = (↑(Fintype.card R))⁻¹

def CatCrypt.Crypto.TreeForking.forkStrategy {Y R : Type} [Fintype R] [Nonempty R] (f : R → Y) : Strategy Y [forkRound R]

The single-round strategy answering challenge e with f e.

Equations

• CatCrypt.Crypto.TreeForking.forkStrategy f = ((), f)

noncomputable def CatCrypt.Crypto.TreeForking.forkProver {Y X Cm R : Type} [Fintype R] [Nonempty R] (A : ForkingLemma.ForkableAdversary X Cm R Y) (x : X) : Core.SPComp (Strategy Y [forkRound R])

A ForkableAdversary as a probabilistic single-round prover: the commitment phase draws the strategy e ↦ respond x c e.

Equations

• CatCrypt.Crypto.TreeForking.forkProver A x = (A.coins x).bind fun (c : Cm) => CatCrypt.Core.SPComp.pure (CatCrypt.Crypto.TreeForking.forkStrategy fun (e : R) => A.respond x c e)

theorem CatCrypt.Crypto.TreeForking.acceptProb_forkProver {Y X Cm R : Type} [Fintype R] [Nonempty R] (A : ForkingLemma.ForkableAdversary X Cm R Y) (x : X) (accept : Y → Bool) : acceptProb [forkRound R] (forkProver A x) (fun (x : Transcript [forkRound R]) (y : Y) => accept y) Core.Heap.empty = ForkingLemma.acceptProb A x accept

theorem CatCrypt.Crypto.TreeForking.forkSuccProb_le_extractProb {Y X Cm R : Type} [Fintype R] [Nonempty R] [DecidableEq R] (A : ForkingLemma.ForkableAdversary X Cm R Y) (x : X) (accept : Y → Bool) : ForkingLemma.forkSuccProb A x accept ≤ extractProb [forkRound R] (forkProver A x) (fun (x : Transcript [forkRound R]) (y : Y) => accept y) Core.Heap.empty

The two-branch fork succeeds with probability at most the tree extractor's on forkProver: a fork success exhibits two distinct accepting challenges for the drawn commitment.

theorem CatCrypt.Crypto.TreeForking.single_round_extract_ge {Y X Cm R : Type} [Fintype R] [Nonempty R] [DecidableEq R] (A : ForkingLemma.ForkableAdversary X Cm R Y) (x : X) (accept : Y → Bool) : ForkingLemma.acceptProb A x accept - (↑(Fintype.card R))⁻¹ ≤ extractProb [forkRound R] (forkProver A x) (fun (x : Transcript [forkRound R]) (y : Y) => accept y) Core.Heap.empty ∧ ForkingLemma.acceptProb A x accept ^ 2 - ForkingLemma.acceptProb A x accept / ↑(Fintype.card R) ≤ extractProb [forkRound R] (forkProver A x) (fun (x : Transcript [forkRound R]) (y : Y) => accept y) Core.Heap.empty

For μ = 1 and k = 2 the tree-extraction probability of forkProver is bounded below both by acc − 1/|R| (acceptProb_sub_le) and by the forking-lemma bound acc² − acc/|R| (fork_success_ge).