Chaum-Pedersen Protocol: Equality of Discrete Logarithms

The Chaum-Pedersen protocol is a Sigma protocol for proving equality of discrete logarithms. Given generators g and h of a cyclic group of prime order, the prover demonstrates knowledge of x such that u = g^x AND v = h^x, thereby proving that u and v share the same discrete logarithm with respect to g and h respectively, without revealing the exponent.

Protocol

• Statement: (g, h, u, v) where u = groupExp g x and v = groupExp h x
• Witness: x (the common exponent)
• Relation: R((g,h,u,v), x) <=> u = groupExp g x /\ v = groupExp h x
• Commit: Sample random r, send (a1, a2) = (groupExp g r, groupExp h r)
• Challenge: Random scalar e
• Response: z = r + e*x
• Verify: groupExp g z = groupMul a1 (groupExp u e) AND groupExp h z = groupMul a2 (groupExp v e)
• Simulate: Sample z, compute a1 = groupMul (groupExp g z) (groupInv (groupExp u e)), a2 = groupMul (groupExp h z) (groupInv (groupExp v e))
• Extract: From two transcripts (a, e, z) and (a, e', z'), extract x = (z-z')/(e-e')

Security properties

• chaumPedersen_complete -- completeness
• chaumPedersen_SHVZK_visible -- special honest-verifier zero-knowledge (given challenge)
• chaumPedersen_special_soundness -- special soundness (witness extraction)
• chaumPedersen_uc_secure -- UC security at eps = 0

References

• [Chaum & Pedersen, Wallet Databases with Observers, CRYPTO 1992]
• [Damgard, On Sigma Protocols]

Chaum-Pedersen Protocol Types

@[reducible, inline]

abbrev CatCryptCore.Examples.ChaumPedersen.CPStatement (gp : CatCrypt.Examples.GroupParam) : Type

Chaum-Pedersen statement: (g, h, u, v).

Equations

• CatCryptCore.Examples.ChaumPedersen.CPStatement gp = (gp.G × gp.G × gp.G × gp.G)

@[reducible, inline]

abbrev CatCryptCore.Examples.ChaumPedersen.CPWitness (gp : CatCrypt.Examples.GroupParam) : Type

Chaum-Pedersen witness: the common exponent x.

Equations

• CatCryptCore.Examples.ChaumPedersen.CPWitness gp = gp.Scalar

@[reducible, inline]

abbrev CatCryptCore.Examples.ChaumPedersen.CPMessage (gp : CatCrypt.Examples.GroupParam) : Type

Chaum-Pedersen commitment message: (r, groupExp g r, groupExp h r).

Equations

• CatCryptCore.Examples.ChaumPedersen.CPMessage gp = (gp.Scalar × gp.G × gp.G)

@[reducible, inline]

abbrev CatCryptCore.Examples.ChaumPedersen.CPChallenge (gp : CatCrypt.Examples.GroupParam) : Type

Chaum-Pedersen challenge: a random scalar.

Equations

• CatCryptCore.Examples.ChaumPedersen.CPChallenge gp = gp.Scalar

@[reducible, inline]

abbrev CatCryptCore.Examples.ChaumPedersen.CPResponse (gp : CatCrypt.Examples.GroupParam) : Type

Chaum-Pedersen response: z = r + e*x.

Equations

• CatCryptCore.Examples.ChaumPedersen.CPResponse gp = gp.Scalar

Chaum-Pedersen Relation

def CatCryptCore.Examples.ChaumPedersen.cpRelation (gp : CatCrypt.Examples.GroupParam) (stmt : CPStatement gp) (w : CPWitness gp) : Prop

The equality-of-discrete-logs relation: R((g, h, u, v), x) <=> u = groupExp g x /\ v = groupExp h x.

Equations

• CatCryptCore.Examples.ChaumPedersen.cpRelation gp stmt w = (stmt.2.2.1 = gp.groupExp stmt.1 w ∧ stmt.2.2.2 = gp.groupExp stmt.2.1 w)

Chaum-Pedersen Protocol Algorithms

noncomputable def CatCryptCore.Examples.ChaumPedersen.cpCommit (gp : CatCrypt.Examples.GroupParam) (stmt : CPStatement gp) (_w : CPWitness gp) : CatCrypt.Core.SPComp (CPMessage gp)

Chaum-Pedersen commitment: sample random r, return (r, groupExp g r, groupExp h r).

Equations

• CatCryptCore.Examples.ChaumPedersen.cpCommit gp stmt _w = do let r ← CatCrypt.Core.SPComp.sample gp.Scalar CatCrypt.Core.SPComp.pure (r, gp.groupExp stmt.1 r, gp.groupExp stmt.2.1 r)

noncomputable def CatCryptCore.Examples.ChaumPedersen.cpRespond (gp : CatCrypt.Examples.GroupParam) (_stmt : CPStatement gp) (w : CPWitness gp) (msg : CPMessage gp) (e : CPChallenge gp) : CatCrypt.Core.SPComp (CPResponse gp)

Chaum-Pedersen response: compute z = r + e*x.

Equations

• CatCryptCore.Examples.ChaumPedersen.cpRespond gp _stmt w msg e = CatCrypt.Core.SPComp.pure (gp.scalarAdd msg.1 (gp.scalarMul e w))

def CatCryptCore.Examples.ChaumPedersen.cpVerify (gp : CatCrypt.Examples.GroupParam) (stmt : CPStatement gp) (msg : CPMessage gp) (e : CPChallenge gp) (z : CPResponse gp) : Bool

Chaum-Pedersen verification.

Equations

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

noncomputable def CatCryptCore.Examples.ChaumPedersen.cpSimulate (gp : CatCrypt.Examples.GroupParam) (stmt : CPStatement gp) (e : CPChallenge gp) : CatCrypt.Core.SPComp (CPMessage gp × CPResponse gp)

Chaum-Pedersen simulator.

Equations

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

def CatCryptCore.Examples.ChaumPedersen.cpExtractor (gp : CatCrypt.Examples.GroupParam) (_stmt : CPStatement gp) (_msg : CPMessage gp) (e e' : CPChallenge gp) (z z' : CPResponse gp) : Option (CPWitness gp)

Chaum-Pedersen extractor.

Equations

• CatCryptCore.Examples.ChaumPedersen.cpExtractor gp _stmt _msg e e' z z' = if (e == e') = true then none else some (gp.scalarDiv (gp.scalarSub z z') (gp.scalarSub e e'))

Sigma Protocol Instance

@[implicit_reducible]

noncomputable def CatCryptCore.Examples.ChaumPedersen.chaumPedersenSigma (gp : CatCrypt.Examples.GroupParam) : CatCrypt.Examples.SigmaProtocol.SigmaProtocol

Chaum-Pedersen identification as a Sigma protocol.

Equations

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

Visible Transcript Equality

def CatCryptCore.Examples.ChaumPedersen.cpVisibleTranscriptEq (gp : CatCrypt.Examples.GroupParam) (t₁ t₂ : CatCrypt.Examples.SigmaProtocol.Transcript (chaumPedersenSigma gp)) : Prop

Visible transcript equality for Chaum-Pedersen: compares only the externally visible parts (a1, a2, e, z), excluding the internal randomness r.

Equations

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

Helper lemmas

theorem CatCryptCore.Examples.ChaumPedersen.groupExp_add_gen (gp : CatCrypt.Examples.GroupParam) (g : gp.G) (a b : gp.Scalar) : gp.groupExp g (gp.scalarAdd a b) = gp.groupMul (gp.groupExp g a) (gp.groupExp g b)

groupExp distributes: groupExp g (scalarAdd a b) = groupMul (groupExp g a) (groupExp g b).

theorem CatCryptCore.Examples.ChaumPedersen.groupInv_groupExp_gen (gp : CatCrypt.Examples.GroupParam) (g : gp.G) (e : gp.Scalar) : gp.groupInv (gp.groupExp g e) = gp.groupExp g (gp.scalarNeg e)

groupInv of groupExp: groupInv (groupExp g e) = groupExp g (scalarNeg e).

theorem CatCryptCore.Examples.ChaumPedersen.groupExp_groupExp_gen (gp : CatCrypt.Examples.GroupParam) (g : gp.G) (w e : gp.Scalar) : gp.groupExp (gp.groupExp g w) e = gp.groupExp g (gp.scalarMul w e)

groupExp composed: groupExp (groupExp g w) e = groupExp g (scalarMul w e). Proved via exp_surj + groupExp_exp + scalarMul_assoc.

Completeness

theorem CatCryptCore.Examples.ChaumPedersen.chaumPedersen_complete (gp : CatCrypt.Examples.GroupParam) (stmt : CPStatement gp) (w : CPWitness gp) (hrel : cpRelation gp stmt w) (r : gp.Scalar) (e : CPChallenge gp) : have msg := (r, gp.groupExp stmt.1 r, gp.groupExp stmt.2.1 r); have z := gp.scalarAdd r (gp.scalarMul e w); cpVerify gp stmt msg e z = true

Completeness for Chaum-Pedersen: honest execution always verifies.

Commitment recovery lemma

theorem CatCryptCore.Examples.ChaumPedersen.commitment_recovery (gp : CatCrypt.Examples.GroupParam) (g u : gp.G) (w r z e : gp.Scalar) (hu : u = gp.groupExp g w) (hz : z = gp.scalarAdd r (gp.scalarMul e w)) : gp.groupExp g r = gp.groupMul (gp.groupExp g z) (gp.groupInv (gp.groupExp u e))

The key algebraic identity: groupExp g r = groupMul (groupExp g z) (groupInv (groupExp u e)) when u = groupExp g w and z = r + e*w.

Cancellation helper for special soundness

theorem CatCryptCore.Examples.ChaumPedersen.cancel_add_neg (gp : CatCrypt.Examples.GroupParam) (ka t1 t2 : gp.Scalar) : gp.scalarAdd (gp.scalarAdd ka t1) (gp.scalarAdd (gp.scalarNeg ka) (gp.scalarNeg t2)) = gp.scalarAdd t1 (gp.scalarNeg t2)

Cancellation: (ka + t1) + (-ka + -t2) = t1 + (-t2).

theorem CatCryptCore.Examples.ChaumPedersen.scalarMul_div (gp : CatCrypt.Examples.GroupParam) (k x y : gp.Scalar) (hy : y ≠ gp.scalarZero) : gp.scalarDiv (gp.scalarMul k x) y = gp.scalarMul k (gp.scalarDiv x y)

Division distributes: scalarDiv (scalarMul k x) y = scalarMul k (scalarDiv x y).

SHVZK

theorem CatCryptCore.Examples.ChaumPedersen.chaumPedersen_SHVZK_visible (gp : CatCrypt.Examples.GroupParam) (stmt : (chaumPedersenSigma gp).Statement) (w : (chaumPedersenSigma gp).Witness) (e : (chaumPedersenSigma gp).Challenge) : (chaumPedersenSigma gp).relation stmt w → CatCrypt.Relational.rHoare (fun (x x_1 : CatCrypt.Core.Heap) => True) (CatCrypt.Examples.SigmaProtocol.realTranscript (chaumPedersenSigma gp) stmt w e) (CatCrypt.Examples.SigmaProtocol.simulatedTranscript (chaumPedersenSigma gp) stmt e) fun (t₁ : CatCrypt.Examples.SigmaProtocol.Transcript (chaumPedersenSigma gp)) (x : CatCrypt.Core.Heap) (t₂ : CatCrypt.Examples.SigmaProtocol.Transcript (chaumPedersenSigma gp)) (x_1 : CatCrypt.Core.Heap) => cpVisibleTranscriptEq gp t₁ t₂

SHVZK for Chaum-Pedersen (given challenge): the visible parts of real and simulated transcripts are identical.

Special Soundness

theorem CatCryptCore.Examples.ChaumPedersen.chaumPedersen_special_soundness (gp : CatCrypt.Examples.GroupParam) : CatCrypt.Examples.SigmaProtocol.SpecialSoundness (chaumPedersenSigma gp)

Special soundness for Chaum-Pedersen.

Visible Transcript and UC Security

The internal CPMessage includes the randomness r for threading between commit and respond. The visible transcript (what the adversary sees) projects out r, keeping only the group elements (a1, a2), the challenge e, and the response z. UC security is stated over these visible transcripts.

@[reducible, inline]

abbrev CatCryptCore.Examples.ChaumPedersen.CPVisibleTranscript (gp : CatCrypt.Examples.GroupParam) : Type

Visible Chaum-Pedersen transcript: (a1, a2, challenge, response).

Equations

• CatCryptCore.Examples.ChaumPedersen.CPVisibleTranscript gp = (gp.G × gp.G × gp.Scalar × gp.Scalar)

def CatCryptCore.Examples.ChaumPedersen.projectTranscript (gp : CatCrypt.Examples.GroupParam) (t : CatCrypt.Examples.SigmaProtocol.Transcript (chaumPedersenSigma gp)) : CPVisibleTranscript gp

Project a full transcript to its visible parts.

Equations

• CatCryptCore.Examples.ChaumPedersen.projectTranscript gp t = (t.message.2.1, t.message.2.2, t.challenge, t.response)

noncomputable def CatCryptCore.Examples.ChaumPedersen.cpRealVisible (gp : CatCrypt.Examples.GroupParam) (stmt : CPStatement gp) (w : CPWitness gp) : CatCrypt.Core.SPComp (CPVisibleTranscript gp)

Real visible transcript computation.

Equations

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

noncomputable def CatCryptCore.Examples.ChaumPedersen.cpSimVisible (gp : CatCrypt.Examples.GroupParam) (stmt : CPStatement gp) : CatCrypt.Core.SPComp (CPVisibleTranscript gp)

Simulated visible transcript computation.

Equations

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

def CatCryptCore.Examples.ChaumPedersen.cpSpec (gp : CatCrypt.Examples.GroupParam) (V : Type) : CatCrypt.Crypto.UCSpec

UC specification for visible Chaum-Pedersen transcripts.

Equations

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

noncomputable def CatCryptCore.Examples.ChaumPedersen.cpReal (gp : CatCrypt.Examples.GroupParam) (stmt : CPStatement gp) (w : CPWitness gp) : CatCrypt.Core.SPComp (Unit ⊕ CPVisibleTranscript gp)

Real Chaum-Pedersen protocol (visible output).

Equations

• CatCryptCore.Examples.ChaumPedersen.cpReal gp stmt w = CatCrypt.Core.SPComp.map Sum.inr (CatCryptCore.Examples.ChaumPedersen.cpRealVisible gp stmt w)

noncomputable def CatCryptCore.Examples.ChaumPedersen.cpIdeal (gp : CatCrypt.Examples.GroupParam) (stmt : CPStatement gp) : CatCrypt.Core.SPComp (Unit ⊕ CPVisibleTranscript gp)

Ideal Chaum-Pedersen functionality (visible output).

Equations

• CatCryptCore.Examples.ChaumPedersen.cpIdeal gp stmt = CatCrypt.Core.SPComp.map Sum.inr (CatCryptCore.Examples.ChaumPedersen.cpSimVisible gp stmt)

theorem CatCryptCore.Examples.ChaumPedersen.cp_real_vis_eq_sim (gp : CatCrypt.Examples.GroupParam) (stmt : CPStatement gp) (w : CPWitness gp) (hrel : cpRelation gp stmt w) : cpRealVisible gp stmt w = cpSimVisible gp stmt

The real and simulated visible transcript computations are equal.

After projecting out the internal randomness r, the bijection r ↦ z = r + e*w shows that the visible parts (g^r, h^r, e, z) of the real transcript and (g^z * u^{-e}, h^z * v^{-e}, e, z) of the simulated transcript have the same distribution, since both visible commitments equal g^r (resp. h^r) when u = g^w, v = h^w.

theorem CatCryptCore.Examples.ChaumPedersen.chaumPedersen_uc_secure (gp : CatCrypt.Examples.GroupParam) (V : Type) (stmt : CPStatement gp) (w : CPWitness gp) (hrel : cpRelation gp stmt w) : CatCrypt.Crypto.UCEmulates 0 (cpSpec gp V) (fun (x : (cpSpec gp V).hon) => cpReal gp stmt w) fun (x : (cpSpec gp V).hon) => cpIdeal gp stmt

The Chaum-Pedersen protocol is perfectly UC-secure: UCEmulates 0.