Fischlin Transform: Core Definitions

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.

This module holds the core definitions: the random-oracle input type FischlinROInput, the oracle signature fischlinROSpec, the proof type FischlinProof, the prover's inner search fischlinSearchAux, the transform Fischlin itself, and the bundled random-oracle runtime used to denote the signature scheme as a probabilistic computation.

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)

Module layout

The development is split across the sibling modules under Fischlin/:

• Fischlin.Defs — the definitions in this file.
• Fischlin.CostAccounting — random-oracle query-cost and expected-query bounds for sign and verify.
• Fischlin.Completeness — the completeness bound almostComplete via the pure-probability model game.
• Fischlin.KnowledgeSoundness — online extraction and the knowledgeSoundness bound via a supermartingale potential argument.

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

def fischlinSearchAux {Stmt Wit Commit PrvState Chal Resp M : Type} {rel : Stmt → Wit → Bool} {ρ b : ℕ} {m : Type → Type v} [Monad m] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) [MonadLiftT ProbComp m] [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) m] (pk : Stmt) (sk : Wit) (sc : PrvState) (msg : M) (comList : List Commit) (i : Fin ρ) : List Chal → Option (Chal × Resp × Fin (2 ^ b)) → m (Option (Chal × Resp))

Recursive search over a list of challenges for one Fischlin repetition.

For each challenge ω, computes the sigma protocol response and queries the hash oracle. Exits early if a hash value of 0 is found (the ideal "proof of work" result). Otherwise, tracks the (challenge, response) pair with the minimal hash value.

This models the sequential search in Construction 1 of the Fischlin paper: the prover queries H on each input and keeps the best.

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.