Fischlin Transform: Online Extraction / Knowledge Soundness

Online (straight-line) knowledge soundness for the Fischlin transform: the extractor onlineExtract observes the prover's random-oracle queries, and the extraction failure probability is bounded via a supermartingale potential argument, culminating in knowledgeSoundness.

Online Extraction / Knowledge Soundness

def Fischlin.ROQueryBound {Stmt Commit Chal Resp : Type} (ρ b : ℕ) (M : Type) {α : Type} (oa : OracleComp (unifSpec + fischlinROSpec Stmt Commit Chal Resp ρ b M) α) (Q : ℕ) : Prop

Structural query bound: the computation makes at most Q total hash oracle queries (Sum.inr queries), with no restriction on unifSpec queries (Sum.inl).

Defined as the generic predicate-targeted query bound IsQueryBoundP with the predicate selecting the right (random-oracle) component of the index sum.

structure Fischlin.KnowledgeSoundnessAdv {Stmt Commit Chal Resp : Type} (ρ b : ℕ) (M : Type) : Type

A cheating prover (knowledge soundness adversary) for the Fischlin transform. The adversary receives a statement and message, has access to both the random oracle and internal randomness (unifSpec), and attempts to produce a valid Fischlin proof without knowing the witness.

The Σ-protocol σ is not referenced in the structure itself (only in the extraction and verification steps of the experiment), so it enters the theorem statements via hypotheses like σ.SpeciallySound.

• run : Stmt → M → OracleComp (unifSpec + fischlinROSpec Stmt Commit Chal Resp ρ b M) (FischlinProof Commit Chal Resp ρ)

noncomputable def Fischlin.onlineExtract {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [DecidableEq Stmt] [DecidableEq Commit] [DecidableEq Chal] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (ρ b : ℕ) (M : Type) (x : Stmt) (π : FischlinProof Commit Chal Resp ρ) (log : (fischlinROSpec Stmt Commit Chal Resp ρ b M).QueryLog) : ProbComp (Option Wit)

Online extractor for the Fischlin transform (Fischlin 2005, Construction 2).

Given statement x, a proof π, and the log of all hash oracle queries made by the prover, the extractor searches for two accepting transcripts at the same commitment with different challenges, then invokes the Σ-protocol's extract function. Returns none if no such collision is found in the log.

The key property enabling this extractor is UniqueResponses: given the same (statement, commitment, challenge), there is at most one valid response. So finding a second valid query at a different challenge gives a proper input pair for the Σ-protocol extractor.

noncomputable def Fischlin.knowledgeSoundnessError (Q ρ b S : ℕ) : ENNReal

Soundness error bound for the Fischlin transform (Fischlin 2005, Theorem 2).

For Q total hash oracle queries, ρ repetitions, b-bit hashes, and max sum S: the error is (Q + 1) · (S + 1) · C(S + ρ - 1, ρ - 1) / 2^(bρ).

For S = 0 this simplifies to (Q + 1) / 2^(bρ). The intended regime is 0 < ρ; theorem statements below make that explicit.

noncomputable def Fischlin.knowledgeSoundnessExp {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [DecidableEq Stmt] [DecidableEq Commit] [DecidableEq Chal] [DecidableEq Resp] [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (ρ b S : ℕ) (M : Type) [DecidableEq M] (prover : Stmt → M → OracleComp (unifSpec + fischlinROSpec Stmt Commit Chal Resp ρ b M) (FischlinProof Commit Chal Resp ρ)) (x : Stmt) (msg : M) : ProbComp Bool

The knowledge soundness experiment for the Fischlin transform.

Runs a cheating prover with a logged random oracle, then checks:

1. Whether the Fischlin verifier accepts the produced proof.
2. Whether the online extractor returns a witness satisfying the relation.

Returns true (the "bad event") when verification succeeds but the extracted output is either none or an invalid witness.

The prover argument is the raw function rather than KnowledgeSoundnessAdv to keep type inference tractable.

def Fischlin.smallSumCount (ρ b S : ℕ) : ℕ

The number of hash-value tuples v : Fin ρ → Fin (2^b) whose entries sum to at most S.

This counts the "small-sum" verifier-accepting hash assignments: a Fischlin proof is accepted only when ∑ᵢ H(…,ωᵢ,respᵢ) ≤ S, so this finite set is the target the prover's fresh random-oracle answers must hit. It is bounded by (S+1)·C(S+ρ-1, ρ-1) (stars-and-bars).

Knowledge-Soundness Assembly: Classifier Instantiation

The supermartingale induction main_induction_gen_init is instantiated on the Fischlin random-oracle records: a record is relevant (ksRelevant) when it carries the proof's statement/message tags and σ-verifies against the commitment stored at its repetition index in its own commitment list; cells are indexed by (comList, rep); and a commitment-list key dies (ksDead) once the cache holds two relevant records in the same cell with distinct challenges — exactly the event in which the online extractor succeeds.

theorem Fischlin.knowledgeSoundness {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [DecidableEq Stmt] [DecidableEq Commit] [DecidableEq Chal] [DecidableEq Resp] [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (ρ b S : ℕ) (M : Type) [DecidableEq M] (hss : σ.SpeciallySound) (hur : σ.UniqueResponses) (adv : KnowledgeSoundnessAdv ρ b M) (Q : ℕ) (hρ : 0 < ρ) (hQ : ∀ (x : Stmt) (msg : M), ROQueryBound ρ b M (adv.run x msg) Q) (x : Stmt) (msg : M) : Pr[= true | knowledgeSoundnessExp σ hr ρ b S M adv.run x msg] ≤ knowledgeSoundnessError Q ρ b S

Knowledge soundness of the Fischlin transform via online (straight-line) extraction (Fischlin 2005, Theorem 2).

If the Σ-protocol is specially sound with unique responses, then for any cheating prover making at most Q hash queries, the probability that the verifier accepts but the online extractor fails to recover a valid witness is at most (Q + 1) · (S + 1) · C(S + ρ - 1, ρ - 1) / 2^(bρ).

Unlike the Fiat-Shamir transform, this extraction is straight-line (no rewinding), which enables a tight security reduction.

EUF-CMA Security

A tight EUF-CMA corollary for the Fischlin signature scheme requires an explicit simulation of signing queries inside a hard-relation experiment. The previous placeholder theorem overclaimed by bounding forgery probability solely by the knowledge-soundness error, so we intentionally leave that corollary unstated until the signing-simulation reduction is formalized.