Sigma Protocol

This file defines a structure type for Σ-protocols.

structure SigmaAlg (S W PC SC Ω P : Type) (p : S → W → Bool) : Type 1

A sigma protocol for statements in S and witnesses in W, where p : X → W → Bool is the proposition that is proven by the Σ-protocol. Commitments are split into private and public parts in PC and SC resp. Verifier challenges are assumed to be drawn uniformly from Ω. Provers final proof responses are in P.

We have two types for the commitments in order to allow for a public part in PC and secret part in SC. Only the commitment in PC is revealed to the verifier, but the prove function may still use SC in generating a proof.

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

• commit (s : S) (w : W) : ProbComp (PC × SC)

  Given a statement s, make a commitment to prove that you have a valid witness w.

• respond (s : S) (w : W) (sc : SC) (ω : Ω) : ProbComp P

  Given a previous secret commitment sc, repond to the challenge ω

• verify (s : S) (pc : PC) (ω : Ω) (p : P) : Bool

  Deterministic function to check that the proof p satisfies the challenge ω.

• sim (s : S) : ProbComp PC

  Simulate public commitment generation while only knowing the statement.

• extract (ω₁ : Ω) (p₁ : P) (ω₂ : Ω) (p₂ : P) : ProbComp W

  Extract a witness to the statement from two proofs.