Pedersen commitments over a prime-order group family

Over a PrimeOrderGroupFamily, Pedersen's commitment scheme ([Ped92], Section 3, Theorem 3.1; [BS23], Section 8.12, Definition 8.8, Section 10.6.1, Fact 10.3 and Theorem 10.4, and Exercise 20.5) uses a group description d and a public commitment key h = α • g : F.Carrier d generated by a secret exponent α : ZMod (F.order d). To commit to a message m : ZMod (F.order d) with randomness r : ZMod (F.order d), the committer computes

pedersenCommit d h m r = m • g + r • h.

On encoded group elements and natural-number exponents, encodePedersenCommit computes F.encode d (F.pedersenCommit d h m r) in polynomial time from (d, encode h, m, r) using F.encode d (F.generator d), F.smul, and F.add.

We instantiate the general public-parameter CommitmentScheme (pedersenScheme) with canonical binary message words (ValidPedersenMessage), commitment-and-opening pair law (pedersenCommitPairLaw), and verification algorithm pedersenVerify (V(m, c, o)), and establish:

1. Algebraic and homomorphic laws (pedersenCommit_zero, pedersenCommit_add, pedersenCommit_neg, pedersenCommit_sub, pedersenCommit_smul) and polynomial-time encoded evaluation (encodePedersenCommit, encodePedersenCommit_encode, computableInPolyTime_encodePedersenCommit).
2. Unconditional hiding (pedersenCommitLaw_eq_uniform_of_ne_zero, pedersenCommitLaw_eq_of_ne_zero, pedersenHidingForKey_eq_of_ne_zero, advantage_pedersenHidingGame_le, negligible_advantage_pedersenHidingGame, pedersenScheme_statisticalHiding): for every non-identity commitment key h ≠ 0, a uniform blinding exponent r ← PMF.uniformOfFintype (ZMod (F.order d)) makes pedersenCommit d h m r uniformly distributed on F.Carrier d and independent of m. Consequently, at any fixed d and h ≠ 0, the chosen-message hiding distributions for bit = false and bit = true in F.pedersenScheme.hidingForKey ⟨d, h⟩ are identical against every (even computationally unbounded) two-stage adversary Encryption.WordAdversary. When the key exponent α ← PMF.uniformOfFintype (ZMod (F.order d)) is drawn uniformly from all of ZMod (F.order d) (matching discreteLogGame and [BS23], Exercise 20.5), the degenerate key α = 0 occurs with probability 1 / F.order d, bounding any unbounded adversary's hiding advantage in F.pedersenScheme.hidingGame (F.pedersenKeyDist setup) by 1 / m whenever supported groups have order at least m.
3. Computational binding under the discrete-logarithm assumption (pedersenVerify, pedersenExtractNat, pedersenToDLAdversary, succProbability_pedersenBindingGame_le_discreteLogGame, isPPTOn_pedersenToDLAdversary, DiscreteLog.pedersenBinding, DiscreteLog.pedersenScheme_binding): any verified double opening (c, (m₀, o₀), (m₁, o₁)) with m₀ ≠ m₁ and pedersenVerify d h mᵢ c oᵢ = true for i ∈ {0, 1} under h = α • g has (ofBits m₀ : ZMod q) ≠ (ofBits m₁ : ZMod q), forces (ofBits o₀ : ZMod q) ≠ (ofBits o₁ : ZMod q), and yields α = (o₁ - o₀)⁻¹ * (m₀ - m₁) modulo q ([Ped92], Section 3, Theorem 3.1; [BS23], Section 10.6.1, Fact 10.3 and Theorem 10.4), computed in polynomial time via Fermat's little theorem (pedersenExtractNat). This gives an exact zero-loss reduction from F.pedersenScheme.bindingGame to discreteLogGame.

Main definitions

• Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit, Cslib.Crypto.PrimeOrderGroupFamily.encodePedersenCommit: algebraic and encoded Pedersen commitment evaluation.
• Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommitLaw, Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommitPairLaw: the commitment element distribution and the (c, o) commitment-and-opening pair distribution for a uniform blinding exponent r : ZMod (F.order d).
• Cslib.Crypto.PrimeOrderGroupFamily.ValidPedersenMessage, Cslib.Crypto.PrimeOrderGroupFamily.pedersenVerify: canonical message space and verification algorithm V(m, c, o).
• Cslib.Crypto.PrimeOrderGroupFamily.PedersenKey, Cslib.Crypto.PrimeOrderGroupFamily.pedersenKeyDist, Cslib.Crypto.PrimeOrderGroupFamily.pedersenScheme: Pedersen commitment packaged as a public-parameter CommitmentScheme.
• Cslib.Crypto.PrimeOrderGroupFamily.pedersenExtractNat, Cslib.Crypto.PrimeOrderGroupFamily.pedersenToDLAdversary: discrete-logarithm extractor and reduction from a binding adversary.

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit_add, Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit_smul, Cslib.Crypto.PrimeOrderGroupFamily.encodePedersenCommit_encode, Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodePedersenCommit: homomorphic laws and polynomial-time encoded commitment evaluation.
• Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommitLaw_eq_uniform_of_ne_zero, Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommitLaw_eq_of_ne_zero, Cslib.Crypto.PrimeOrderGroupFamily.pedersenHidingForKey_eq_of_ne_zero, Cslib.Crypto.PrimeOrderGroupFamily.advantage_pedersenHidingGame_le, Cslib.Crypto.PrimeOrderGroupFamily.negligible_advantage_pedersenHidingGame, Cslib.Crypto.PrimeOrderGroupFamily.pedersenScheme_statisticalHiding: perfect hiding for h ≠ 0 and unconditional 1 / m hiding bound over uniform α : ZMod (F.order d).
• Cslib.Crypto.PrimeOrderGroupFamily.succProbability_pedersenBindingGame_le_discreteLogGame, Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_pedersenToDLAdversary, Cslib.Crypto.PrimeOrderGroupFamily.DiscreteLog.pedersenBinding, Cslib.Crypto.PrimeOrderGroupFamily.DiscreteLog.pedersenScheme_binding: computational binding under the discrete-logarithm assumption.

References

• T. P. Pedersen, Non-Interactive and Information-Theoretic Secure Verifiable Secret Sharing, Section 3, Theorem 3.1.
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 8.12 (Definition 8.8, p. 344), Section 10.6.1 (Fact 10.3 and Theorem 10.4, pp. 414–415), and Exercise 20.5 (pp. 843–844).

Algebraic and encoded Pedersen commitments

def Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) (m r : ZMod (F.order d)) : F.Carrier d

Algebraic Pedersen commitment ([Ped92], Section 3; [BS23], Section 10.6.1 and Exercise 20.5): commit to message m : ZMod (F.order d) with randomness r : ZMod (F.order d) under commitment key h : F.Carrier d as m • g + r • h.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit_zero (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) : F.pedersenCommit d h 0 0 = 0

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit_add (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) (m₁ r₁ m₂ r₂ : ZMod (F.order d)) : F.pedersenCommit d h (m₁ + m₂) (r₁ + r₂) = F.pedersenCommit d h m₁ r₁ + F.pedersenCommit d h m₂ r₂

Additive homomorphism of Pedersen commitments: committing to (m₁ + m₂, r₁ + r₂) equals the sum of the individual commitments.

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit_neg (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) (m r : ZMod (F.order d)) : F.pedersenCommit d h (-m) (-r) = -F.pedersenCommit d h m r

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit_sub (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) (m₁ r₁ m₂ r₂ : ZMod (F.order d)) : F.pedersenCommit d h (m₁ - m₂) (r₁ - r₂) = F.pedersenCommit d h m₁ r₁ - F.pedersenCommit d h m₂ r₂

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit_smul (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) (c m r : ZMod (F.order d)) : F.pedersenCommit d h (c * m) (c * r) = c • F.pedersenCommit d h m r

Scalar-multiplication homomorphism of Pedersen commitments.

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit_smul_generator (F : PrimeOrderGroupFamily) (d : F.Desc) (α m r : ZMod (F.order d)) : F.pedersenCommit d (α • F.generator d) m r = (m + r * α) • F.generator d

Under a commitment key h = α • g, pedersenCommit d (α • g) m r = (m + r * α) • g.

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommit_smul_generator_eq_iff (F : PrimeOrderGroupFamily) (d : F.Desc) (α m₀ r₀ m₁ r₁ : ZMod (F.order d)) : F.pedersenCommit d (α • F.generator d) m₀ r₀ = F.pedersenCommit d (α • F.generator d) m₁ r₁ ↔ m₀ + r₀ * α = m₁ + r₁ * α

Two openings (m₀, r₀) and (m₁, r₁) produce the same commitment under h = α • g if and only if m₀ + r₀ * α = m₁ + r₁ * α in ZMod (F.order d).

def Cslib.Crypto.PrimeOrderGroupFamily.encodePedersenCommit (F : PrimeOrderGroupFamily) (input : F.Desc × List Bool × ℕ × ℕ) : List Bool

Pedersen commitment on encoded group elements: given (d, encode h, m, r), compute encode (m • g + r • h).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodePedersenCommit_encode (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) (m r : ℕ) : F.encodePedersenCommit (d, F.encode d h, m, r) = F.encode d (F.pedersenCommit d h ↑m ↑r)

encodePedersenCommit computes F.encode d (F.pedersenCommit d h m r) on encoded group elements.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodePedersenCommit (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime F.encodePedersenCommit (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))) Turing.MultiTapeTM.encBits

Encoded Pedersen commitment evaluation is computable in polynomial time.

Unconditional hiding and CommitmentScheme packaging

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommitLaw (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) (m : ZMod (F.order d)) : PMF (F.Carrier d)

The distribution of F.pedersenCommit d h m r when r is drawn uniformly from ZMod (F.order d).

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommitLaw_eq_uniform_of_ne_zero (F : PrimeOrderGroupFamily) (d : F.Desc) {h : F.Carrier d} (hh : h ≠ 0) (m : ZMod (F.order d)) : F.pedersenCommitLaw d h m = PMF.map (fun (x : ZMod (F.order d)) => x • F.generator d) (Probability.PMF.uniformOfFintype (ZMod (F.order d)))

Perfect hiding for any non-identity commitment key h ≠ 0 ([Ped92], Section 3, Theorem 3.1): for every message m : ZMod (F.order d), F.pedersenCommitLaw d h m equals the uniform distribution (PMF.uniformOfFintype (ZMod (F.order d))).map (· • F.generator d) on F.Carrier d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommitLaw_eq_of_ne_zero (F : PrimeOrderGroupFamily) (d : F.Desc) {h : F.Carrier d} (hh : h ≠ 0) (m₀ m₁ : ZMod (F.order d)) : F.pedersenCommitLaw d h m₀ = F.pedersenCommitLaw d h m₁

Perfect hiding ([Ped92], Section 3, Theorem 3.1): for any h ≠ 0 and any two messages m₀, m₁ : ZMod (F.order d), the commitment distributions F.pedersenCommitLaw d h m₀ and F.pedersenCommitLaw d h m₁ are identical.

theorem Cslib.Crypto.PrimeOrderGroupFamily.uniform_pedersenCommit (F : PrimeOrderGroupFamily) {β : Type u_1} (d : F.Desc) {h : F.Carrier d} (hh : h ≠ 0) (m : ZMod (F.order d)) (f : F.Carrier d → PMF β) : ((Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (r : ZMod (F.order d)) => f (F.pedersenCommit d h m r)) = (Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (γ : ZMod (F.order d)) => f (γ • F.generator d)

Bind form of pedersenCommitLaw_eq_uniform_of_ne_zero: for any h ≠ 0 and message m, sampling r ← PMF.uniformOfFintype (ZMod (F.order d)) and passing F.pedersenCommit d h m r to a continuation f has the same distribution as sampling γ ← PMF.uniformOfFintype (ZMod (F.order d)) and passing γ • F.generator d.

def Cslib.Crypto.PrimeOrderGroupFamily.ValidPedersenMessage (F : PrimeOrderGroupFamily) (d : F.Desc) (m : List Bool) : Prop

A message word m : List Bool is a canonical Pedersen message for group description d if ofBits m < F.order d and m is the canonical binary representation (ofBits m).bits. Requiring canonical binary representation ensures that distinct message words in the message space represent distinct elements of ZMod (F.order d).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.pedersenCommitPairLaw (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) (m : ZMod (F.order d)) : PMF (List Bool × List Bool)

The distribution of (F.encode d (F.pedersenCommit d h m r), r.val.bits) (encoded commitment string and canonical binary opening string) when r is drawn uniformly from ZMod (F.order d).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.map_fst_pedersenCommitPairLaw (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) (m : ZMod (F.order d)) : PMF.map Prod.fst (F.pedersenCommitPairLaw d h m) = PMF.map (F.encode d) (F.pedersenCommitLaw d h m)

The commitment-string marginal of pedersenCommitPairLaw is (pedersenCommitLaw d h m).map (F.encode d).

def Cslib.Crypto.PrimeOrderGroupFamily.pedersenVerify (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) (m c o : List Bool) : Bool

Pedersen commitment verification V(m, c, o) ([BS23], Section 8.12, p. 344, and Section 10.6.1, p. 414; [Ped92], Section 3): verify that m is a canonical message word for d (ofBits m < F.order d and (ofBits m).bits = m) and that recomputing the commitment from (ofBits m, ofBits o) under (d, h) yields c.

theorem Cslib.Crypto.PrimeOrderGroupFamily.validPedersenMessage_of_pedersenVerify (F : PrimeOrderGroupFamily) {d : F.Desc} {h : F.Carrier d} {m c o : List Bool} (hv : F.pedersenVerify d h m c o = true) : F.ValidPedersenMessage d m

pedersenVerify accepts only canonical Pedersen message words (ValidPedersenMessage).

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenVerify_of_mem_support_pedersenCommitPairLaw (F : PrimeOrderGroupFamily) (d : F.Desc) (h : F.Carrier d) {m : List Bool} {co : List Bool × List Bool} (hm : F.ValidPedersenMessage d m) (hco : co ∈ (F.pedersenCommitPairLaw d h ↑(Turing.MultiTapeTM.ofBits m)).support) : F.pedersenVerify d h m co.1 co.2 = true

Correctness of pedersenVerify: every (c, o) in the support of pedersenCommitPairLaw d h (ofBits m) for a canonical message word m is accepted by pedersenVerify d h m c o.

@[reducible, inline]

abbrev Cslib.Crypto.PrimeOrderGroupFamily.PedersenKey (F : PrimeOrderGroupFamily) : Type

A Pedersen commitment key over F: a group description d : F.Desc together with a public group element h : F.Carrier d.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.pedersenKeyDist (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (n : ℕ) : PMF F.PedersenKey

Draw d ← setup n and a uniform key exponent α ← PMF.uniformOfFintype (ZMod (F.order d)), returning the Pedersen key ⟨d, α • g⟩ ([BS23], Exercise 20.5, pp. 843–844).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.pedersenScheme (F : PrimeOrderGroupFamily) : CommitmentScheme F.PedersenKey

Pedersen's commitment scheme as an instance of the general public-parameter CommitmentScheme ([BS23], Section 8.12, Definition 8.8, p. 344, and Section 10.6.1, p. 414; [Ped92], Section 3).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenScheme_encodeKey (F : PrimeOrderGroupFamily) (k : F.PedersenKey) : F.pedersenScheme.encodeKey k = (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) (k.fst, F.encode k.fst k.snd)

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenHidingForKey_eq_of_ne_zero (F : PrimeOrderGroupFamily) (d : F.Desc) {h : F.Carrier d} (hh : h ≠ 0) (adversary : Encryption.WordAdversary) (b₁ b₂ : Bool) (n : ℕ) : F.pedersenScheme.hidingForKey ⟨d, h⟩ adversary b₁ n = F.pedersenScheme.hidingForKey ⟨d, h⟩ adversary b₂ n

For any non-identity commitment key h ≠ 0, F.pedersenScheme.hidingForKey ⟨d, h⟩ produces the exact same output distribution for any two hidden bits b₁ and b₂, against every (even computationally unbounded) Encryption.WordAdversary.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_pedersenHidingForKey_eq_zero (F : PrimeOrderGroupFamily) (d : F.Desc) {h : F.Carrier d} (hh : h ≠ 0) (adversary : Encryption.WordAdversary) (n : ℕ) : (F.pedersenScheme.hidingForKey ⟨d, h⟩ adversary false n).advantage (F.pedersenScheme.hidingForKey ⟨d, h⟩ adversary true n) = 0

At any non-identity commitment key h ≠ 0, the hiding advantage of any (computationally unbounded) adversary between bit = false and bit = true is 0.

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenHidingGame_apply_true_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : Encryption.WordAdversary) (b₁ b₂ : Bool) (n m : ℕ) (hm : ∀ d ∈ (setup n).support, m ≤ F.order d) : (F.pedersenScheme.hidingGame (F.pedersenKeyDist setup) adversary b₁ n) true ≤ (F.pedersenScheme.hidingGame (F.pedersenKeyDist setup) adversary b₂ n) true + (↑m)⁻¹

When every supported group at parameter n has order at least m, changing the hidden bit from b₁ to b₂ changes acceptance probability in F.pedersenScheme.hidingGame (F.pedersenKeyDist setup) by at most 1 / m (arising solely from the 1 / F.order d probability of sampling the degenerate key α = 0).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_pedersenHidingGame_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : Encryption.WordAdversary) (n m : ℕ) (hm0 : 0 < m) (hm : ∀ d ∈ (setup n).support, m ≤ F.order d) : (F.pedersenScheme.hidingGame (F.pedersenKeyDist setup) adversary false n).advantage (F.pedersenScheme.hidingGame (F.pedersenKeyDist setup) adversary true n) ≤ 1 / ↑m

Unconditional hiding bound for Pedersen commitments: when every supported group at parameter n has order at least m > 0, any (even computationally unbounded) Encryption.WordAdversary has distinguishing advantage at most 1 / m in F.pedersenScheme.hidingGame (F.pedersenKeyDist setup).

theorem Cslib.Crypto.PrimeOrderGroupFamily.negligible_advantage_pedersenHidingGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : Encryption.WordAdversary) {m : ℕ → ℕ} (hm0 : ∀ (n : ℕ), 0 < m n) (hm : ∀ (n : ℕ), ∀ d ∈ (setup n).support, m n ≤ F.order d) (hinv : Negligible fun (n : ℕ) => 1 / ↑(m n)) : Negligible fun (n : ℕ) => (F.pedersenScheme.hidingGame (F.pedersenKeyDist setup) adversary false n).advantage (F.pedersenScheme.hidingGame (F.pedersenKeyDist setup) adversary true n)

Asymptotic unconditional hiding of Pedersen commitments ([Ped92], Section 3, Theorem 3.1; [BS23], Section 8.12, Definition 8.8, and Exercise 20.5): when every supported group at parameter n has order at least m n > 0 and 1 / m n is negligible, every (even computationally unbounded) Encryption.WordAdversary has negligible advantage in F.pedersenScheme.hidingGame (F.pedersenKeyDist setup).

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenScheme_statisticalHiding (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) {m : ℕ → ℕ} (hm0 : ∀ (n : ℕ), 0 < m n) (hm : ∀ (n : ℕ), ∀ d ∈ (setup n).support, m n ≤ F.order d) (hinv : Negligible fun (n : ℕ) => 1 / ↑(m n)) : F.pedersenScheme.StatisticalHiding (F.pedersenKeyDist setup)

Statistical hiding (CommitmentScheme.StatisticalHiding) of pedersenScheme ([Ped92], Section 3, Theorem 3.1; [BS23], Section 8.12, Definition 8.8, and Exercise 20.5).

Computational binding under the discrete-logarithm assumption

def Cslib.Crypto.PrimeOrderGroupFamily.pedersenExtractNat (q m₀ r₀ m₁ r₁ : ℕ) : ℕ

Extract the discrete logarithm (r₁ - r₀)⁻¹ * (m₀ - m₁) mod q from a Pedersen commitment collision ((m₀, r₀), (m₁, r₁)) ([Ped92], Section 3, Theorem 3.1; [BS23], Section 10.6.1, Fact 10.3, p. 415), computing the modular inverse via Fermat's little theorem as a (q - 2)-th power.

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenExtractNat_cast {q : ℕ} [Fact (Nat.Prime q)] {m₀ r₀ m₁ r₁ : ℕ} (hr : ↑r₁ ≠ ↑r₀) : ↑(pedersenExtractNat q m₀ r₀ m₁ r₁) = (↑r₁ - ↑r₀)⁻¹ * (↑m₀ - ↑m₁)

Fermat's little theorem gives the modular inverse in pedersenExtractNat whenever (r₁ : ZMod q) ≠ (r₀ : ZMod q).

theorem Cslib.Crypto.PrimeOrderGroupFamily.pedersenExtractNat_eq_of_isBindingCollision (F : PrimeOrderGroupFamily) (d : F.Desc) (α : ZMod (F.order d)) {out : List Bool × (List Bool × List Bool) × List Bool × List Bool} (hcoll : F.pedersenScheme.isBindingCollision ⟨d, α • F.generator d⟩ out = true) : ↑(pedersenExtractNat (F.order d) (Turing.MultiTapeTM.ofBits out.2.1.1) (Turing.MultiTapeTM.ofBits out.2.1.2) (Turing.MultiTapeTM.ofBits out.2.2.1) (Turing.MultiTapeTM.ofBits out.2.2.2)) = α

Any valid Pedersen binding collision (c, (m₀, o₀), (m₁, o₁)) under h = α • g recovers α via pedersenExtractNat ([Ped92], Section 3, Theorem 3.1; [BS23], Section 10.6.1, Fact 10.3).

def Cslib.Crypto.PrimeOrderGroupFamily.pedersenToDLAdversary (F : PrimeOrderGroupFamily) (adversary : ℕ → List Bool → ProbComp (List Bool × (List Bool × List Bool) × List Bool × List Bool)) (n : ℕ) (input : F.Desc × List Bool) : ProbComp (List Bool)

Turn a pedersenScheme binding adversary into a discrete-logarithm adversary by passing the encoded Pedersen key encPair F.encDesc encBits input and extracting pedersenExtractNat in binary from the two candidate openings ([BS23], Section 10.6.1, Theorem 10.4, pp. 414–415).

theorem Cslib.Crypto.PrimeOrderGroupFamily.succProbability_pedersenBindingGame_le_discreteLogGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : ℕ → List Bool → ProbComp (List Bool × (List Bool × List Bool) × List Bool × List Bool)) (n : ℕ) : (F.pedersenScheme.bindingGame (F.pedersenKeyDist setup) adversary n).succProbability ≤ (F.discreteLogGame setup (F.pedersenToDLAdversary adversary) n).succProbability

Exact binding-to-discrete-logarithm reduction ([BS23], Section 10.6.1, Theorem 10.4, pp. 414–415; [Ped92], Section 3, Theorem 3.1): for every security parameter n, the success probability of adversary in F.pedersenScheme.bindingGame (F.pedersenKeyDist setup) is at most the discrete-logarithm success probability of pedersenToDLAdversary adversary.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_pedersenToDLAdversary (F : PrimeOrderGroupFamily) {adversary : ℕ → List Bool → ProbComp (List Bool × (List Bool × List Bool) × List Bool × List Bool)} (hA : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) fun (input : ℕ × List Bool) => adversary input.1 input.2) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (input : ℕ × F.Desc × List Bool) => F.pedersenToDLAdversary adversary input.1 input.2

pedersenToDLAdversary is uniform strict PPT whenever the binding adversary is.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DiscreteLog.pedersenBinding {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} (hDL : F.DiscreteLog setup) (adversary : ℕ → List Bool → ProbComp (List Bool × (List Bool × List Bool) × List Bool × List Bool)) (hA : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) fun (input : ℕ × List Bool) => adversary input.1 input.2) : Negligible fun (n : ℕ) => (F.pedersenScheme.bindingGame (F.pedersenKeyDist setup) adversary n).succProbability

Computational binding of Pedersen commitments under the discrete-logarithm assumption ([Ped92], Section 3, Theorem 3.1; [BS23], Section 8.12, Definition 8.8, and Section 10.6.1, Theorem 10.4): if F.DiscreteLog setup holds, every uniform strict PPT adversary succeeds in F.pedersenScheme.bindingGame (F.pedersenKeyDist setup) with negligible probability.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DiscreteLog.pedersenScheme_binding {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} (hDL : F.DiscreteLog setup) : F.pedersenScheme.Binding (F.pedersenKeyDist setup)

Computational binding (CommitmentScheme.Binding) of pedersenScheme under the discrete-logarithm assumption ([Ped92], Section 3, Theorem 3.1; [BS23], Section 8.12, Definition 8.8, and Section 10.6.1, Theorem 10.4).