From 6a1177ffdf41fafc82b20971670b08f6c722e33c Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 31 Jul 2026 22:34:00 -0400 Subject: [PATCH 1/2] feat: add commitment schemes and statistical distance --- Cslib.lean | 4 + Cslib/Crypto/Protocols/Commitment/Basic.lean | 63 ++++++ Cslib/Crypto/Protocols/Commitment/Defs.lean | 77 +++++++ Cslib/Crypto/Protocols/Commitment/Scheme.lean | 101 +++++++++ Cslib/Probability/StatisticalDistance.lean | 205 ++++++++++++++++++ CslibTests.lean | 1 + CslibTests/Commitment.lean | 42 ++++ references.bib | 8 + 8 files changed, 501 insertions(+) create mode 100644 Cslib/Crypto/Protocols/Commitment/Basic.lean create mode 100644 Cslib/Crypto/Protocols/Commitment/Defs.lean create mode 100644 Cslib/Crypto/Protocols/Commitment/Scheme.lean create mode 100644 Cslib/Probability/StatisticalDistance.lean create mode 100644 CslibTests/Commitment.lean diff --git a/Cslib.lean b/Cslib.lean index d67431976..e32d48492 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -50,6 +50,9 @@ public import Cslib.Computability.URM.Defs public import Cslib.Computability.URM.Execution public import Cslib.Computability.URM.StandardForm public import Cslib.Computability.URM.StraightLine +public import Cslib.Crypto.Protocols.Commitment.Basic +public import Cslib.Crypto.Protocols.Commitment.Defs +public import Cslib.Crypto.Protocols.Commitment.Scheme public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption @@ -168,3 +171,4 @@ public import Cslib.MachineLearning.PACLearning.VCDimension public import Cslib.MachineLearning.PACLearning.VersionSpace public import Cslib.MachineLearning.PACLearning.VersionSpaceLattice public import Cslib.Probability.PMF +public import Cslib.Probability.StatisticalDistance diff --git a/Cslib/Crypto/Protocols/Commitment/Basic.lean b/Cslib/Crypto/Protocols/Commitment/Basic.lean new file mode 100644 index 000000000..bcbbc0af8 --- /dev/null +++ b/Cslib/Crypto/Protocols/Commitment/Basic.lean @@ -0,0 +1,63 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Crypto.Protocols.Commitment.Defs + +/-! +# Commitment Schemes + +Basic results about information-theoretic commitment schemes. + +## Main results + +- `Scheme.perfectlyHiding_iff_statisticallyHiding_zero`: perfect hiding is + statistical hiding with zero error +- `Scheme.subsingleton_of_perfectlyHiding_of_perfectlyBinding`: a scheme + cannot be both perfectly hiding and perfectly binding unless any two + messages are equal +-/ + +@[expose] public section + +namespace Cslib.Crypto.Protocols.Commitment.Scheme + +open scoped NNReal + +variable {Message Commitment Opening : Type*} + +/-- Perfect hiding is exactly statistical hiding with zero error. -/ +theorem perfectlyHiding_iff_statisticallyHiding_zero + [Fintype Commitment] (scheme : Scheme Message Commitment Opening) : + scheme.PerfectlyHiding ↔ scheme.StatisticallyHiding 0 := by + simp [PerfectlyHiding, StatisticallyHiding] + +/-- Enlarging the permitted error preserves statistical hiding. -/ +theorem StatisticallyHiding.mono [Fintype Commitment] + {scheme : Scheme Message Commitment Opening} {ε δ : ℝ≥0} + (h : scheme.StatisticallyHiding ε) (hεδ : ε ≤ δ) : + scheme.StatisticallyHiding δ := + fun message₀ message₁ => (h message₀ message₁).mono hεδ + +/-- A scheme cannot be both perfectly hiding and perfectly binding unless any +two messages are equal. -/ +theorem subsingleton_of_perfectlyHiding_of_perfectlyBinding + (scheme : Scheme Message Commitment Opening) + (hhide : scheme.PerfectlyHiding) (hbind : scheme.PerfectlyBinding) : + Subsingleton Message := by + refine ⟨fun message₀ message₁ => ?_⟩ + obtain ⟨commitment, hcommitment⟩ := + (scheme.commitmentDist message₀).support_nonempty + obtain ⟨opening₀, hpair₀⟩ := + scheme.mem_support_commitmentDist_iff.mp hcommitment + rw [hhide message₀ message₁] at hcommitment + obtain ⟨opening₁, hpair₁⟩ := + scheme.mem_support_commitmentDist_iff.mp hcommitment + exact hbind commitment message₀ opening₀ message₁ opening₁ + (scheme.accepts_of_mem_support hpair₀) (scheme.accepts_of_mem_support hpair₁) + +end Cslib.Crypto.Protocols.Commitment.Scheme diff --git a/Cslib/Crypto/Protocols/Commitment/Defs.lean b/Cslib/Crypto/Protocols/Commitment/Defs.lean new file mode 100644 index 000000000..4b544d9fc --- /dev/null +++ b/Cslib/Crypto/Protocols/Commitment/Defs.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Crypto.Protocols.Commitment.Scheme +public import Cslib.Probability.StatisticalDistance + +/-! +# Commitment Schemes: Information-Theoretic Security + +Hiding and binding for commitment schemes, in their information-theoretic forms +([BonehShoup2023], Section 8.12). Perfect hiding: every message yields the same +commitment distribution. Statistical hiding: any two commitment distributions +are within statistical distance `ε`. Perfect binding: no commitment can be +opened to two different messages, even by an unbounded committer. + +Each definition is about a single, fixed scheme; statistical hiding carries an +explicit error bound, and the perfect notions have no error at all. The +asymptotic notions in the book — negligible statistical distance for families +of distributions ([BonehShoup2023], Definition 3.6), or security against +efficient adversaries (Section 8.12) — can be layered on top of these later. + +## Main definitions + +- `Scheme.PerfectlyHiding`: the commitment distributions are equal for every + pair of messages +- `Scheme.StatisticallyHiding`: the commitment distributions are statistically + close with error `ε` +- `Scheme.PerfectlyBinding`: no commitment has accepted openings to two + different messages + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023] +-/ + +@[expose] public section + +namespace Cslib.Crypto.Protocols.Commitment.Scheme + +open Cslib.Probability.PMF +open scoped NNReal + +variable {Message Commitment Opening : Type*} + +/-- A scheme is perfectly hiding when every message yields the same commitment +distribution, so a commitment reveals nothing about the message as long as its +opening is withheld ([BonehShoup2023], Section 8.12). -/ +def PerfectlyHiding (scheme : Scheme Message Commitment Opening) : Prop := + ∀ message₀ message₁ : Message, + scheme.commitmentDist message₀ = scheme.commitmentDist message₁ + +/-- A scheme is statistically hiding with error `ε` when the commitment +distributions of any two messages are within statistical distance `ε` +([BonehShoup2023], Definition 3.5 and Section 8.12). -/ +def StatisticallyHiding [Fintype Commitment] + (scheme : Scheme Message Commitment Opening) (ε : ℝ≥0) : Prop := + ∀ message₀ message₁ : Message, + StatisticallyClose (scheme.commitmentDist message₀) + (scheme.commitmentDist message₁) ε + +/-- A scheme is perfectly binding when a commitment can be opened to at most +one message: any two accepted openings of the same commitment agree on the +message ([BonehShoup2023], Section 8.12). Different openings of the same +message are still allowed. -/ +def PerfectlyBinding (scheme : Scheme Message Commitment Opening) : Prop := + ∀ commitment message₀ opening₀ message₁ opening₁, + scheme.Accepts message₀ commitment opening₀ → + scheme.Accepts message₁ commitment opening₁ → + message₀ = message₁ + +end Cslib.Crypto.Protocols.Commitment.Scheme diff --git a/Cslib/Crypto/Protocols/Commitment/Scheme.lean b/Cslib/Crypto/Protocols/Commitment/Scheme.lean new file mode 100644 index 000000000..d68845ceb --- /dev/null +++ b/Cslib/Crypto/Protocols/Commitment/Scheme.lean @@ -0,0 +1,101 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Init +public import Mathlib.Probability.ProbabilityMassFunction.Constructions + +/-! +# Commitment Schemes: Syntax and Correctness + +The syntax of a commitment scheme ([BonehShoup2023], Section 8.12): committing +to a message samples a commitment-opening pair `(c, o)`, verification of a +claimed opening is deterministic, and honestly generated pairs always verify. + +The algorithms are plain functions, with no efficiency or finiteness +assumptions. Security notions live in separate definitions, so the same syntax +can carry perfect, statistical, or computational security. + +## Main definitions + +- `Scheme`: commitment syntax with perfect correctness +- `Scheme.commitmentDist`: the public commitment distribution for a message +- `Scheme.mem_support_commitmentDist_iff`: a commitment is possible exactly + when it has a possible opening +- `Scheme.Accepts`: the verifier's acceptance relation + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023] +-/ + +@[expose] public section + +namespace Cslib.Crypto.Protocols.Commitment + +/-- A noninteractive, unkeyed commitment scheme over message, commitment, and +opening types ([BonehShoup2023], Section 8.12). + +Committing is randomized and produces the commitment and opening together, +since the two may be correlated. Correctness requires that every +commitment-opening pair the honest committer can output is accepted by the +verifier; for a `PMF`, this says honest openings verify with probability +one. -/ +structure Scheme (Message Commitment Opening : Type*) where + /-- Randomized commitment and opening generation. -/ + commit (message : Message) : PMF (Commitment × Opening) + /-- Deterministic verification of a claimed opening. -/ + verify (message : Message) (commitment : Commitment) (opening : Opening) : Bool + /-- Every honestly generated commitment-opening pair verifies. -/ + correct : ∀ message commitment opening, + (commitment, opening) ∈ (commit message).support → + verify message commitment opening = true + +namespace Scheme + +variable {Message Commitment Opening : Type*} + +/-- The public commitment distribution obtained by forgetting the opening. -/ +noncomputable def commitmentDist (scheme : Scheme Message Commitment Opening) + (message : Message) : PMF Commitment := + (scheme.commit message).map Prod.fst + +/-- A commitment lies in the public distribution's support exactly when some +opening makes the corresponding pair an honest possible output. -/ +theorem mem_support_commitmentDist_iff + (scheme : Scheme Message Commitment Opening) {message : Message} + {commitment : Commitment} : + commitment ∈ (scheme.commitmentDist message).support ↔ + ∃ opening, (commitment, opening) ∈ (scheme.commit message).support := by + simp [commitmentDist] + +/-- The proposition that an opening is accepted for a commitment and message. -/ +def Accepts (scheme : Scheme Message Commitment Opening) (message : Message) + (commitment : Commitment) (opening : Opening) : Prop := + scheme.verify message commitment opening = true + +/-- Every pair in the support of honest commitment is accepted. -/ +theorem accepts_of_mem_support (scheme : Scheme Message Commitment Opening) + {message : Message} {commitment : Commitment} {opening : Opening} + (h : (commitment, opening) ∈ (scheme.commit message).support) : + scheme.Accepts message commitment opening := + scheme.correct message commitment opening h + +/-- Build a commitment scheme from deterministic commitment generation. -/ +noncomputable def ofPure (commit : Message → Commitment × Opening) + (verify : Message → Commitment → Opening → Bool) + (correct : ∀ message, verify message (commit message).1 (commit message).2 = true) : + Scheme Message Commitment Opening where + commit message := PMF.pure (commit message) + verify := verify + correct message commitment opening h := by + grind [PMF.mem_support_pure_iff] + +end Scheme + +end Cslib.Crypto.Protocols.Commitment diff --git a/Cslib/Probability/StatisticalDistance.lean b/Cslib/Probability/StatisticalDistance.lean new file mode 100644 index 000000000..784270f5c --- /dev/null +++ b/Cslib/Probability/StatisticalDistance.lean @@ -0,0 +1,205 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Init +public import Mathlib.Probability.ProbabilityMassFunction.Constructions + +/-! +# Statistical Distance of Finite Probability Mass Functions + +For PMFs `p` and `q` on a finite type, their statistical distance is + +`(1 / 2) * ∑ a, |p a - q a|`. + +This is [BonehShoup2023], Definition 3.5. The probabilities are converted from +`ℝ≥0∞`, Mathlib's codomain for a `PMF`, to `ℝ` before taking the finite sum. + +Besides the basic metric properties, this file proves that applying the same +transformation — deterministic or randomized — to two PMFs cannot increase +their statistical distance; [BonehShoup2023], Theorem 3.13 is the +deterministic case. + +## Main definitions + +- `statisticalDistance`: statistical distance +- `StatisticallyClose`: an upper bound on statistical distance + +## Main results + +- `statisticalDistance_bind_le`: randomized postprocessing cannot increase + statistical distance +- `StatisticallyClose.trans`: closeness bounds chain through an intermediate + distribution, adding the errors +- `statisticallyClose_zero_iff`: zero error is equality + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023] +-/ + +@[expose] public section + +namespace Cslib.Probability.PMF + +open scoped NNReal + +universe u v + +variable {α : Type u} {β : Type v} + +private theorem sum_toReal [Fintype α] (p : PMF α) : + ∑ a, (p a).toReal = 1 := by + rw [← ENNReal.toReal_one, ← p.tsum_coe, tsum_fintype, + ENNReal.toReal_sum fun a _ => p.apply_ne_top a] + +private theorem bind_apply_toReal [Fintype α] (p : PMF α) + (kernel : α → PMF β) (b : β) : + (p.bind kernel b).toReal = + ∑ a, (p a).toReal * (kernel a b).toReal := by + rw [PMF.bind_apply, tsum_fintype, + ENNReal.toReal_sum fun a _ => + ENNReal.mul_ne_top (p.apply_ne_top a) ((kernel a).apply_ne_top b)] + simp only [ENNReal.toReal_mul] + +/-- The statistical distance between two PMFs on a finite type +([BonehShoup2023], Definition 3.5). -/ +noncomputable def statisticalDistance [Fintype α] (p q : PMF α) : ℝ := + (∑ a, |(p a).toReal - (q a).toReal|) / 2 + +/-- Statistical distance is nonnegative. -/ +theorem statisticalDistance_nonneg [Fintype α] (p q : PMF α) : + 0 ≤ statisticalDistance p q := + div_nonneg (Finset.sum_nonneg fun _ _ => abs_nonneg _) zero_le_two + +/-- Statistical distance is at most one. -/ +theorem statisticalDistance_le_one [Fintype α] (p q : PMF α) : + statisticalDistance p q ≤ 1 := by + rw [statisticalDistance] + have h := Finset.sum_le_sum fun a (_ : a ∈ Finset.univ) => + abs_sub_le (p a).toReal 0 (q a).toReal + simp only [sub_zero, zero_sub, abs_neg, abs_of_nonneg ENNReal.toReal_nonneg, + Finset.sum_add_distrib, sum_toReal] at h + linarith + +/-- A PMF has zero statistical distance from itself. -/ +@[simp] +theorem statisticalDistance_self [Fintype α] (p : PMF α) : + statisticalDistance p p = 0 := by + simp [statisticalDistance] + +/-- Statistical distance is symmetric. -/ +theorem statisticalDistance_comm [Fintype α] (p q : PMF α) : + statisticalDistance p q = statisticalDistance q p := by + simp only [statisticalDistance, abs_sub_comm] + +/-- Statistical distance satisfies the triangle inequality. -/ +theorem statisticalDistance_triangle [Fintype α] (p q r : PMF α) : + statisticalDistance p r ≤ statisticalDistance p q + statisticalDistance q r := by + simp only [statisticalDistance, ← add_div, ← Finset.sum_add_distrib] + gcongr with a + exact abs_sub_le (p a).toReal (q a).toReal (r a).toReal + +/-- Statistical distance is zero exactly when the PMFs are equal. -/ +@[simp] +theorem statisticalDistance_eq_zero_iff [Fintype α] (p q : PMF α) : + statisticalDistance p q = 0 ↔ p = q := by + refine ⟨fun h => ?_, by rintro rfl; simp⟩ + have hsum : ∑ a, |(p a).toReal - (q a).toReal| = 0 := by + simpa [statisticalDistance] using h + ext a + apply (ENNReal.toReal_eq_toReal_iff' (p.apply_ne_top a) (q.apply_ne_top a)).mp + simpa [sub_eq_zero] using congr_fun + ((Fintype.sum_eq_zero_iff_of_nonneg fun _ => abs_nonneg _).mp hsum) a + +/-- Applying the same randomized kernel to two PMFs cannot increase their +statistical distance. -/ +theorem statisticalDistance_bind_le [Fintype α] [Fintype β] + (p q : PMF α) (kernel : α → PMF β) : + statisticalDistance (p.bind kernel) (q.bind kernel) ≤ statisticalDistance p q := by + simp only [statisticalDistance, bind_apply_toReal] + apply div_le_div_of_nonneg_right _ (by norm_num) + calc + (∑ b, |(∑ a, (p a).toReal * (kernel a b).toReal) - + ∑ a, (q a).toReal * (kernel a b).toReal|) + ≤ ∑ b, ∑ a, |(p a).toReal * (kernel a b).toReal - + (q a).toReal * (kernel a b).toReal| := + Finset.sum_le_sum fun _ _ => by + rw [← Finset.sum_sub_distrib] + exact Finset.abs_sum_le_sum_abs _ _ + _ = ∑ b, ∑ a, (kernel a b).toReal * + |(p a).toReal - (q a).toReal| := by + congr 1 with b + congr 1 with a + rw [← sub_mul, abs_mul, abs_of_nonneg ENNReal.toReal_nonneg] + ring + _ = ∑ a, |(p a).toReal - (q a).toReal| := by + rw [Finset.sum_comm] + simp_rw [← Finset.sum_mul, sum_toReal, one_mul] + +/-- Deterministic postprocessing cannot increase statistical distance +([BonehShoup2023], Theorem 3.13). -/ +theorem statisticalDistance_map_le [Fintype α] [Fintype β] + (p q : PMF α) (f : α → β) : + statisticalDistance (p.map f) (q.map f) ≤ statisticalDistance p q := by + simpa only [PMF.bind_pure_comp] using + statisticalDistance_bind_le p q (PMF.pure ∘ f) + +/-- Two PMFs are `ε`-statistically close when their statistical distance is at +most `ε`. The `ℝ≥0` parameter rules out meaningless negative bounds. -/ +def StatisticallyClose [Fintype α] (p q : PMF α) (ε : ℝ≥0) : Prop := + statisticalDistance p q ≤ (ε : ℝ) + +namespace StatisticallyClose + +/-- Every PMF is statistically close to itself with zero error. -/ +theorem refl [Fintype α] (p : PMF α) : StatisticallyClose p p 0 := by + simp [StatisticallyClose] + +/-- Statistical closeness is symmetric. -/ +theorem symm [Fintype α] {p q : PMF α} {ε : ℝ≥0} + (h : StatisticallyClose p q ε) : StatisticallyClose q p ε := by + simpa only [StatisticallyClose, statisticalDistance_comm] using h + +/-- A statistical-closeness bound remains valid when its error is enlarged. -/ +theorem mono [Fintype α] {p q : PMF α} {ε δ : ℝ≥0} + (h : StatisticallyClose p q ε) (hεδ : ε ≤ δ) : + StatisticallyClose p q δ := + h.trans (by exact_mod_cast hεδ) + +/-- Closeness bounds chain through an intermediate distribution, adding the +errors. -/ +theorem trans [Fintype α] {p q r : PMF α} {ε δ : ℝ≥0} + (hpq : StatisticallyClose p q ε) (hqr : StatisticallyClose q r δ) : + StatisticallyClose p r (ε + δ) := + (statisticalDistance_triangle p q r).trans (by + simpa only [NNReal.coe_add] using add_le_add hpq hqr) + +/-- A shared randomized postprocessing kernel preserves statistical +closeness. -/ +theorem bind [Fintype α] [Fintype β] {p q : PMF α} {ε : ℝ≥0} + (h : StatisticallyClose p q ε) (kernel : α → PMF β) : + StatisticallyClose (p.bind kernel) (q.bind kernel) ε := + (statisticalDistance_bind_le p q kernel).trans h + +/-- Deterministic postprocessing preserves statistical closeness. -/ +theorem map [Fintype α] [Fintype β] {p q : PMF α} {ε : ℝ≥0} + (h : StatisticallyClose p q ε) (f : α → β) : + StatisticallyClose (p.map f) (q.map f) ε := + (statisticalDistance_map_le p q f).trans h + +end StatisticallyClose + +/-- Statistical closeness with zero error is equality. -/ +@[simp] +theorem statisticallyClose_zero_iff [Fintype α] (p q : PMF α) : + StatisticallyClose p q 0 ↔ p = q := by + rw [StatisticallyClose, ← statisticalDistance_eq_zero_iff] + exact ⟨fun h => le_antisymm h (statisticalDistance_nonneg p q), Eq.le⟩ + +end Cslib.Probability.PMF diff --git a/CslibTests.lean b/CslibTests.lean index ed3063209..0f59ccfb5 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -1,6 +1,7 @@ import CslibTests.Bisimulation import CslibTests.CCS import CslibTests.CLL +import CslibTests.Commitment import CslibTests.DFA import CslibTests.FreeMonad import CslibTests.GrindLint diff --git a/CslibTests/Commitment.lean b/CslibTests/Commitment.lean new file mode 100644 index 000000000..054cef1f8 --- /dev/null +++ b/CslibTests/Commitment.lean @@ -0,0 +1,42 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Cslib.Crypto.Protocols.Commitment.Basic + +namespace CslibTests.Commitment + +open Cslib.Crypto.Protocols.Commitment +open Cslib.Probability.PMF +open scoped NNReal + +example {α β : Type*} [Fintype α] [Fintype β] {p q : PMF α} {ε : ℝ≥0} + (h : StatisticallyClose p q ε) (kernel : α → PMF β) : + StatisticallyClose (p.bind kernel) (q.bind kernel) ε := + h.bind kernel + +/-- A toy scheme that reveals nothing and accepts every opening. -/ +noncomputable def opaqueScheme (Message : Type*) : Scheme Message Unit Unit := + Scheme.ofPure (fun _ => ((), ())) (fun _ _ _ => true) (by simp) + +theorem opaqueScheme_perfectlyHiding (Message : Type*) : + (opaqueScheme Message).PerfectlyHiding := by + simp [Scheme.PerfectlyHiding, opaqueScheme, Scheme.commitmentDist, Scheme.ofPure] + +example (Message : Type*) : (opaqueScheme Message).StatisticallyHiding 0 := + ((opaqueScheme Message).perfectlyHiding_iff_statisticallyHiding_zero).mp + (opaqueScheme_perfectlyHiding Message) + +/-- A toy scheme whose commitment is the message itself. -/ +noncomputable def revealingScheme (Message : Type*) [DecidableEq Message] : + Scheme Message Message Unit := + Scheme.ofPure (fun message => (message, ())) + (fun message commitment _ => decide (commitment = message)) (by simp) + +theorem revealingScheme_perfectlyBinding (Message : Type*) [DecidableEq Message] : + (revealingScheme Message).PerfectlyBinding := by + simp [Scheme.PerfectlyBinding, Scheme.Accepts, revealingScheme, Scheme.ofPure] + +end CslibTests.Commitment diff --git a/references.bib b/references.bib index 7366ab0c2..946942654 100644 --- a/references.bib +++ b/references.bib @@ -49,6 +49,14 @@ @book{Blackburn2001 collection={Cambridge Tracts in Theoretical Computer Science} } +@misc{BonehShoup2023, + author = {Dan Boneh and Victor Shoup}, + title = {A Graduate Course in Applied Cryptography}, + year = {2023}, + note = {Version 0.6}, + url = {https://crypto.stanford.edu/~dabo/cryptobook/BonehShoup_0_6.pdf} +} + @misc{Burghardt2018, title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}}, url = {https://arxiv.org/abs/1806.05036v2}, From 51bd04fbd6844166e39218ca3e150715c647f763 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 31 Jul 2026 22:50:31 -0400 Subject: [PATCH 2/2] feat: prove the hiding-binding trade-off for commitment schemes --- Cslib/Crypto/Protocols/Commitment/Basic.lean | 63 ++++++++++++++++++-- Cslib/Probability/StatisticalDistance.lean | 19 ++++++ CslibTests/Commitment.lean | 8 +++ 3 files changed, 86 insertions(+), 4 deletions(-) diff --git a/Cslib/Crypto/Protocols/Commitment/Basic.lean b/Cslib/Crypto/Protocols/Commitment/Basic.lean index bcbbc0af8..05079ed36 100644 --- a/Cslib/Crypto/Protocols/Commitment/Basic.lean +++ b/Cslib/Crypto/Protocols/Commitment/Basic.lean @@ -13,19 +13,32 @@ public import Cslib.Crypto.Protocols.Commitment.Defs Basic results about information-theoretic commitment schemes. +The main result is the hiding–binding trade-off: a perfectly binding scheme +places the commitment distributions of distinct messages at the maximum +statistical distance, so it cannot be statistically hiding for any error below +one. Hiding and binding can therefore not both hold unconditionally; real +schemes make at most one side information-theoretic and settle for a +computational version of the other. + ## Main results +- `Scheme.subsingleton_of_statisticallyHiding_of_perfectlyBinding`: a scheme + cannot be both statistically hiding with error below one and perfectly + binding unless any two messages are equal +- `Scheme.PerfectlyBinding.statisticalDistance_commitmentDist_eq_one`: perfect + binding forces distinct messages' commitment distributions to the maximum + statistical distance +- `Scheme.subsingleton_of_perfectlyHiding_of_perfectlyBinding`: the perfect + hiding case, with no finiteness assumption on commitments - `Scheme.perfectlyHiding_iff_statisticallyHiding_zero`: perfect hiding is statistical hiding with zero error -- `Scheme.subsingleton_of_perfectlyHiding_of_perfectlyBinding`: a scheme - cannot be both perfectly hiding and perfectly binding unless any two - messages are equal -/ @[expose] public section namespace Cslib.Crypto.Protocols.Commitment.Scheme +open Cslib.Probability.PMF open scoped NNReal variable {Message Commitment Opening : Type*} @@ -43,8 +56,50 @@ theorem StatisticallyHiding.mono [Fintype Commitment] scheme.StatisticallyHiding δ := fun message₀ message₁ => (h message₀ message₁).mono hεδ +/-- Distinct messages of a perfectly binding scheme have disjoint sets of +possible commitments. -/ +theorem PerfectlyBinding.disjoint_support_commitmentDist + {scheme : Scheme Message Commitment Opening} (hbind : scheme.PerfectlyBinding) + {message₀ message₁ : Message} (hne : message₀ ≠ message₁) : + Disjoint (scheme.commitmentDist message₀).support + (scheme.commitmentDist message₁).support := by + rw [Set.disjoint_left] + intro commitment h₀ h₁ + obtain ⟨opening₀, hpair₀⟩ := scheme.mem_support_commitmentDist_iff.mp h₀ + obtain ⟨opening₁, hpair₁⟩ := scheme.mem_support_commitmentDist_iff.mp h₁ + exact hne (hbind commitment message₀ opening₀ message₁ opening₁ + (scheme.accepts_of_mem_support hpair₀) (scheme.accepts_of_mem_support hpair₁)) + +/-- In a perfectly binding scheme, the commitment distributions of distinct +messages are at the maximum statistical distance: an unbounded observer can +read the message off the commitment. -/ +theorem PerfectlyBinding.statisticalDistance_commitmentDist_eq_one + [Fintype Commitment] {scheme : Scheme Message Commitment Opening} + (hbind : scheme.PerfectlyBinding) {message₀ message₁ : Message} + (hne : message₀ ≠ message₁) : + statisticalDistance (scheme.commitmentDist message₀) + (scheme.commitmentDist message₁) = 1 := + statisticalDistance_eq_one_of_disjoint_support (hbind.disjoint_support_commitmentDist hne) + +/-- **The hiding–binding trade-off.** A scheme cannot be both statistically +hiding with error below one and perfectly binding unless any two messages are +equal. The error bound is sharp: statistical hiding with error one holds +vacuously for every scheme. -/ +theorem subsingleton_of_statisticallyHiding_of_perfectlyBinding + [Fintype Commitment] (scheme : Scheme Message Commitment Opening) {ε : ℝ≥0} + (hε : ε < 1) (hhide : scheme.StatisticallyHiding ε) + (hbind : scheme.PerfectlyBinding) : Subsingleton Message := by + refine ⟨fun message₀ message₁ => ?_⟩ + by_contra hne + have hone := hbind.statisticalDistance_commitmentDist_eq_one hne + have hle : statisticalDistance (scheme.commitmentDist message₀) + (scheme.commitmentDist message₁) ≤ (ε : ℝ) := hhide message₀ message₁ + rw [hone] at hle + exact absurd hle (by exact_mod_cast hε.not_ge) + /-- A scheme cannot be both perfectly hiding and perfectly binding unless any -two messages are equal. -/ +two messages are equal. Unlike the statistical version, this needs no +finiteness assumption on the commitment type. -/ theorem subsingleton_of_perfectlyHiding_of_perfectlyBinding (scheme : Scheme Message Commitment Opening) (hhide : scheme.PerfectlyHiding) (hbind : scheme.PerfectlyBinding) : diff --git a/Cslib/Probability/StatisticalDistance.lean b/Cslib/Probability/StatisticalDistance.lean index 784270f5c..d1af265dc 100644 --- a/Cslib/Probability/StatisticalDistance.lean +++ b/Cslib/Probability/StatisticalDistance.lean @@ -33,6 +33,8 @@ deterministic case. - `statisticalDistance_bind_le`: randomized postprocessing cannot increase statistical distance +- `statisticalDistance_eq_one_of_disjoint_support`: PMFs with disjoint + supports are at the maximum statistical distance - `StatisticallyClose.trans`: closeness bounds chain through an intermediate distribution, adding the errors - `statisticallyClose_zero_iff`: zero error is equality @@ -117,6 +119,23 @@ theorem statisticalDistance_eq_zero_iff [Fintype α] (p q : PMF α) : simpa [sub_eq_zero] using congr_fun ((Fintype.sum_eq_zero_iff_of_nonneg fun _ => abs_nonneg _).mp hsum) a +/-- PMFs with disjoint supports are at the maximum statistical distance. -/ +theorem statisticalDistance_eq_one_of_disjoint_support [Fintype α] {p q : PMF α} + (h : Disjoint p.support q.support) : statisticalDistance p q = 1 := by + have key : ∀ a, |(p a).toReal - (q a).toReal| = (p a).toReal + (q a).toReal := by + intro a + by_cases hp : p a = 0 + · rw [hp] + simp [abs_of_nonneg ENNReal.toReal_nonneg] + · have hq : q a = 0 := by + by_contra hq + exact Set.disjoint_left.mp h ((p.mem_support_iff a).mpr hp) + ((q.mem_support_iff a).mpr hq) + rw [hq] + simp [abs_of_nonneg ENNReal.toReal_nonneg] + simp only [statisticalDistance, key, Finset.sum_add_distrib, sum_toReal] + norm_num + /-- Applying the same randomized kernel to two PMFs cannot increase their statistical distance. -/ theorem statisticalDistance_bind_le [Fintype α] [Fintype β] diff --git a/CslibTests/Commitment.lean b/CslibTests/Commitment.lean index 054cef1f8..b2f797ca8 100644 --- a/CslibTests/Commitment.lean +++ b/CslibTests/Commitment.lean @@ -39,4 +39,12 @@ theorem revealingScheme_perfectlyBinding (Message : Type*) [DecidableEq Message] (revealingScheme Message).PerfectlyBinding := by simp [Scheme.PerfectlyBinding, Scheme.Accepts, revealingScheme, Scheme.ofPure] +/-- The hiding–binding trade-off: no scheme with two distinct messages is both +statistically hiding with error below one and perfectly binding. -/ +example {ε : ℝ≥0} (hε : ε < 1) (scheme : Scheme Bool Bool Unit) + (hhide : scheme.StatisticallyHiding ε) (hbind : scheme.PerfectlyBinding) : + False := by + have h := scheme.subsingleton_of_statisticallyHiding_of_perfectlyBinding hε hhide hbind + exact absurd (h.allEq true false) (by decide) + end CslibTests.Commitment