Pedersen Commitment: UC Security via a Trapdoor Equivocator

Pedersen commitment over an abstract discrete-log group, proved UC-secure at error 0 (perfect security) with a non-trivial simulator.

Scope: the equivocation direction only

This file proves the equivocation direction of UC commitment: an honest committer against a corrupt receiver. In that direction Pedersen is perfectly hiding, and the CRS trapdoor lets the simulator produce a commitment before it learns the message and open it consistently afterwards. The bound is exactly ε = 0.

It does not cover the extraction direction (a corrupt committer, where the simulator must extract the committed message and the commitment must be binding). Perfectly-hiding Pedersen cannot provide that: hiding is information-theoretic, so a commitment carries no information the simulator could extract, and equivocation is the concrete witness that the same C opens to every message given the trapdoor. Realizing the full F_commit functionality — both directions — requires an extractable (equivalently, mixed / dual-mode) commitment, not a plain perfectly-hiding one. So the result here is one half of UC commitment, stated as such.

Modeling choice: reveal the exponent, not the group element

pedersen_real returns the exponent s = dlog C = m + t · r rather than the group element C = g ^ s itself. For a fixed generator, s ↦ g ^ s is a bijection, so the two carry the same information and the distributions are equivalent; working with the exponent makes the change-of-variables comparison against the ideal exponent direct.

Protocol

For a cyclic group G with generator g and CRS h = g ^ t:

• Commit(m): sample r, output C = g ^ m · h ^ r with decommitment r.
• Open(m, r): the verifier checks C = g ^ m · h ^ r.

UC security via the CRS trapdoor

The simulator knows the CRS trapdoor t (the discrete log of h):

• on commit, the ideal samples a uniform exponent s and sets C = g ^ s;
• on open of m, the simulator computes r = (s - m) / t, so that m + t · r = s.

In the real world the pair (s, r) with s = m + t · r is uniform because r is uniform; in the ideal world (s, r) with r = (s - m) / t is uniform because s is uniform and s ↦ (s - m) / t is a bijection (for t ≠ 0). The two joint distributions coincide, so the views are identically distributed.

Non-trivial simulator

pedersen_sim is not the adversary. Using the trapdoor t it computes fake randomness r from the ideal exponent s and the message m — genuine equivocation, retroactively opening a commitment produced without the message.

Interface types

• leak = Scalar × Scalar — the real world leaks the exponent s = m + t·r and the randomness r.
• sim_if = Scalar × Scalar — the ideal hands the simulator the exponent s and the message m. The simulator turns (s, m) into a view indistinguishable from (s, r).

CRS Setup

structure CatCrypt.Crypto.Commitment.PedersenUC.PedersenCRS (gp : Examples.GroupParam) : Type

CRS for Pedersen commitment: h = g ^ trapdoor. In the real protocol the trapdoor is unknown; the UC simulator knows it.

• h : gp.G

  The CRS public key h, a group element.

• trapdoor : gp.Scalar

  The trapdoor: the discrete log of h with respect to g.

• h_eq : self.h = gp.exp self.trapdoor

  CRS correctness: h = g ^ trapdoor.

Protocol

def CatCrypt.Crypto.Commitment.PedersenUC.pedersen_commit (gp : Examples.GroupParam) (crs : PedersenCRS gp) (m r : gp.Scalar) : gp.G

Pedersen commitment to m with randomness r: C = g ^ m · h ^ r.

Equations

• CatCrypt.Crypto.Commitment.PedersenUC.pedersen_commit gp crs m r = gp.groupMul (gp.exp m) (gp.groupExp crs.h r)

noncomputable def CatCrypt.Crypto.Commitment.PedersenUC.pedersen_real (gp : Examples.GroupParam) (crs : PedersenCRS gp) : gp.Scalar → Core.SPComp (Unit ⊕ gp.Scalar × gp.Scalar)

Real protocol: commit to m, revealing the exponent s = m + t · r of C = g ^ s and the randomness r. Returning the exponent rather than the group element makes the distribution comparison direct.

Equations

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

noncomputable def CatCrypt.Crypto.Commitment.PedersenUC.pedersen_ideal (gp : Examples.GroupParam) (_crs : PedersenCRS gp) : gp.Scalar → Core.SPComp (Unit ⊕ gp.Scalar × gp.Scalar)

Ideal functionality: sample a uniform exponent s and reveal (s, m) on the simulator interface.

Equations

• CatCrypt.Crypto.Commitment.PedersenUC.pedersen_ideal gp _crs m = do let s ← CatCrypt.Core.SPComp.sample gp.Scalar CatCrypt.Core.SPComp.pure (Sum.inr (s, m))

Non-Trivial Simulator

noncomputable def CatCrypt.Crypto.Commitment.PedersenUC.pedersen_sim (gp : Examples.GroupParam) (crs : PedersenCRS gp) (view : Type) (A : gp.Scalar × gp.Scalar → Core.SPComp view) : gp.Scalar × gp.Scalar → Core.SPComp view

The Pedersen simulator: from (s, m) it produces a fake (s, r) for the adversary using the CRS trapdoor t, computing r = (s - m) / t so that m + t · r = s.

Equations

• CatCrypt.Crypto.Commitment.PedersenUC.pedersen_sim gp crs view A (s, m) = A (s, gp.scalarDiv (gp.scalarSub s m) crs.trapdoor)

UC Specification

noncomputable def CatCrypt.Crypto.Commitment.PedersenUC.pedersenSpec (gp : Examples.GroupParam) (V : Type) : UCSpec

UC spec for Pedersen commitment: honest input is a message, the real world leaks (exponent, randomness), and the ideal world hands the simulator (exponent, message).

Equations

• CatCrypt.Crypto.Commitment.PedersenUC.pedersenSpec gp V = { hon := gp.Scalar, out := Unit, leak := gp.Scalar × gp.Scalar, sim_if := gp.Scalar × gp.Scalar, view := V }

Security Proof

noncomputable def CatCrypt.Crypto.Commitment.PedersenUC.affineEquiv (gp : Examples.GroupParam) (crs : PedersenCRS gp) (ht : crs.trapdoor ≠ gp.scalarZero) (m : gp.Scalar) : gp.Scalar ≃ gp.Scalar

The affine map r ↦ m + t · r is a bijection of Scalar when t ≠ 0.

Equations

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

theorem CatCrypt.Crypto.Commitment.PedersenUC.pedersen_view_eq (gp : Examples.GroupParam) (crs : PedersenCRS gp) (ht : crs.trapdoor ≠ gp.scalarZero) (m : gp.Scalar) (view : Type) (A : gp.Scalar × gp.Scalar → Core.SPComp view) : (pedersen_real gp crs m).bind (mapSum Core.SPComp.pure A) = (pedersen_ideal gp crs m).bind (mapSum Core.SPComp.pure (pedersen_sim gp crs view A))

The real and simulated views coincide pointwise: the change of variables r ↦ m + t · r couples the real randomness with the ideal exponent.

theorem CatCrypt.Crypto.Commitment.PedersenUC.pedersen_uc_secure (gp : Examples.GroupParam) (crs : PedersenCRS gp) (ht : crs.trapdoor ≠ gp.scalarZero) (V : Type) : UCEmulates 0 (pedersenSpec gp V) (pedersen_real gp crs) (pedersen_ideal gp crs)

Pedersen commitment with a CRS trapdoor realizes the equivocation direction of UC commitment at ε = 0 (perfect), with a non-trivial simulator. This is the honest-committer / corrupt-receiver direction: given (s, m) from the ideal, the simulator pedersen_sim equivocates by computing r = (s - m) / t and passing (s, r) to the adversary.

Scope: this does not cover the corrupt-committer / extraction direction — a perfectly-hiding commitment cannot be extractable, and full F_commit needs an extractable (mixed / dual-mode) commitment. (genuine UC)

Nice-to-have: the extraction direction

The complementary half — a corrupt committer, where the simulator extracts the committed message from C and the commitment is binding — is out of reach for this protocol, not merely unproved: plain Pedersen is perfectly hiding, so no extractor exists. Closing the gap to full F_commit means changing the primitive, not extending this proof: instantiate an extractable / dual-mode commitment (e.g. a hiding+extractable CRS mode, or an El-Gamal-style commitment whose CRS trapdoor is a decryption key), then state and prove the extraction direction against it. That belongs in a separate file for the extractable scheme; there is deliberately no extraction theorem here to fake.

This is not left open across CatCrypt: the full account — the F_commit functionality with both equivocation and extraction, an extractable commitment realizing it, and the plain-model impossibility — is developed in the larger CatCrypt UC development built on top of this basis (a Commitment/ tree with FCOM / Extraction / PlainModelImpossibility), which is outside this minimal-basis release. This file is the self-contained equivocation exemplar.