Σ-Protocol to Honest-Verifier UC Zero-Knowledge via a Witness-Free Simulator

A Σ-protocol with special honest-verifier zero-knowledge (SHVZK) yields a UC-secure honest-verifier / public-coin zero-knowledge proof at error 0 (perfect ZK), with a non-trivial simulator that never uses the witness.

Scope

The protocol itself samples the challenge, e ← SPComp.sample sp.Challenge (see sigma_real), so the verifier is public-coin: it draws e uniformly and independently of the commitment. The result is therefore honest-verifier UC-ZK. SHVZK alone does not give malicious-verifier ZK, and this file does not claim it: lifting to a verifier that chooses e adaptively as a function of the commitment requires an additional mechanism — a challenge commitment (the verifier commits to e before seeing a) or a Fiat–Shamir transform in the random-oracle model.

sigma_uc_zk_secure covers the ZK / simulation direction only — it shows the real prover's view is reproducible without the witness. It says nothing about knowledge soundness: there is no extractor here, so this is not a full realization of an F_ZK proof-of-knowledge functionality (which also requires extracting a witness from a convincing prover, e.g. via special soundness and rewinding).

The transformation

Given a Σ-protocol (commit, respond, simulate):

• the real prover knows the witness w and produces a transcript (a, e, z) via commit, a uniform (public-coin) challenge, then respond;
• the UC-ZK simulator does not know w: it samples a challenge e and runs simulate x e to produce (a, z) backwards.

SHVZK guarantees that the simulated transcript (a, e, z) is distributed exactly as a real one, so the two views coincide even though the simulator never uses the witness.

Non-trivial simulator

sigma_uc_sim calls simulate in place of the real prover's commit/respond:

• real: commit x w → (a, e, z) — uses w;
• simulated: simulate x e → (a, z) — witness-free.

Producing valid-looking transcripts without the witness is exactly the zero-knowledge property.

Interface types

• leak = Transcript — the real world leaks the full transcript (a, e, z).
• sim_if = Statement — the ideal hands the simulator only the statement x.

References

• [Damgård, On Σ-Protocols]

Transcript

structure CatCrypt.Crypto.ZK.SigmaUCZK.Transcript (sp : Examples.SigmaProtocol.SigmaProtocol) : Type

A Σ-protocol transcript: commitment, challenge, response.

• commitment : sp.Message

  The commitment (first message).

• challenge : sp.Challenge

  The challenge.

• response : sp.Response

  The response.

Real Protocol

noncomputable def CatCrypt.Crypto.ZK.SigmaUCZK.sigma_real (sp : Examples.SigmaProtocol.SigmaProtocol) : sp.Statement × sp.Witness → Core.SPComp (Unit ⊕ Transcript sp)

Real ZK prover: on input (x, w) with R(x, w), runs the honest protocol and reveals the full transcript (a, e, z).

Equations

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

Ideal Functionality

noncomputable def CatCrypt.Crypto.ZK.SigmaUCZK.sigma_ideal (sp : Examples.SigmaProtocol.SigmaProtocol) : sp.Statement × sp.Witness → Core.SPComp (Unit ⊕ sp.Statement)

Ideal ZK: reveals only the statement, neither the witness nor the transcript. The simulator receives x and must produce a transcript without w.

Equations

• CatCrypt.Crypto.ZK.SigmaUCZK.sigma_ideal sp (x_1, w) = CatCrypt.Core.SPComp.pure (Sum.inr x_1)

Non-Trivial Simulator

noncomputable def CatCrypt.Crypto.ZK.SigmaUCZK.sigma_uc_sim (sp : Examples.SigmaProtocol.SigmaProtocol) (view : Type) (A : Transcript sp → Core.SPComp view) : sp.Statement → Core.SPComp view

UC-ZK simulator: given only the statement x, sample a challenge e, run simulate x e to obtain (a, z), and hand the transcript (a, e, z) to the adversary. Non-trivial because it calls simulate rather than the honest commit/respond; SHVZK guarantees the same distribution.

Equations

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

UC Specification

noncomputable def CatCrypt.Crypto.ZK.SigmaUCZK.sigmaUCZKSpec (sp : Examples.SigmaProtocol.SigmaProtocol) (V : Type) : UCSpec

UC spec for Σ-protocol UC-ZK: honest input is (Statement × Witness), the real world leaks the full Transcript, and the ideal hands the simulator only the Statement.

Equations

• CatCrypt.Crypto.ZK.SigmaUCZK.sigmaUCZKSpec sp V = { hon := sp.Statement × sp.Witness, out := Unit, leak := CatCrypt.Crypto.ZK.SigmaUCZK.Transcript sp, sim_if := sp.Statement, view := V }

SHVZK Assumption

def CatCrypt.Crypto.ZK.SigmaUCZK.SHVZK (sp : Examples.SigmaProtocol.SigmaProtocol) : Prop

Special honest-verifier zero-knowledge: for every statement x, witness w, and challenge e, the honestly generated (a, z) and the simulated (a, z) have the same distribution. This is what makes the witness-free simulator indistinguishable from the real prover.

Equations

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

Nice-to-have (not formalized here)

Two natural extensions, each requiring machinery this file does not build:

• Malicious-verifier ZK. Replace the protocol's SPComp.sample sp.Challenge by a challenge chosen by an adversarial verifier V* (possibly depending on the commitment a), and restore honesty via a challenge commitment (the verifier commits to e before seeing a) or a Fiat–Shamir hash e := H(x, a) in the random-oracle model. The simulator then programs the random oracle instead of freely sampling e, and SHVZK is invoked at the programmed challenge.
• Knowledge soundness / extractor. Add a witness extractor from two accepting transcripts that share a commitment but have distinct challenges (special soundness) together with a rewinding argument, giving the soundness half of a full F_ZK proof-of-knowledge functionality. sigma_uc_zk_secure proves only the simulation direction.

Both are developed in the larger CatCrypt UC development built on top of this basis (outside this minimal-basis release): a ProofOfKnowledge module supplies the knowledge extractor via special soundness plus the forking/rewinding argument (sigma_is_pok), and a Fiat–Shamir layer supplies the malicious-verifier NIZK with a random-oracle-programming simulator. This file is the self-contained honest-verifier simulation exemplar.

Security Proof

theorem CatCrypt.Crypto.ZK.SigmaUCZK.sigma_view_eq (sp : Examples.SigmaProtocol.SigmaProtocol) (hshvzk : SHVZK sp) (x : sp.Statement) (w : sp.Witness) (V : Type) (A : Transcript sp → Core.SPComp V) : (sigma_real sp (x, w)).bind (mapSum Core.SPComp.pure A) = (sigma_ideal sp (x, w)).bind (mapSum Core.SPComp.pure (sigma_uc_sim sp V A))

Under SHVZK the real and simulated views coincide pointwise.

theorem CatCrypt.Crypto.ZK.SigmaUCZK.sigma_uc_zk_secure (sp : Examples.SigmaProtocol.SigmaProtocol) (hshvzk : SHVZK sp) (V : Type) : UCEmulates 0 (sigmaUCZKSpec sp V) (sigma_real sp) (sigma_ideal sp)

A Σ-protocol with SHVZK gives honest-verifier UC zero-knowledge at ε = 0 (perfect ZK), with a witness-free simulator. The protocol is public-coin: it samples the challenge e ← SPComp.sample sp.Challenge in sigma_real, so this is honest-verifier UC-ZK, not malicious-verifier UC-ZK (SHVZK alone does not give the latter — that needs a challenge commitment or a ROM Fiat–Shamir transform). The theorem covers the ZK / simulation direction only: sigma_uc_sim reproduces the prover's view via simulate, without the witness; it does not establish knowledge soundness (there is no extractor). (genuine UC)