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_commit_output_depends_on_message (gp : Examples.GroupParam) (crs : PedersenCRS gp) (m₀ m₁ r : gp.Scalar) (hm : m₀ ≠ m₁) : pedersen_commit gp crs m₀ r ≠ pedersen_commit gp crs m₁ r

The Pedersen commitment C = g ^ m · h ^ r varies with the committed message: for fixed randomness, distinct messages give distinct commitments (the generator has prime order, so exp is injective). Perfect hiding therefore comes from the uniform randomness r, not from the commit function ignoring the message.

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.