Sigma protocols

A Sigma protocol ([BS23], Section 19.4) is a three-move protocol for a relation R : X → Y → Prop: given a witness x for the statement y, the prover sends a commitment t, the verifier replies with a uniformly random challenge c from a finite set, the prover answers with a response z, and the verifier decides deterministically from y and the conversation (t, c, z).

The prover's private state between its two messages is explicit. Its commitment and state are sampled together, and its response is a function of the state and the challenge; randomness the response needs can be sampled with the commitment and kept in the state. Protocols are plain functions and distributions, with no efficiency or finiteness assumption; the properties are exact statements about a single protocol.

Each property carries its algorithm explicitly. SpecialSoundness R extract says that the deterministic extract computes a witness from any two accepting conversations that share a commitment and have distinct challenges, for every statement, with or without a witness. SpecialHVZK R simulate says that the simulator, given a statement and a challenge, always outputs accepting conversations, and that for each witness-statement pair and each fixed challenge its output has exactly the law of the honest commitment and response. With a uniform challenge this gives the book's Definition 19.5 (SpecialHVZK.conversation_eq).

Main definitions

• Cslib.Crypto.Protocols.SigmaProtocol: commitment, response and verification.
• SigmaProtocol.transcript, SigmaProtocol.conversation: honest executions.
• SigmaProtocol.Complete: honest conversations always accept.
• SigmaProtocol.SpecialSoundness: an explicit witness extractor (Definition 19.4).
• SigmaProtocol.SpecialHVZK: an explicit perfect simulator (Definition 19.5).

Main results

• SigmaProtocol.Complete.accepts_of_mem_support_conversation: the verifier always accepts the honest prover.
• SigmaProtocol.SpecialHVZK.conversation_eq: a simulated conversation with a uniform challenge has the law of an honest one.
• SigmaProtocol.SpecialSoundness.exists_witness: two accepting conversations with a common commitment and distinct challenges certify that the statement has a witness.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 19.4.

structure Cslib.Crypto.Protocols.SigmaProtocol (Witness Statement Commitment Challenge Response : Type u) : Type (u + 1)

A Sigma protocol with witnesses in Witness, statements in Statement, and conversations (t, c, z) in Commitment × Challenge × Response ([BS23], Definition 19.3). Completeness and the security properties are separate predicates.

• State : Type u

  The prover's private state between its commitment and its response.

• commit : Witness → Statement → PMF (Commitment × self.State)

  Sample the commitment together with the prover's private state.

• respond : Witness → Statement → self.State → Challenge → Response

  Answer a challenge from the private state.

• verify : Statement → Commitment → Challenge → Response → Bool

  The verifier's deterministic decision on a statement and a conversation.

def Cslib.Crypto.Protocols.SigmaProtocol.Accepts {X Y T C Z : Type u} (P : SigmaProtocol X Y T C Z) (y : Y) (t : T) (c : C) (z : Z) : Prop

The conversation (t, c, z) is accepting for the statement y.

@[instance_reducible]

instance Cslib.Crypto.Protocols.SigmaProtocol.instDecidableAccepts {X Y T C Z : Type u} (P : SigmaProtocol X Y T C Z) (y : Y) (t : T) (c : C) (z : Z) : Decidable (P.Accepts y t c z)

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.transcript {X Y T C Z : Type u} (P : SigmaProtocol X Y T C Z) (x : X) (y : Y) (c : C) : PMF (T × Z)

The honest prover's commitment and response when the verifier sends the challenge c.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.conversation {X Y T C Z : Type u} (P : SigmaProtocol X Y T C Z) [Fintype C] [Nonempty C] (x : X) (y : Y) : PMF (T × C × Z)

An honest execution: the prover commits, the verifier sends a uniform challenge, and the prover responds.

def Cslib.Crypto.Protocols.SigmaProtocol.Complete {X Y T C Z : Type u} (P : SigmaProtocol X Y T C Z) (R : X → Y → Prop) : Prop

Completeness ([BS23], Definition 19.3): for every witness-statement pair in R and every challenge, every honest transcript is accepting.

def Cslib.Crypto.Protocols.SigmaProtocol.SpecialSoundness {X Y T C Z : Type u} (P : SigmaProtocol X Y T C Z) (R : X → Y → Prop) (extract : Y → T → C → Z → C → Z → X) : Prop

Special soundness ([BS23], Definition 19.4): extract returns a witness for any statement from two accepting conversations with a common commitment and distinct challenges.

structure Cslib.Crypto.Protocols.SigmaProtocol.SpecialHVZK {X Y T C Z : Type u} (P : SigmaProtocol X Y T C Z) (R : X → Y → Prop) (simulate : Y → C → PMF (T × Z)) : Prop

Special honest-verifier zero knowledge ([BS23], Definition 19.5) with the explicit simulator simulate. The simulator gets a statement and a challenge and returns a commitment and a response.

• accepts (y : Y) (c : C) (tz : T × Z) : tz ∈ (simulate y c).support → P.Accepts y tz.1 c tz.2

  Simulated conversations are accepting, for every statement and challenge.

• transcript_eq (x : X) (y : Y) : R x y → ∀ (c : C), simulate y c = P.transcript x y c

  For a witness-statement pair, simulation at any fixed challenge has the honest law.

theorem Cslib.Crypto.Protocols.SigmaProtocol.Complete.mono {X Y T C Z : Type u} {P : SigmaProtocol X Y T C Z} {R R' : X → Y → Prop} (h : P.Complete R) (hR : ∀ (x : X) (y : Y), R' x y → R x y) : P.Complete R'

Completeness for a relation implies completeness for every smaller relation.

theorem Cslib.Crypto.Protocols.SigmaProtocol.SpecialSoundness.mono {X Y T C Z : Type u} {P : SigmaProtocol X Y T C Z} {R R' : X → Y → Prop} {extract : Y → T → C → Z → C → Z → X} (h : P.SpecialSoundness R extract) (hR : ∀ (x : X) (y : Y), R x y → R' x y) : P.SpecialSoundness R' extract

A witness extractor for a relation is one for every larger relation.

theorem Cslib.Crypto.Protocols.SigmaProtocol.SpecialHVZK.mono {X Y T C Z : Type u} {P : SigmaProtocol X Y T C Z} {R R' : X → Y → Prop} {simulate : Y → C → PMF (T × Z)} (h : P.SpecialHVZK R simulate) (hR : ∀ (x : X) (y : Y), R' x y → R x y) : P.SpecialHVZK R' simulate

A simulator for a relation is one for every smaller relation.

theorem Cslib.Crypto.Protocols.SigmaProtocol.Complete.accepts_of_mem_support_commit {X Y T C Z : Type u} {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} (h : P.Complete R) {x : X} {y : Y} (hxy : R x y) {ts : T × P.State} (hts : ts ∈ (P.commit x y).support) (c : C) : P.Accepts y ts.1 c (P.respond x y ts.2 c)

Every possible honest commitment leads to an accepting response, whatever the challenge.

theorem Cslib.Crypto.Protocols.SigmaProtocol.SpecialSoundness.exists_witness {X Y T C Z : Type u} {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} {extract : Y → T → C → Z → C → Z → X} (h : P.SpecialSoundness R extract) {y : Y} {t : T} {c c' : C} {z z' : Z} (hc : c ≠ c') (hz : P.Accepts y t c z) (hz' : P.Accepts y t c' z') : ∃ (x : X), R x y

Special soundness certifies that the statement has a witness.

theorem Cslib.Crypto.Protocols.SigmaProtocol.transcript_bind {X Y T C Z : Type u} (P : SigmaProtocol X Y T C Z) {β : Type u_1} (x : X) (y : Y) (c : C) (next : T × Z → PMF β) : (P.transcript x y c).bind next = (P.commit x y).bind fun (ts : T × P.State) => next (ts.1, P.respond x y ts.2 c)

Continuing after an honest transcript is continuing after the commitment with the honest response.

theorem Cslib.Crypto.Protocols.SigmaProtocol.conversation_eq_bind_transcript {X Y T C Z : Type u} (P : SigmaProtocol X Y T C Z) [Fintype C] [Nonempty C] (x : X) (y : Y) : P.conversation x y = do let c ← Probability.PMF.uniformOfFintype C let tz ← P.transcript x y c pure (tz.1, c, tz.2)

An honest execution samples the challenge first and then the prover's messages.

theorem Cslib.Crypto.Protocols.SigmaProtocol.Complete.accepts_of_mem_support_conversation {X Y T C Z : Type u} {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} [Fintype C] [Nonempty C] (h : P.Complete R) {x : X} {y : Y} (hxy : R x y) {tcz : T × C × Z} (htcz : tcz ∈ (P.conversation x y).support) : P.Accepts y tcz.1 tcz.2.1 tcz.2.2

Every honest conversation is accepting: the verifier always accepts the honest prover.

theorem Cslib.Crypto.Protocols.SigmaProtocol.SpecialHVZK.conversation_eq {X Y T C Z : Type u} {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} [Fintype C] [Nonempty C] {simulate : Y → C → PMF (T × Z)} (h : P.SpecialHVZK R simulate) {x : X} {y : Y} (hxy : R x y) : P.conversation x y = do let c ← Probability.PMF.uniformOfFintype C let tz ← simulate y c pure (tz.1, c, tz.2)

With a uniform challenge, the simulator reproduces the honest conversation law ([BS23], Definition 19.5 (ii)).