From 592d9d9e4990300cbcccffc621a0396b6c450bab Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 05:26:10 -0400 Subject: [PATCH 1/2] fix(crypto): require faithful public commitment parameters Require CommitmentScheme.encodeKey to be an embedding, excluding the concealed setup bit found by the independent semantic review forwarded in #1716. Prove the existing Pedersen encoding injective without changing its bytes, and migrate the Unit-key test schemes. Regressions reject erased Boolean setup keys, establish public dependence of all honest operations, exhibit the erased-key verifier obstruction, and show that exposing the XOR key defeats StatisticalHiding for every setup law. Validation: scripts/check.sh passed all six gates. Selected abstracts and rendering are unaffected. AI assistance: Codex implemented and validated this repair; outside-author-fleet API/correctness/security review remains required. Refs #1716. --- .../Crypto/Computational/Commitment.lean | 6 +- .../Computational/PedersenCommitment.lean | 7 +- .../Crypto/CommitmentPublicSetup.lean | 83 +++++++++++++++++++ .../Crypto/PedersenCommitment.lean | 4 +- 4 files changed, 95 insertions(+), 5 deletions(-) create mode 100644 ComplexityTests/Crypto/CommitmentPublicSetup.lean diff --git a/Complexity/Crypto/Computational/Commitment.lean b/Complexity/Crypto/Computational/Commitment.lean index 14184f515..aceb897f4 100644 --- a/Complexity/Crypto/Computational/Commitment.lean +++ b/Complexity/Crypto/Computational/Commitment.lean @@ -1244,6 +1244,8 @@ theorem OneWay.exists_bitCommitmentScheme {f : List Bool → List Bool} (hf : On /-- A commitment scheme `(C, V)` with public parameters ([BonehShoup2023], Section 8.12, p. 344, and Definition 8.8): * `encodeKey k`: the encoded public parameter string presented to the adversary for key `k`. + This encoding is injective: equal public strings determine the same key and hence the same + valid messages, commitment distributions, and verification results. * `ValidMessage k m`: predicate characterizing valid message words `m` in the message space for key `k`. * `commitDist k msg`: the distribution of `(c, o)` (encoded commitment string `c` and encoded @@ -1264,8 +1266,8 @@ Chosen-message hiding reuses `Encryption.WordAdversary` (`Encryption.AdversaryOf `Complexity/Crypto/Computational/Encryption/Basic.lean`), matching Boneh–Shoup's semantic-security formulation of commitment hiding. -/ structure CommitmentScheme (Key : Type) where - /-- Encoded public parameter presented to the adversary for key `k`. -/ - encodeKey : Key → List Bool + /-- Faithful encoding of the entire public parameter presented to the adversary. -/ + encodeKey : Key ↪ List Bool /-- Predicate characterizing valid message words in the message space for key `k`. -/ ValidMessage : Key → List Bool → Prop /-- Distribution of `(c, o)` (encoded commitment string and encoded opening string) for message diff --git a/Complexity/Crypto/Computational/PedersenCommitment.lean b/Complexity/Crypto/Computational/PedersenCommitment.lean index 09842b79b..1e5ff91c4 100644 --- a/Complexity/Crypto/Computational/PedersenCommitment.lean +++ b/Complexity/Crypto/Computational/PedersenCommitment.lean @@ -321,7 +321,12 @@ noncomputable def pedersenKeyDist (setup : ℕ → PMF F.Desc) (n : ℕ) : PMF F ([BonehShoup2023], Section 8.12, Definition 8.8, p. 344, and Section 10.6.1, p. 414; [Pedersen1991], Section 3). -/ noncomputable def pedersenScheme : CommitmentScheme F.PedersenKey where - encodeKey k := encPair F.encDesc encBits (k.1, F.encode k.1 k.2) + encodeKey := ⟨fun k => encPair F.encDesc encBits (k.1, F.encode k.1 k.2), by + rintro ⟨d, h⟩ ⟨d', h'⟩ heq + obtain ⟨hd, hh⟩ := Prod.ext_iff.mp ((encPair F.encDesc encBits).injective heq) + cases hd + cases F.encode_injective d hh + rfl⟩ ValidMessage k := F.ValidPedersenMessage k.1 commitDist k msg := F.pedersenCommitPairLaw k.1 k.2 (ofBits msg) verify k := F.pedersenVerify k.1 k.2 diff --git a/ComplexityTests/Crypto/CommitmentPublicSetup.lean b/ComplexityTests/Crypto/CommitmentPublicSetup.lean new file mode 100644 index 000000000..63f6775df --- /dev/null +++ b/ComplexityTests/Crypto/CommitmentPublicSetup.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Crypto.Computational.Commitment +import Complexity.Crypto.Negligible.Basic + +/-! +# Public setup for commitment schemes + +Regressions for the concealed setup bit reported in issue #1716. The public encoding must +determine every honest operation. Exposing the setup bit in the XOR construction lets a +chosen-message adversary recover the challenge bit exactly. +-/ + +namespace ComplexityTests.Crypto.CommitmentPublicSetup + +open Cslib Cslib.Probability Cslib.Crypto + +/-- Two distinct Boolean setup keys cannot both be advertised by the empty string. -/ +example (S : CommitmentScheme Bool) : ¬ (∀ k, S.encodeKey k = []) := by + intro h + have hkey : false = true := S.encodeKey.injective ((h false).trans (h true).symm) + cases hkey + +/-- Equal exposed public parameters determine all three honest operations. -/ +example {Key : Type} (S : CommitmentScheme Key) {k₁ k₂ : Key} + (h : S.encodeKey k₁ = S.encodeKey k₂) : + S.ValidMessage k₁ = S.ValidMessage k₂ ∧ + S.commitDist k₁ = S.commitDist k₂ ∧ S.verify k₁ = S.verify k₂ := by + cases S.encodeKey.injective h + exact ⟨rfl, rfl, rfl⟩ + +/-- The XOR verifier from the reported example, with an empty opening. -/ +def xorVerify (k : Bool) (m c o : List Bool) : Bool := + decide (m.length = 1 ∧ o = [] ∧ c = [m.headD false ^^ k]) + +/-- Erasing the setup bit prevents the XOR verifier from factoring through the public string. -/ +example : ¬ ∃ V : List Bool → List Bool → List Bool → List Bool → Bool, + ∀ k m c o, xorVerify k m c o = V [] m c o := by + rintro ⟨V, h⟩ + have hfalse := h false [false] [false] [] + have htrue := h true [false] [false] [] + have hbad : true = false := hfalse.trans htrue.symm + cases hbad + +/-- The XOR construction with its setup bit actually public. -/ +noncomputable def xorScheme : CommitmentScheme Bool where + encodeKey := ⟨fun k => [k], by intro a b h; simpa using h⟩ + ValidMessage _ m := m.length = 1 + commitDist k m := PMF.pure ([m.headD false ^^ k], []) + verify := xorVerify + validMessage_of_verify _ _ _ _ h := (of_decide_eq_true h).1 + verify_of_mem_support _ _ co hm hco := by + rw [PMF.support_pure, Set.mem_singleton_iff] at hco + subst co + simp [xorVerify, hm] + +theorem xorScheme_encodeKey (k : Bool) : xorScheme.encodeKey k = [k] := rfl + +/-- Retain the public bit, then XOR it with the commitment to recover the chosen message. -/ +def xorAdversary : Encryption.WordAdversary where + choose _ pk := pure (([false], [true]), pk) + guess _ pk c := pure (c.headD false ^^ pk.headD false) + +/-- Recovery is exact at each setup key, so it does not depend on the setup distribution. -/ +theorem xor_hidingForKey (k bit : Bool) (n : ℕ) : + xorScheme.hidingForKey k xorAdversary bit n = PMF.pure bit := by + simp only [CommitmentScheme.hidingForKey, xorScheme_encodeKey, xorAdversary] + cases k <;> cases bit <;> simp [xorScheme] + +/-- Public setup rules out statistical hiding for the XOR construction under every setup law. -/ +example (keyDist : ℕ → PMF Bool) : ¬ xorScheme.StatisticalHiding keyDist := by + intro h + have hgame (bit : Bool) (n : ℕ) : + xorScheme.hidingGame keyDist xorAdversary bit n = PMF.pure bit := by + simp [CommitmentScheme.hidingGame, xor_hidingForKey] + exact not_negligible_const (c := 1) one_ne_zero (by + simpa [hgame, Game.advantage, Game.succProbability] using h xorAdversary trivial) + +end ComplexityTests.Crypto.CommitmentPublicSetup diff --git a/ComplexityTests/Crypto/PedersenCommitment.lean b/ComplexityTests/Crypto/PedersenCommitment.lean index 9295d9593..33897f9a2 100644 --- a/ComplexityTests/Crypto/PedersenCommitment.lean +++ b/ComplexityTests/Crypto/PedersenCommitment.lean @@ -117,7 +117,7 @@ example (setup : ℕ → PMF schnorrGroups.Desc) (hDL : schnorrGroups.DiscreteLo /-- Regression witness (`openScheme`): a scheme with empty commitment string and opening equal to the message is perfectly hiding, and is rejected by `CommitmentScheme.Binding`. -/ noncomputable def openScheme : CommitmentScheme Unit where - encodeKey _ := [] + encodeKey := ⟨fun _ => [], fun _ _ _ => Subsingleton.elim _ _⟩ ValidMessage _ _ := True commitDist _ m := PMF.pure ([], m) verify _ m c o := decide (c = [] ∧ o = m) @@ -150,7 +150,7 @@ example : ¬ openScheme.Binding (fun _ => PMF.pure ()) := by commitment string equals the message word satisfies `StatisticalHiding` because `hidingForKey` commits to `m_bit` only when both challenge words satisfy `ValidMessage`. -/ noncomputable def singletonScheme : CommitmentScheme Unit where - encodeKey _ := [] + encodeKey := ⟨fun _ => [], fun _ _ _ => Subsingleton.elim _ _⟩ ValidMessage _ m := m = [] commitDist _ m := PMF.pure (m, []) verify _ m c _ := decide (m = [] ∧ c = []) From b531dbf0130fd8992deab7887a67b97684de67ef Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 06:09:55 -0400 Subject: [PATCH 2/2] doc(crypto): clarify commitment efficiency boundary Clarify the independent reviewer-crei-opus suggestion on #1718: the key embedding enforces information-theoretic public dependence; efficient decoding and evaluation from the exposed string need separate certificates. No definition, theorem, game, test or selected abstract changes. scripts/check.sh passes all six gates. AI assistance: Codex. --- Complexity/Crypto/Computational/Commitment.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Complexity/Crypto/Computational/Commitment.lean b/Complexity/Crypto/Computational/Commitment.lean index aceb897f4..a3bc5d40f 100644 --- a/Complexity/Crypto/Computational/Commitment.lean +++ b/Complexity/Crypto/Computational/Commitment.lean @@ -1246,6 +1246,8 @@ and Definition 8.8): * `encodeKey k`: the encoded public parameter string presented to the adversary for key `k`. This encoding is injective: equal public strings determine the same key and hence the same valid messages, commitment distributions, and verification results. + Injectivity is an information-theoretic condition; decoding and evaluating honest operations + from this string need separate efficiency certificates. * `ValidMessage k m`: predicate characterizing valid message words `m` in the message space for key `k`. * `commitDist k msg`: the distribution of `(c, o)` (encoded commitment string `c` and encoded