Fischlin Transform

This file defines the Fischlin transform (CRYPTO 2005), which converts a Σ-protocol into a signature scheme (non-interactive proof of knowledge) in the random oracle model with online (straight-line) extraction.

Unlike the Fiat-Shamir transform, which requires a rewinding extractor (via the forking lemma), the Fischlin transform enables extraction by simply observing the prover's hash queries. This comes at the cost of a more complex prover that performs a "proof-of-work" search over the challenge space, and a slight completeness error.

Parameters

• ρ — number of parallel repetitions
• b — hash output bit-length (random oracle range is Fin (2^b))
• S — maximum allowed sum of hash values in a valid proof (paper notation)

References

• Marc Fischlin, "Communication-Efficient Non-Interactive Proofs of Knowledge with Online Extractors", CRYPTO 2005.

Type Definitions

structure FischlinROInput (Stmt Commit Chal Resp : Type) (ρ : ℕ) (M : Type) : Type

Input to the Fischlin random oracle. Defined as a structure rather than a nested product to give fast DecidableEq synthesis (avoiding deep product-type unfolding).

• stmt : Stmt
• msg : M
• comList : List Commit
• rep : Fin ρ
• chal : Chal
• resp : Resp

@[implicit_reducible]

instance instDecidableEqFischlinROInput {Stmt✝ Commit✝ Chal✝ Resp✝ : Type} {ρ✝ : ℕ} {M✝ : Type} [DecidableEq Stmt✝] [DecidableEq Commit✝] [DecidableEq Chal✝] [DecidableEq Resp✝] [DecidableEq M✝] : DecidableEq (FischlinROInput Stmt✝ Commit✝ Chal✝ Resp✝ ρ✝ M✝)

def instDecidableEqFischlinROInput.decEq {Stmt✝ Commit✝ Chal✝ Resp✝ : Type} {ρ✝ : ℕ} {M✝ : Type} [DecidableEq Stmt✝] [DecidableEq Commit✝] [DecidableEq Chal✝] [DecidableEq Resp✝] [DecidableEq M✝] (x✝ x✝¹ : FischlinROInput Stmt✝ Commit✝ Chal✝ Resp✝ ρ✝ M✝) : Decidable (x✝ = x✝¹)

@[reducible, inline]

abbrev fischlinROSpec (Stmt Commit Chal Resp : Type) (ρ b : ℕ) (M : Type) : OracleSpec (FischlinROInput Stmt Commit Chal Resp ρ M)

The random oracle specification for the Fischlin transform. Domain: FischlinROInput (statement, message, commitment list, index, challenge, response). Range: Fin (2^b) (b-bit hash values).

@[reducible, inline]

abbrev FischlinProof (Commit Chal Resp : Type) (ρ : ℕ) : Type

A Fischlin proof consists of one (commitment, challenge, response) triple per parallel repetition.

Prover Search

Main Definition

def Fischlin {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] {m : Type → Type v} [Monad m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (ρ b S : ℕ) (M : Type) [DecidableEq M] [MonadLiftT ProbComp m] [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) m] : SignatureAlg m M Stmt Wit (FischlinProof Commit Chal Resp ρ)

The Fischlin transform applied to a Σ-protocol and a generable relation produces a signature scheme in the random oracle model.

Signing: generates ρ independent commitments, then for each repetition searches through all challenges ω ∈ Ω (via FinEnum.toList) to find the (ω, response) pair whose hash value is minimal, exiting early at hash 0.

Verification: re-hashes each (commitment, challenge, response) triple, checks sigma-protocol verification for each repetition, and verifies that the sum of hash values is at most S.

noncomputable def Fischlin.runtime {Stmt Commit Chal Resp : Type} [DecidableEq Stmt] [DecidableEq Commit] [DecidableEq Chal] [DecidableEq Resp] (ρ b : ℕ) (M : Type) [DecidableEq M] : ProbCompRuntime (OracleComp (unifSpec + fischlinROSpec Stmt Commit Chal Resp ρ b M))

Runtime bundle for the Fischlin random-oracle world.

theorem Fischlin.verify_usesAtMostRhoQueries {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [HasEvalSet m] (runtime : QueryRuntime (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (msg : M) (π : FischlinProof Commit Chal Resp ρ) : HasQuery.UsesAtMostQueries (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] => (Fischlin σ hr ρ b S M).verify pk msg π) runtime ρ

Fischlin verification makes at most ρ random-oracle queries under unit-cost instrumentation.

theorem Fischlin.verify_usesAtLeastRhoQueries {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [HasEvalSet m] (runtime : QueryRuntime (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (msg : M) (π : FischlinProof Commit Chal Resp ρ) : HasQuery.UsesAtLeastQueries (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] => (Fischlin σ hr ρ b S M).verify pk msg π) runtime ρ

Fischlin verification makes at least ρ random-oracle queries under unit-cost instrumentation.

theorem Fischlin.sign_usesAtMostRhoCardOmegaQueries {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [HasEvalSet m] (runtime : QueryRuntime (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (sk : Wit) (msg : M) : HasQuery.UsesAtMostQueries (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] => (Fischlin σ hr ρ b S M).sign pk sk msg) runtime (ρ * FinEnum.card Chal)

Fischlin signing makes at most ρ * |Ω| random-oracle queries under unit-cost instrumentation.

theorem Fischlin.sign_usesWeightedQueryCostAtMost {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [HasEvalSet m] {κ : Type} [AddCommMonoid κ] [PartialOrder κ] [IsOrderedAddMonoid κ] [CanonicallyOrderedAdd κ] (runtime : QueryRuntime (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : (fischlinROSpec Stmt Commit Chal Resp ρ b M).Domain → κ) (w : κ) (hcost : ∀ (t : (fischlinROSpec Stmt Commit Chal Resp ρ b M).Domain), costFn t ≤ w) : HasQuery.UsesCostAtMost (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT κ m)] => (Fischlin σ hr ρ b S M).sign pk sk msg) runtime costFn (ρ • FinEnum.card Chal • w)

Fischlin signing has weighted query cost at most ρ • (|Ω| • w) whenever every random-oracle query carries cost at most w.

theorem Fischlin.sign_expectedQueryCost_le {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [HasEvalSPMF m] {κ : Type} [AddCommMonoid κ] [PartialOrder κ] [IsOrderedAddMonoid κ] [CanonicallyOrderedAdd κ] (runtime : QueryRuntime (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : (fischlinROSpec Stmt Commit Chal Resp ρ b M).Domain → κ) (w : κ) (val : κ → ENNReal) (hcost : ∀ (t : (fischlinROSpec Stmt Commit Chal Resp ρ b M).Domain), costFn t ≤ w) (hval : Monotone val) : HasQuery.expectedQueryCost (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT κ m)] => (Fischlin σ hr ρ b S M).sign pk sk msg) runtime costFn val ≤ val (ρ • FinEnum.card Chal • w)

Fischlin signing has expected weighted query cost at most ρ • (|Ω| • w) whenever every random-oracle query is weighted by at most w.

theorem Fischlin.sign_expectedQueries_le_rhoCardOmega {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [HasEvalSPMF m] (runtime : QueryRuntime (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (sk : Wit) (msg : M) : HasQuery.expectedQueries (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] => (Fischlin σ hr ρ b S M).sign pk sk msg) runtime ≤ ↑ρ * ↑(FinEnum.card Chal)

Fischlin signing has expected query count at most ρ * |Ω| in the unit-cost runtime model.

This is the expectation-level counterpart of [Fischlin.sign_usesAtMostRhoCardOmegaQueries].

theorem Fischlin.verify_expectedQueries_eq_rho {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ρ b : ℕ) (M : Type) {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [FinEnum Chal] [Inhabited Chal] [Inhabited Resp] (hr : GenerableRelation Stmt Wit rel) (S : ℕ) [DecidableEq M] [HasEvalPMF m] (runtime : QueryRuntime (fischlinROSpec Stmt Commit Chal Resp ρ b M) m) (pk : Stmt) (msg : M) (π : FischlinProof Commit Chal Resp ρ) : HasQuery.expectedQueries (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] => (Fischlin σ hr ρ b S M).verify pk msg π) runtime = ↑ρ

Fischlin verification has expected query count exactly ρ in the unit-cost runtime model.

Completeness

noncomputable def Fischlin.completenessError (ρ b S t : ℕ) : ENNReal

Completeness error bound for the Fischlin transform (Fischlin 2005, Lemma 1).

Given ρ repetitions, b-bit hashes, max sum S, and challenge space size t: the error is ρ · ((2^b - ⌊S/ρ⌋ - 1) / 2^b)^t.

Derivation: by a union/pigeonhole bound over repetitions, if the sum of minimum hash values exceeds S, at least one minimum exceeds ⌊S/ρ⌋. The probability that the minimum of t independent uniform samples from Fin (2^b) exceeds k is ((2^b - k - 1) / 2^b)^t.

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

theorem Fischlin.almostComplete {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] [SampleableType Chal] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (ρ b S : ℕ) (M : Type) [DecidableEq M] (hρ : 0 < ρ) (hc : σ.PerfectlyComplete) (msg : M) : Pr[= true | (runtime ρ b M).evalDist do let __discr ← (Fischlin σ hr ρ b S M).keygen match __discr with | (pk, sk) => do let sig ← (Fischlin σ hr ρ b S M).sign pk sk msg (Fischlin σ hr ρ b S M).verify pk msg sig] ≥ 1 - completenessError ρ b S (FinEnum.card Chal)

Almost completeness of the Fischlin transform: if the underlying Σ-protocol is perfectly complete, then the signature scheme verifies with probability at least 1 - completenessError ρ b S t where t = FinEnum.card Chal is the challenge space size.

Unlike the Fiat-Shamir transform (which is perfectly complete), the Fischlin transform has a non-zero completeness error because the prover's proof-of-work search may fail to find hash values whose sum is at most S.

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).

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 with sorry bodies.

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] [SampleableType Chal] (σ : 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.