Sigma Protocol Example

This file demonstrates Sigma protocols formalized in CatCrypt-Lean4.

Overview

A Sigma protocol is a three-move public-coin interactive proof system:

1. Prover sends commitment (message)
2. Verifier sends random challenge
3. Prover sends response
4. Verifier accepts/rejects

Properties

• Completeness: Honest prover with valid witness is always accepted
• Special Soundness: From two accepting transcripts with same commitment but different challenges, one can extract a valid witness
• Special Honest-Verifier Zero-Knowledge (SHVZK): A simulator can produce transcripts indistinguishable from real ones given only the statement and challenge

Main definitions

• SigmaProtocol — the three-move structure with a stateless prover.
• SigmaProtocolS — the three-move structure whose prover carries state from the first move to the third, with SigmaProtocol.toSigmaProtocolS for the trivial-state case and SigmaProtocolS.toSigmaProtocol for the stateless protocol whose first message carries the state.
• Completeness, SpecialSoundness, SHVZK, SHVZK_given — the property predicates.

Implementation

We use a simplified model over Bool types (like PRF.lean) to demonstrate the proof techniques. The key insight for SHVZK is that if the simulator samples the challenge first and then computes (message, response) via a bijection, it produces the same distribution as the real protocol.

References

• [Damgard, On Sigma Protocols]
• [Cramer & Damgard, Sigma Protocols and Efficient Zero-Knowledge]

Type Definitions

@[reducible, inline]

abbrev CatCrypt.Examples.Sigma.Value : Type

Use Bool as simple finite type for demonstration

Equations

• CatCrypt.Examples.Sigma.Value = Bool

@[instance_reducible]

def CatCrypt.Examples.Sigma.instFintypeValue : Fintype Value

Equations

• CatCrypt.Examples.Sigma.instFintypeValue = inferInstance

theorem CatCrypt.Examples.Sigma.instNonemptyValue : Nonempty Value

@[instance_reducible]

def CatCrypt.Examples.Sigma.instDecidableEqValue : DecidableEq Value

Equations

• CatCrypt.Examples.Sigma.instDecidableEqValue = inferInstance

Sigma Protocol Structure

structure CatCrypt.Examples.Sigma.SigmaProtocol : Type 1

A Sigma protocol consists of types and algorithms for the three-move interaction between prover and verifier.

• Statement : Type

  Type of statements (what we're proving)

• Witness : Type

  Type of witnesses (secret known to prover)

• Message : Type

  Type of first message (commitment)

• Challenge : Type

  Type of challenge (from verifier)

• Response : Type

  Type of response

• finChallenge : Fintype self.Challenge

  Challenge type is finite (for uniform sampling)

• neChallenge : Nonempty self.Challenge

  Challenge type is nonempty

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

  The NP relation: R(x, w) means w is a valid witness for x

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

  Prover's first message (commitment)

• 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 check

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

  Simulator for SHVZK

Sigma Protocols with Prover State

structure CatCrypt.Examples.Sigma.SigmaProtocolS : Type 1

A Sigma protocol whose prover carries state from the first move to the third. The commitment step returns a message together with a private state PState, and the response step reads that state.

SigmaProtocol is the special case PState = Unit, recorded by SigmaProtocol.toSigmaProtocolS. A protocol whose response depends on randomness that the commitment does not determine — because the map from that randomness to the message loses information — is expressible here and not over SigmaProtocol.

• Statement : Type

  Type of statements (what we're proving)

• Witness : Type

  Type of witnesses (secret known to prover)

• Message : Type

  Type of first message (commitment)

• Challenge : Type

  Type of challenge (from verifier)

• Response : Type

  Type of response

• PState : Type

  Type of the prover's private state between the first and third move

• finChallenge : Fintype self.Challenge

  Challenge type is finite (for uniform sampling)

• neChallenge : Nonempty self.Challenge

  Challenge type is nonempty

• neState : Nonempty self.PState

  The prover-state type is nonempty

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

  The NP relation: R(x, w) means w is a valid witness for x

• commit : self.Statement → self.Witness → Core.SPComp (self.Message × self.PState)

  Prover's first message together with the state it retains

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

  Prover's response, reading the retained state

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

  Verifier's check, on the public transcript only

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

  Simulator for SHVZK, producing a public transcript

noncomputable def CatCrypt.Examples.Sigma.SigmaProtocol.toSigmaProtocolS (sp : SigmaProtocol) : SigmaProtocolS

A SigmaProtocol viewed as a SigmaProtocolS with trivial prover state.

Equations

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

noncomputable def CatCrypt.Examples.Sigma.SigmaProtocolS.toSigmaProtocol (sps : SigmaProtocolS) : SigmaProtocol

The stateless Sigma protocol obtained by appending the prover state to the first message. The verifier ignores the appended component, so the predicates that read only the types and verify — the soundness error, TwoTranscripts, SpecialSoundness — are statements about the same verification equation as sps.

The simulator has no state to produce and emits an arbitrary one, so the zero-knowledge predicates, which compare real and simulated first messages, do not transfer.

Equations

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

Transcript Type

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

A transcript of a Sigma protocol execution

• message : sp.Message
• challenge : sp.Challenge
• response : sp.Response

Protocol Computations

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

Real protocol execution: prover with witness generates transcript

Equations

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

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

Simulated transcript: simulator generates transcript given challenge

Equations

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

Protocol Computations with Given Challenge (Rocq style)

In the standard cryptographic definition of SHVZK, the challenge is provided as input rather than sampled internally. This matches Rocq's CatCrypt formalization where chInput = (h, w, e) includes the challenge. This allows a simpler 1D bijection coupling proof.

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

Real protocol with given challenge: prover generates transcript for fixed challenge

Equations

• CatCrypt.Examples.Sigma.realTranscriptGiven 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.Sigma.simulatedTranscriptGiven (sp : SigmaProtocol) (x : sp.Statement) (e : sp.Challenge) : Core.SPComp (Transcript sp)

Simulated transcript with given challenge

Equations

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

Completeness Property

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

Completeness: honest execution with valid witness always verifies

Equations

• CatCrypt.Examples.Sigma.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

Special Soundness Property

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

Two accepting transcripts with same message but different challenges

• message : sp.Message
• challenge1 : sp.Challenge
• response1 : sp.Response
• challenge2 : sp.Challenge
• response2 : sp.Response
• accept1 : sp.verify x self.message self.challenge1 self.response1 = true
• accept2 : sp.verify x self.message self.challenge2 self.response2 = true
• diff : self.challenge1 ≠ self.challenge2

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

Special soundness: from two accepting transcripts with same commitment but different challenges, extract a valid witness

Equations

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

SHVZK Property

def CatCrypt.Examples.Sigma.SHVZK_given (sp : SigmaProtocol) : Prop

Special Honest-Verifier Zero-Knowledge (given challenge version): For any given challenge, real and simulated transcripts have the same distribution.

This is the standard cryptographic definition where the challenge is provided as input (matching Rocq's CatCrypt formalization). This formulation allows a simple 1D bijection coupling proof.

Equations

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

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

Special Honest-Verifier Zero-Knowledge: real and simulated transcripts have the same distribution for any statement with a valid witness.

This is formalized using rHoare: for any precondition, the real and simulated computations produce outputs that are equal (same transcript).

Equations

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

Simple Example: XOR-based Protocol over Bool

@[implicit_reducible]

noncomputable def CatCrypt.Examples.Sigma.simpleSigma : SigmaProtocol

A simple Sigma protocol where the statement is the XOR of message and response, and the witness is either true or false.

Statement: x Witness: w such that x = (witness property) Protocol:

• Commit: sample random message a
• Challenge: e (random Bool)
• Response: z = xor a (xor w e)
• Verify: check that xor a z = xor w e... (simplified)

For simplicity, we use a trivial protocol where everything is in Bool.

Equations

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

Bijection for SHVZK Proof

The key bijection for SHVZK relates sampled values directly:

• Real: sample a, compute z = xor (xor a w) e
• Simulated: sample z, compute a = xor z (xor x e)

When x = w:

• From real (a, z): z = xor (xor a w) e
• The bijection f : a ↦ z = xor (xor a w) e is an equiv on Bool

If we show uniform(a).bind(a ↦ pure(a, f(a))) = uniform(z).bind(z ↦ pure(f⁻¹(z), z)), then the transcripts have the same distribution.

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

XOR-based bijection: for fixed w and e, mapping a to z

Equations

• CatCrypt.Examples.Sigma.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.Sigma.xorTransformBij_apply (w e a : Bool) : (xorTransformBij w e) a = (a ^^ w ^^ e)

The forward map of xorTransformBij w e sends a to a ⊕ w ⊕ e.

@[simp]

theorem CatCrypt.Examples.Sigma.xorTransformBij_symm_apply (w e z : Bool) : (xorTransformBij w e).symm z = (z ^^ e ^^ w)

The inverse map of xorTransformBij w e sends z to z ⊕ e ⊕ w.

def CatCrypt.Examples.Sigma.sigmaBij (w : Bool) : Bool × Bool ≃ Bool × Bool

2D bijection for Sigma protocol SHVZK: Maps (a, e) from Real protocol to (e', z) from Simulation where e' = e (challenges match) and z = xor (xor a w) e (responses match). Then Sim's computed message = xor z (xor w e') = a = Real's message.

Equations

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

@[simp]

theorem CatCrypt.Examples.Sigma.sigmaBij_fst (w a e : Bool) : ((sigmaBij w) (a, e)).1 = e

The first component of sigmaBij w (a, e) is the challenge e.

@[simp]

theorem CatCrypt.Examples.Sigma.sigmaBij_snd (w a e : Bool) : ((sigmaBij w) (a, e)).2 = (a ^^ w ^^ e)

The second component of sigmaBij w (a, e) is the response a ⊕ w ⊕ e.

Completeness Proof for simpleSigma

theorem CatCrypt.Examples.Sigma.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 for simpleSigma: honest executions always verify.

Note: The generic Completeness definition above is too strong as it requires verify to succeed for ALL z values. The correct formulation is that verify succeeds for z produced by the honest respond function. This theorem captures the correct completeness property.

SHVZK Proof for simpleSigma

theorem CatCrypt.Examples.Sigma.simpleSigma_shvzk_given : SHVZK_given simpleSigma

SHVZK for simpleSigma with given challenge: the core bijection coupling proof.

This follows Rocq's CatCrypt approach where the challenge e is provided as input. The bijection xorTransformBij w e : a ↦ z = a ⊕ w ⊕ e couples:

• Real's sampled commitment a
• Sim's sampled response z

Since a' = z ⊕ w ⊕ e = (a ⊕ w ⊕ e) ⊕ w ⊕ e = a, both produce the same transcript.

theorem CatCrypt.Examples.Sigma.simpleSigma_shvzk : SHVZK simpleSigma

SHVZK for simpleSigma with the challenge sampled internally rather than supplied as input.

This extends the standard SHVZK definition used in Rocq's CatCrypt (SigmaProtocol.v:163-170), where the challenge is part of the input (h, w, e). The SHVZK_given theorem above matches that input-challenge formulation; this variant samples the challenge inside the protocol.

Special Soundness for simpleSigma

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

The extractor for simpleSigma: given two transcripts with same a, different e, extract the witness.

From two accepting transcripts:

• (a, e₁, z₁) with xor a z₁ = xor x e₁
• (a, e₂, z₂) with xor a z₂ = xor x e₂

We can compute: xor (xor a z₁) (xor a z₂) = xor (xor x e₁) (xor x e₂) xor z₁ z₂ = xor e₁ e₂ (by XOR properties)

And from xor a z₁ = xor x e₁: x = xor (xor a z₁) e₁

So the extractor returns: xor (xor a z₁) e₁

Equations

• CatCrypt.Examples.Sigma.simpleSigmaExtractor x tt = (tt.message ^^ tt.response1 ^^ tt.challenge1)

theorem CatCrypt.Examples.Sigma.simpleSigma_special_sound : SpecialSoundness simpleSigma

simpleSigma satisfies special soundness: simpleSigmaExtractor recovers a valid witness from any two accepting transcripts sharing a commitment.