Σ-Protocols: Completeness, SHVZK, Special Soundness, and Commitment

A Σ-protocol is a three-move public-coin proof of knowledge: the prover sends a commitment a, the verifier replies with a uniform challenge e, the prover answers with a response z, and the verifier checks (a, e, z). The three canonical properties are

• completeness — an honest prover with a valid witness always convinces the verifier;
• special soundness — from two accepting transcripts sharing the first message but with distinct challenges one extracts a witness;
• special honest-verifier zero-knowledge (SHVZK) — for a fixed challenge the real transcript and a witness-free simulated transcript are identically distributed.

This file ports the Schnorr/Σ example so its scope matches SSProve-Rocq's Schnorr.v (perfect SHVZK + the derived commitment). We give a SigmaProtocol structure, the given-challenge transcript distributions, and the three property predicates, then instantiate the XOR-based Bool protocol simpleSigma and discharge all three. Following Damgård and SSProve's SigmaProtocol.v § Commitments, we derive a commitment scheme: hiding reduces to SHVZK (the one-time-pad masking argument that also underlies Examples/Commitment.maskComm_perfect_hiding) and binding reduces to special soundness.

The SHVZK proof is a one-line bijection coupling: XOR-by-(w ⊕ e) is a bijection of the sampled bit, so the real commitment a and the simulated response z are coupled and both transcripts coincide. This is the same liftR_uniform_bij coupling toolkit used by the core one-time-pad and masking-commitment examples.

Main results

• simpleSigma_complete — honest executions verify.
• simpleSigma_shvzk — perfect SHVZK: real and simulated transcripts are equal as distributions (advantage 0 for every transcript distinguisher, via simpleSigma_shvzk_zero_adv).
• simpleSigma_special_sound — the extractor recovers the witness.
• simpleSigma_hiding / simpleSigma_binding — the derived commitment is hiding (from SHVZK) and binding (from special soundness).

References

• [Damgård, On Σ-Protocols, §5]
• [Cramer & Damgård, Σ-Protocols and Efficient Zero-Knowledge]
• [Schnorr, Efficient Signature Generation by Smart Cards, J. Cryptology 1991]
• SSProve, theories/Crypt/examples/Schnorr.v and SigmaProtocol.v

Σ-Protocol Structure

structure CatCrypt.Examples.SigmaProtocol.SigmaProtocol : Type 1

A Σ-protocol: types and algorithms for the three-move prover/verifier interaction, together with an SHVZK simulator.

• Statement : Type

  Statements (what is proved).

• Witness : Type

  Witnesses (the prover's secret).

• Message : Type

  First messages (commitments).

• Challenge : Type

  Challenges (verifier coins).

• Response : Type

  Responses.

• finChallenge : Fintype self.Challenge

  Challenges are finite (for uniform sampling).

• neChallenge : Nonempty self.Challenge

  Challenges are nonempty.

• relation : self.Statement → self.Witness → Prop

  The NP relation: relation x w means w is a witness for x.

• commit : self.Statement → self.Witness → Core.SPComp self.Message

  Prover's first message.

• respond : self.Statement → self.Witness → self.Message → self.Challenge → Core.SPComp self.Response

  Prover's response to a challenge.

• verify : self.Statement → self.Message → self.Challenge → self.Response → Bool

  Verifier's decision.

• simulate : self.Statement → self.Challenge → Core.SPComp (self.Message × self.Response)

  SHVZK simulator.

structure CatCrypt.Examples.SigmaProtocol.Transcript (sp : SigmaProtocol) : Type

A transcript of a Σ-protocol run.

• message : sp.Message

  First message (commitment).

• challenge : sp.Challenge

  Challenge.

• response : sp.Response

  Response.

Given-Challenge Transcript Distributions

Following SSProve's SigmaProtocol.v, the challenge e is provided as input (the TRANSCRIPT procedure takes (h, w, e)); this is the standard SHVZK scope and admits a one-dimensional bijection coupling.

noncomputable def CatCrypt.Examples.SigmaProtocol.realTranscript (sp : SigmaProtocol) (x : sp.Statement) (w : sp.Witness) (e : sp.Challenge) : Core.SPComp (Transcript sp)

Real transcript for a fixed challenge: honest prover commits and responds.

Equations

• CatCrypt.Examples.SigmaProtocol.realTranscript sp x w e = do let a ← sp.commit x w let z ← sp.respond x w a e pure { message := a, challenge := e, response := z }

noncomputable def CatCrypt.Examples.SigmaProtocol.simulatedTranscript (sp : SigmaProtocol) (x : sp.Statement) (e : sp.Challenge) : Core.SPComp (Transcript sp)

Simulated transcript for a fixed challenge: the simulator produces (a, z) without the witness.

Equations

• CatCrypt.Examples.SigmaProtocol.simulatedTranscript sp x e = do let __discr ← sp.simulate x e match __discr with | (a, z) => pure { message := a, challenge := e, response := z }

Property Predicates

def CatCrypt.Examples.SigmaProtocol.Completeness (sp : SigmaProtocol) : Prop

Completeness: honest transcripts verify.

Equations

• CatCrypt.Examples.SigmaProtocol.Completeness sp = ∀ (x : sp.Statement) (w : sp.Witness), sp.relation x w → ∀ (a : sp.Message) (e : sp.Challenge) (z : sp.Response), sp.verify x a e z = true

def CatCrypt.Examples.SigmaProtocol.SHVZK (sp : SigmaProtocol) : Prop

Perfect SHVZK: for any valid statement/witness and any fixed challenge, the real and simulated transcript distributions are equal — coupled by eqPre to eqPost, hence indistinguishable to every transcript distinguisher.

Equations

• One or more equations did not get rendered due to their size.

structure CatCrypt.Examples.SigmaProtocol.TwoTranscripts (sp : SigmaProtocol) (x : sp.Statement) : Type

Two accepting transcripts sharing the first message but with distinct challenges — the input to a special-soundness extractor.

• message : sp.Message

  Shared first message.

• challenge₁ : sp.Challenge

  First challenge.

• response₁ : sp.Response

  First response.

• challenge₂ : sp.Challenge

  Second challenge.

• response₂ : sp.Response

  Second response.

• accept₁ : sp.verify x self.message self.challenge₁ self.response₁ = true

  First transcript accepts.

• accept₂ : sp.verify x self.message self.challenge₂ self.response₂ = true

  Second transcript accepts.

• diff : self.challenge₁ ≠ self.challenge₂

  Challenges differ.

def CatCrypt.Examples.SigmaProtocol.SpecialSoundness (sp : SigmaProtocol) : Prop

Special soundness: an extractor turns any TwoTranscripts into a witness.

Equations

• One or more equations did not get rendered due to their size.

XOR-Based Σ-Protocol over Bool

The demonstration protocol: everything is a bit, the relation is x = w, the response masks the commitment by w ⊕ e, and the simulator masks a fresh response instead.

def CatCrypt.Examples.SigmaProtocol.xorTransformBij (w e : Bool) : Bool ≃ Bool

The XOR bijection carrying SHVZK: for fixed w, e, the map a ↦ a ⊕ w ⊕ e couples the real commitment with the simulated response.

Equations

• CatCrypt.Examples.SigmaProtocol.xorTransformBij w e = { toFun := fun (a : Bool) => a ^^ w ^^ e, invFun := fun (z : Bool) => z ^^ e ^^ w, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CatCrypt.Examples.SigmaProtocol.xorTransformBij_apply (w e a : Bool) : (xorTransformBij w e) a = (a ^^ w ^^ e)

noncomputable def CatCrypt.Examples.SigmaProtocol.simpleSigma : SigmaProtocol

The XOR-based Σ-protocol over Bool.

Equations

• One or more equations did not get rendered due to their size.

Completeness

theorem CatCrypt.Examples.SigmaProtocol.simpleSigma_complete (x w : Bool) (hrel : simpleSigma.relation x w) (a e : Bool) : have z := a ^^ w ^^ e; simpleSigma.verify x a e z = true

Completeness: an honest transcript (a, e, a ⊕ w ⊕ e) verifies.

SHVZK

theorem CatCrypt.Examples.SigmaProtocol.simpleSigma_shvzk : SHVZK simpleSigma

Perfect SHVZK for simpleSigma. The bijection xorTransformBij x e couples the real sampled commitment a with the simulated sampled response z = a ⊕ x ⊕ e; the simulated message z ⊕ x ⊕ e collapses back to a, so both runs yield the identical transcript. The whole argument is one liftR_bind (liftR_uniform_bij …) coupling.

theorem CatCrypt.Examples.SigmaProtocol.simpleSigma_shvzk_zero_adv (x e : Bool) (A : Transcript simpleSigma → Core.SPComp Bool) : Crypto.AdvantageA (realTranscript simpleSigma x x e) (simulatedTranscript simpleSigma x e) A = 0

Perfect SHVZK, advantage form: no distinguisher separates the real from the simulated transcript.

Special Soundness

def CatCrypt.Examples.SigmaProtocol.simpleSigmaExtractor (x : Bool) (tt : TwoTranscripts simpleSigma x) : Bool

Extractor for simpleSigma: from (a, e₁, z₁) accepting, a ⊕ z₁ = x ⊕ e₁, so x = a ⊕ z₁ ⊕ e₁.

Equations

• CatCrypt.Examples.SigmaProtocol.simpleSigmaExtractor x tt = (tt.message ^^ tt.response₁ ^^ tt.challenge₁)

theorem CatCrypt.Examples.SigmaProtocol.simpleSigma_special_sound : SpecialSoundness simpleSigma

Special soundness for simpleSigma.

Derived Commitment Scheme

The Σ-protocol's first message is a commitment to the challenge, with the response as opening (Damgård §5, SSProve SigmaProtocol.v § Commitments).

theorem CatCrypt.Examples.SigmaProtocol.simpleSigma_hiding (x e : Bool) : Relational.rHoare Relational.eqPre (realTranscript simpleSigma x x e) (simulatedTranscript simpleSigma x e) Relational.eqPost

Hiding: the real and simulated commitment transcripts are equidistributed — a direct instance of SHVZK. The masking here is exactly the one-time pad that makes Examples/Commitment.maskComm perfectly hiding.

structure CatCrypt.Examples.SigmaProtocol.DoubleOpening (sp : SigmaProtocol) (x : sp.Statement) : Type

Two openings of a single commitment under different challenges.

• commitment : sp.Message

  The shared commitment.

• challenge₁ : sp.Challenge

  First challenge.

• response₁ : sp.Response

  First response.

• challenge₂ : sp.Challenge

  Second challenge.

• response₂ : sp.Response

  Second response.

• diff : self.challenge₁ ≠ self.challenge₂

  Challenges differ.

• verify₁ : sp.verify x self.commitment self.challenge₁ self.response₁ = true

  First opening verifies.

• verify₂ : sp.verify x self.commitment self.challenge₂ self.response₂ = true

  Second opening verifies.

def CatCrypt.Examples.SigmaProtocol.DoubleOpening.toTwoTranscripts {sp : SigmaProtocol} {x : sp.Statement} (dop : DoubleOpening sp x) : TwoTranscripts sp x

A double opening is exactly the input to the special-soundness extractor.

Equations

• One or more equations did not get rendered due to their size.

theorem CatCrypt.Examples.SigmaProtocol.commitment_binding (sp : SigmaProtocol) (hSS : SpecialSoundness sp) (x : sp.Statement) (dop : DoubleOpening sp x) : ∃ (w : sp.Witness), sp.relation x w

Binding from special soundness. An adversary who double-opens a commitment yields a witness, so breaking binding solves the hard instance.

theorem CatCrypt.Examples.SigmaProtocol.simpleSigma_binding (x : Bool) (dop : DoubleOpening simpleSigma x) : ∃ (w : simpleSigma.Witness), simpleSigma.relation x w

Binding for the simpleSigma commitment.