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