Sigma Protocol

This file defines a structure type for Σ-protocols, along with standard security properties: completeness, special soundness, and honest-verifier zero-knowledge (HVZK).

Type Parameters

• Stmt: statement (public key)
• Wit: witness (secret key)
• Commit: public commitment
• PrvState: private prover state (retained between commit and respond)
• Chal: verifier challenge (drawn uniformly)
• Resp: prover response
• rel: the relation proven by the protocol

Coercion to IdenSchemeWithAbort

Every SigmaProtocol can be viewed as a non-aborting IdenSchemeWithAbort via SigmaProtocol.toIdenSchemeWithAbort, which wraps respond with some.

structure SigmaProtocol (Stmt Wit Commit PrvState Chal Resp : Type) (rel : Stmt → Wit → Bool) : Type

A sigma protocol for statements in Stmt and witnesses in Wit, where rel : Stmt → Wit → Bool is the proposition proven by the Σ-protocol. Commitments are split into a public part Commit (revealed to the verifier) and a private part PrvState (retained by the prover). Verifier challenges are drawn uniformly from Chal. Prover responses are in Resp.

We leave properties like special soundness as separate definitions for better modularity.

• commit (stmt : Stmt) (wit : Wit) : ProbComp (Commit × PrvState)

  Generate a commitment to prove knowledge of a valid witness.

• respond (stmt : Stmt) (wit : Wit) (prvState : PrvState) (chal : Chal) : ProbComp Resp

  Given a previous private state, respond to the challenge.

• verify (stmt : Stmt) (commit : Commit) (chal : Chal) (resp : Resp) : Bool

  Deterministic verification: check that the response satisfies the challenge.

• sim (stmt : Stmt) : ProbComp Commit

  Simulate public commitment generation while only knowing the statement.

• extract (chal₁ : Chal) (resp₁ : Resp) (chal₂ : Chal) (resp₂ : Resp) : ProbComp Wit

  Extract a witness to the statement from two accepting transcripts.

def SigmaProtocol.PerfectlyComplete {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] [unifSpec.Fintype] [unifSpec.Inhabited] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) : Prop

A Σ-protocol is perfectly complete if the honest prover always convinces the verifier on valid statement-witness pairs.

def SigmaProtocol.SpeciallySoundAt {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (x : Stmt) : Prop

Special soundness at a particular statement: given two accepting transcripts with the same commitment but different challenges, the extracted witness is valid.

def SigmaProtocol.SpeciallySound {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) : Prop

A Σ-protocol is specially sound if SpeciallySoundAt holds for all statements.

theorem SigmaProtocol.extract_sound_of_speciallySoundAt {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) {x : Stmt} (hss : σ.SpeciallySoundAt x) {pc : Commit} {ω₁ ω₂ : Chal} {p₁ p₂ : Resp} (hω : ω₁ ≠ ω₂) (hv₁ : σ.verify x pc ω₁ p₁ = true) (hv₂ : σ.verify x pc ω₂ p₂ = true) {w : Wit} (hw : w ∈ support (σ.extract ω₁ p₁ ω₂ p₂)) : rel x w = true

Special soundness immediately validates any witness returned by the Σ-protocol extractor from two accepting transcripts with the same statement and commitment and with distinct challenges.

def SigmaProtocol.realTranscript {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (x : Stmt) (w : Wit) : ProbComp (Commit × Chal × Resp)

The honest prover's transcript distribution for a Σ-protocol.

def SigmaProtocol.HVZK {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] [unifSpec.Fintype] [unifSpec.Inhabited] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (simTranscript : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk : ℝ) : Prop

Honest-verifier zero-knowledge: the real transcript distribution is within total variation distance ζ_zk of the simulated one.

The real transcript is σ.realTranscript x w. The simulated transcript is produced by simTranscript given only the statement x.

Note: the sim field of SigmaProtocol only produces a public commitment. For HVZK we need a full transcript simulator Stmt → ProbComp (Commit × Chal × Resp). We parameterize by this simulator.

def SigmaProtocol.PerfectHVZK {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] [unifSpec.Fintype] [unifSpec.Inhabited] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (simTranscript : Stmt → ProbComp (Commit × Chal × Resp)) : Prop

Exact honest-verifier zero-knowledge: the real transcript distribution equals the simulated one.

theorem SigmaProtocol.perfectHVZK_iff_hvzk_zero {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Chal] [unifSpec.Fintype] [unifSpec.Inhabited] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (simTranscript : Stmt → ProbComp (Commit × Chal × Resp)) : σ.PerfectHVZK simTranscript ↔ σ.HVZK simTranscript 0

The perfect HVZK property is equivalent to the approximate HVZK property with ζ_zk = 0.

def SigmaProtocol.simCommitPredictability {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [unifSpec.Fintype] [unifSpec.Inhabited] (_σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (simTranscript : Stmt → ProbComp (Commit × Chal × Resp)) (β : ENNReal) : Prop

The simulator's commitment marginal has predictability at most β: no single commitment value is output with probability exceeding β. Equivalently, the commitment has min-entropy at least -log₂ β.

This is a companion assumption to HVZK that bounds the collision probability of programmed cache entries in the Fiat-Shamir CMA-to-NMA reduction. For Schnorr, β = 1/|G| because the commitment g^r is uniform over the group.

The _σ : SigmaProtocol … argument is dummy (the predicate only depends on simTranscript and β); it is present to enable field-notation usage like σ.simCommitPredictability simTranscript β.

def SigmaProtocol.simChalUniformGivenCommit {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [unifSpec.Fintype] [unifSpec.Inhabited] [Fintype Chal] (_σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (simTranscript : Stmt → ProbComp (Commit × Chal × Resp)) : Prop

Conditional uniformity of the simulator's challenge given its commitment, expressed in product form: for any statement x admitting a witness, any commit value c₀, and any challenge value ch₀, the joint marginal Pr[(commit, chal) = (c₀, ch₀)] factors as Pr[commit = c₀] * (1 / |Chal|).

This is a strengthening of simCommitPredictability (which only bounds the commit marginal). Where the latter says "no commit value is too likely", simChalUniformGivenCommit says "the challenge is uniform conditional on any commit value", which is exactly the hypothesis required by identical_until_bad_with_flag when bridging the Fiat-Shamir programming-oracle and no-programming-oracle worlds: cache misses on programmed points return the simulator's challenge, and the bridge needs that challenge to be marginally uniform conditional on the simulator's commit (which is what gets compared against the random oracle's would-be answer).

The product form P[(c₀, ch₀)] = P[c₀] * 1/|Chal| avoids conditional-probability ambiguities when P[c₀] = 0 and is the most directly-usable shape inside the tvDist calculation.

The rel pk sk = true hypothesis is needed because typical Schnorr-style simulators only satisfy this when pk admits a witness (the proof uses a witness-indexed bijection on the response variable); for statements outside the relation's image, the simulator's joint may have any structure.

def SigmaProtocol.UniqueResponses {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) : Prop

A Σ-protocol has unique responses if for any statement, commitment, and challenge, there is at most one valid response. This property is required by the Fischlin transform and holds for most common Σ-protocols (Schnorr, Guillou-Quisquater, etc.).

def SigmaProtocol.toIdenSchemeWithAbort {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel

Every SigmaProtocol can be viewed as a non-aborting IdenSchemeWithAbort by wrapping the response in some. The sim and extract fields are not part of IdenSchemeWithAbort and are dropped.

@[implicit_reducible]

instance SigmaProtocol.instCoeIdenSchemeWithAbort {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} : Coe (SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel)