From be26797f1c46055aa813ff844a6400445c77886b Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 15 Apr 2026 14:48:34 -0400 Subject: [PATCH 1/4] feat(Cryptography/SecretSharing): Shamir's secret sharing --- Cslib.lean | 6 + .../PerfectSecrecy/PMFUtilities.lean | 47 +++- .../Crypto/Protocols/SecretSharing/Basic.lean | 107 +++++++++ .../Crypto/Protocols/SecretSharing/Defs.lean | 90 +++++++ .../SecretSharing/Internal/ShamirAlgebra.lean | 140 +++++++++++ .../Protocols/SecretSharing/Scheme.lean | 96 ++++++++ .../Protocols/SecretSharing/Shamir.lean | 220 ++++++++++++++++++ .../SecretSharing/ShamirPrivacy.lean | 198 ++++++++++++++++ CslibTests.lean | 2 + CslibTests/Shamir.lean | 67 ++++++ CslibTests/ShamirPrivacy.lean | 66 ++++++ references.bib | 13 ++ 12 files changed, 1050 insertions(+), 2 deletions(-) create mode 100644 Cslib/Crypto/Protocols/SecretSharing/Basic.lean create mode 100644 Cslib/Crypto/Protocols/SecretSharing/Defs.lean create mode 100644 Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean create mode 100644 Cslib/Crypto/Protocols/SecretSharing/Scheme.lean create mode 100644 Cslib/Crypto/Protocols/SecretSharing/Shamir.lean create mode 100644 Cslib/Crypto/Protocols/SecretSharing/ShamirPrivacy.lean create mode 100644 CslibTests/Shamir.lean create mode 100644 CslibTests/ShamirPrivacy.lean diff --git a/Cslib.lean b/Cslib.lean index ef09e6f16..6c736b4a0 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -43,6 +43,12 @@ public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.OneTimePad public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy public import Cslib.Crypto.Protocols.PerfectSecrecy.OneTimePad public import Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities +public import Cslib.Crypto.Protocols.SecretSharing.Basic +public import Cslib.Crypto.Protocols.SecretSharing.Defs +public import Cslib.Crypto.Protocols.SecretSharing.Internal.ShamirAlgebra +public import Cslib.Crypto.Protocols.SecretSharing.Scheme +public import Cslib.Crypto.Protocols.SecretSharing.Shamir +public import Cslib.Crypto.Protocols.SecretSharing.ShamirPrivacy public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey public import Cslib.Foundations.Control.Monad.Free public import Cslib.Foundations.Control.Monad.Free.Effects diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean index 3980e3e89..7d211d8fa 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean @@ -8,6 +8,7 @@ module public import Cslib.Init public import Mathlib.Probability.ProbabilityMassFunction.Monad +public import Mathlib.Probability.Distributions.Uniform @[expose] public section @@ -27,16 +28,21 @@ the Mathlib module instead. - `PMFUtilities.bind_pair_apply`: the "pairing" bind at `(a, b)` equals `p a * f a b` - `PMFUtilities.bind_pair_tsum_fst`: marginalizing over the first component +- `PMFUtilities.uniformOfFintype_map_equiv`: + a uniform distribution is invariant under equivalence - `PMFUtilities.posterior_hasSum`: posterior probabilities sum to 1 - `PMFUtilities.posteriorDist`: the posterior as a `PMF` +- `PMFUtilities.posteriorDist_eq_prior_of_outputIndist`: + if the output distribution does not depend on the input, conditioning does + not change the prior -/ namespace Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities open PMF ENNReal -universe u -variable {α β : Type u} +universe u v +variable {α : Type u} {β : Type v} /-- Evaluating the "pairing" bind `(do let a ← p; return (a, ← f a))` at `(a, b)` gives the product `p a * f a b`. -/ @@ -54,6 +60,24 @@ theorem bind_pair_tsum_fst (p : PMF α) (f : α → PMF β) (b : β) : (p.bind f) b := by simp_rw [bind_pair_apply, PMF.bind_apply] +/-- A uniform distribution on a finite type is invariant under any equivalence. -/ +theorem uniformOfFintype_map_equiv {γ : Type v} [Fintype α] [Fintype γ] [Nonempty α] [Nonempty γ] + (e : α ≃ γ) : + (PMF.uniformOfFintype α).map e = PMF.uniformOfFintype γ := by + classical + have hcard : Fintype.card α = Fintype.card γ := Fintype.card_congr e + ext c + rw [PMF.map_apply, PMF.uniformOfFintype_apply, tsum_eq_single (e.symm c)] + · simp_rw [PMF.uniformOfFintype_apply] + simp [hcard] + · intro a ha + simp_rw [PMF.uniformOfFintype_apply] + split_ifs with h + · exfalso + apply ha + simpa using congrArg e.symm h.symm + · simp + /-- Posterior probabilities `joint(a, b) / marginal(b)` sum to 1 when `b` is in the support of the marginal. -/ theorem posterior_hasSum (p : PMF α) (f : α → PMF β) (b : β) @@ -87,4 +111,23 @@ theorem posteriorDist_apply (p : PMF α) (f : α → PMF β) (b : β) (p.bind f) b := rfl +/-- If the output distribution of a channel does not depend on the input, then +conditioning on any output with positive probability leaves the prior unchanged. -/ +theorem posteriorDist_eq_prior_of_outputIndist (p : PMF α) (f : α → PMF β) + (h : ∀ a₀ a₁ : α, f a₀ = f a₁) + (b : β) (hb : b ∈ (p.bind f).support) : + posteriorDist p f b hb = p := by + ext a + rw [posteriorDist_apply, bind_pair_apply, PMF.bind_apply] + have hf : ∀ a', f a' b = f a b := fun a' => by rw [h a' a] + simp_rw [hf] + rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] + have hb' : (p.bind f) b ≠ 0 := (PMF.mem_support_iff _ _).mp hb + have hmarg : (p.bind f) b = f a b := by + rw [PMF.bind_apply] + simp_rw [hf] + rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] + exact ENNReal.mul_div_cancel_right (hmarg ▸ hb') + (ne_top_of_le_ne_top ENNReal.one_ne_top (PMF.coe_le_one _ _)) + end Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities diff --git a/Cslib/Crypto/Protocols/SecretSharing/Basic.lean b/Cslib/Crypto/Protocols/SecretSharing/Basic.lean new file mode 100644 index 000000000..1c342fb67 --- /dev/null +++ b/Cslib/Crypto/Protocols/SecretSharing/Basic.lean @@ -0,0 +1,107 @@ +/- +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.SecretSharing.Defs +public import Mathlib.Probability.Distributions.Uniform + +@[expose] public section + +/-! +# Secret Sharing: Basic Privacy Theory + +This file proves that the two standard information-theoretic formulations of +privacy agree for secret-sharing schemes: + +- view indistinguishability for unauthorized coalitions +- posterior equals prior after conditioning on one unauthorized view + +## Main results + +- `Cslib.Crypto.Protocols.SecretSharing.Scheme.perfectlyPrivate_of_viewIndist` +- `Cslib.Crypto.Protocols.SecretSharing.Scheme.viewIndist_of_perfectlyPrivate` +- `Cslib.Crypto.Protocols.SecretSharing.Scheme.perfectlyPrivate_iff_viewIndist` + +## References + +* [Adi Shamir, *How to Share a Secret*][Shamir1979] +* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020] +-/ + +namespace Cslib.Crypto.Protocols.SecretSharing + +open PMF ENNReal + +namespace Scheme + +variable {Secret Randomness Party Share : Type*} [DecidableEq Party] + +/-- View indistinguishability implies posterior privacy. -/ +theorem perfectlyPrivate_of_viewIndist + (scheme : Scheme Secret Randomness Party Share) + (h : scheme.ViewIndist) : + scheme.PerfectlyPrivate := by + intro s hs secretDist v hv + exact Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities.posteriorDist_eq_prior_of_outputIndist + (p := secretDist) (f := scheme.viewDist s) + (fun secret₀ secret₁ => h s hs secret₀ secret₁) v hv + +/-- Posterior privacy implies view indistinguishability for unauthorized +coalitions. -/ +theorem viewIndist_of_perfectlyPrivate + (scheme : Scheme Secret Randomness Party Share) + (h : scheme.PerfectlyPrivate) : + scheme.ViewIndist := by + classical + intro s hs secret₀ secret₁ + ext v + let secrets : Finset Secret := {secret₀, secret₁} + have hsecrets : secrets.Nonempty := ⟨secret₀, by simp [secrets]⟩ + let μ : PMF Secret := PMF.uniformOfFinset secrets hsecrets + by_cases hv : v ∈ (μ.bind (scheme.viewDist s)).support + · have hmarg : (μ.bind (scheme.viewDist s)) v ≠ 0 := + (PMF.mem_support_iff _ _).mp hv + have hmarg_top : (μ.bind (scheme.viewDist s)) v ≠ ∞ := + ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one (μ.bind (scheme.viewDist s)) v) + have hkey : + ∀ secret ∈ secrets, scheme.viewDist s secret v = (μ.bind (scheme.viewDist s)) v := by + intro secret hsecret + have hμ_mem : secret ∈ μ.support := + (PMF.mem_support_uniformOfFinset_iff hsecrets secret).2 hsecret + have hμ_ne : μ secret ≠ 0 := (PMF.mem_support_iff _ _).mp hμ_mem + have hμ_top : μ secret ≠ ∞ := + ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one μ secret) + have hpost : scheme.posteriorSecretDist s μ v hv secret = μ secret := + congrArg (fun q : PMF Secret => q secret) (h s hs μ v hv) + rw [posteriorSecretDist_apply, + Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities.bind_pair_apply] at hpost + have hpost' : + (μ.bind (scheme.viewDist s)) v * μ secret = + μ secret * (scheme.viewDist s secret) v := + (ENNReal.eq_div_iff hmarg hmarg_top).mp hpost.symm + rw [mul_comm ((μ.bind (scheme.viewDist s)) v) (μ secret)] at hpost' + exact (ENNReal.mul_right_inj hμ_ne hμ_top).mp hpost'.symm + exact (hkey secret₀ (by simp [secrets])).trans (hkey secret₁ (by simp [secrets])).symm + · have hkey : + ∀ secret ∈ secrets, scheme.viewDist s secret v = 0 := by + intro secret hsecret + by_contra hsecretv + have hμ_mem : secret ∈ μ.support := + (PMF.mem_support_uniformOfFinset_iff hsecrets secret).2 hsecret + exact hv <| (PMF.mem_support_bind_iff _ _ _).2 + ⟨secret, hμ_mem, (PMF.mem_support_iff _ _).2 hsecretv⟩ + rw [hkey secret₀ (by simp [secrets]), hkey secret₁ (by simp [secrets])] + +/-- Posterior privacy and view indistinguishability are equivalent. -/ +theorem perfectlyPrivate_iff_viewIndist + (scheme : Scheme Secret Randomness Party Share) : + scheme.PerfectlyPrivate ↔ scheme.ViewIndist := + ⟨viewIndist_of_perfectlyPrivate scheme, perfectlyPrivate_of_viewIndist scheme⟩ + +end Scheme + +end Cslib.Crypto.Protocols.SecretSharing diff --git a/Cslib/Crypto/Protocols/SecretSharing/Defs.lean b/Cslib/Crypto/Protocols/SecretSharing/Defs.lean new file mode 100644 index 000000000..e2d46b7ad --- /dev/null +++ b/Cslib/Crypto/Protocols/SecretSharing/Defs.lean @@ -0,0 +1,90 @@ +/- +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.PerfectSecrecy.PMFUtilities +public import Cslib.Crypto.Protocols.SecretSharing.Scheme + +@[expose] public section + +/-! +# Secret Sharing: Definitions + +Privacy for secret sharing is formalized by looking at the view induced on one +coalition, then comparing posterior and prior distributions on secrets. + +## Main definitions + +- `Cslib.Crypto.Protocols.SecretSharing.Scheme.shareDist`: + the full share distribution for one secret +- `Cslib.Crypto.Protocols.SecretSharing.Scheme.viewDist`: + the distribution of the restricted view for one coalition +- `Cslib.Crypto.Protocols.SecretSharing.Scheme.posteriorSecretDist`: + the posterior distribution on secrets after observing one view +- `Cslib.Crypto.Protocols.SecretSharing.Scheme.ViewIndist`: + indistinguishability of views for unauthorized coalitions +- `Cslib.Crypto.Protocols.SecretSharing.Scheme.PerfectlyPrivate`: + posterior equals prior for unauthorized coalitions + +## References + +* [Adi Shamir, *How to Share a Secret*][Shamir1979] +* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020] +-/ + +namespace Cslib.Crypto.Protocols.SecretSharing + +namespace Scheme + +variable {Secret Randomness Party Share : Type*} [DecidableEq Party] + +/-- The distribution of the full share assignment for one secret. -/ +noncomputable def shareDist (scheme : Scheme Secret Randomness Party Share) + (secret : Secret) : PMF (Party → Share) := + scheme.gen.map (fun r => scheme.share r secret) + +/-- The view distribution induced on the coalition `s`. -/ +noncomputable def viewDist (scheme : Scheme Secret Randomness Party Share) + (s : Finset Party) (secret : Secret) : PMF (s → Share) := + scheme.gen.map (fun r => scheme.view s r secret) + +/-- The posterior distribution on secrets after observing the coalition view +`v`. -/ +noncomputable def posteriorSecretDist + (scheme : Scheme Secret Randomness Party Share) + (s : Finset Party) (secretDist : PMF Secret) (v : s → Share) + (hv : v ∈ (secretDist.bind (scheme.viewDist s)).support) : PMF Secret := + Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities.posteriorDist + (p := secretDist) (f := scheme.viewDist s) v hv + +@[simp] +theorem posteriorSecretDist_apply + (scheme : Scheme Secret Randomness Party Share) + (s : Finset Party) (secretDist : PMF Secret) (v : s → Share) + (hv : v ∈ (secretDist.bind (scheme.viewDist s)).support) (secret : Secret) : + scheme.posteriorSecretDist s secretDist v hv secret = + (secretDist.bind fun secret' => + (scheme.viewDist s secret').bind fun v' => PMF.pure (secret', v')) (secret, v) / + (secretDist.bind (scheme.viewDist s)) v := + rfl + +/-- View indistinguishability for unauthorized coalitions. -/ +def ViewIndist (scheme : Scheme Secret Randomness Party Share) : Prop := + ∀ (s : Finset Party), ¬ scheme.authorized s → ∀ secret₀ secret₁ : Secret, + scheme.viewDist s secret₀ = scheme.viewDist s secret₁ + +/-- Perfect privacy for unauthorized coalitions: conditioning on a view does not +change the prior on secrets. -/ +def PerfectlyPrivate (scheme : Scheme Secret Randomness Party Share) : Prop := + ∀ (s : Finset Party) (_hs : ¬ scheme.authorized s) + (secretDist : PMF Secret) (v : s → Share) + (hv : v ∈ (secretDist.bind (scheme.viewDist s)).support), + scheme.posteriorSecretDist s secretDist v hv = secretDist + +end Scheme + +end Cslib.Crypto.Protocols.SecretSharing diff --git a/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean b/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean new file mode 100644 index 000000000..1e08455d6 --- /dev/null +++ b/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean @@ -0,0 +1,140 @@ +/- +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.LinearAlgebra.Lagrange + +@[expose] public section + +/-! +# Shamir Secret Sharing: Algebraic Core + +This internal file contains the interpolation lemmas used to prove correctness +of the public Shamir scheme construction and privacy of the corresponding +finite-field instance. +-/ + +noncomputable section + +namespace Cslib.Crypto.Protocols.SecretSharing.Shamir.Internal + +open Polynomial + +variable {F : Type*} [Field F] + +/-- The secret carried by a sharing polynomial is its value at `0`. -/ +def secret (p : F[X]) : F := + p.eval 0 + +@[simp] +theorem secret_eq_coeff_zero (p : F[X]) : secret p = p.coeff 0 := + (Polynomial.coeff_zero_eq_eval_zero p).symm + +/-- The tail polynomial determined by the first `n` coefficients. -/ +def tailPolynomial (n : ℕ) (coeffs : Fin n → F) : F[X] := + ↑((Polynomial.degreeLTEquiv F n).symm coeffs) + +@[simp] +theorem tailPolynomial_coeff (n : ℕ) (coeffs : Fin n → F) (i : Fin n) : + (tailPolynomial (F := F) n coeffs).coeff i = coeffs i := by + have h := congrFun (LinearEquiv.apply_symm_apply (Polynomial.degreeLTEquiv F n) coeffs) i + simpa [tailPolynomial, Polynomial.degreeLTEquiv] using h + +/-- `tailPolynomial n coeffs` has degree `< n` by construction. -/ +theorem tailPolynomial_degree_lt (n : ℕ) (coeffs : Fin n → F) : + (tailPolynomial (F := F) n coeffs).degree < n := + Polynomial.mem_degreeLT.1 + (((Polynomial.degreeLTEquiv F n).symm coeffs : Polynomial.degreeLT F n)).2 + +/-- The standard Shamir sharing polynomial `s + X * q(X)`. -/ +def sharingPolynomial (secretValue : F) (tail : F[X]) : F[X] := + C secretValue + X * tail + +@[simp] +theorem sharingPolynomial_eval (secretValue x : F) (tail : F[X]) : + (sharingPolynomial secretValue tail).eval x = secretValue + x * tail.eval x := by + simp [sharingPolynomial, mul_comm] + +@[simp] +theorem coeff_zero_sharingPolynomial (secretValue : F) (tail : F[X]) : + (sharingPolynomial secretValue tail).coeff 0 = secretValue := by + simp [sharingPolynomial] + +theorem secret_sharingPolynomial (secretValue : F) (tail : F[X]) : + secret (sharingPolynomial secretValue tail) = secretValue := by + simp [secret_eq_coeff_zero] + +/-- If the tail polynomial has degree `< n`, then the sharing polynomial has +degree `< n + 1`. -/ +theorem degree_sharingPolynomial_lt_succ (secretValue : F) (tail : F[X]) {n : ℕ} + (hdeg : tail.degree < n) : + (sharingPolynomial secretValue tail).degree < (n + 1 : WithBot ℕ) := by + have hadd := Polynomial.degree_add_le (C secretValue) ((X : F[X]) * tail) + simp only [sharingPolynomial] at hadd ⊢ + refine lt_of_le_of_lt hadd (max_lt ?_ ?_) + · exact lt_of_le_of_lt Polynomial.degree_C_le (by exact_mod_cast Nat.succ_pos n) + · by_cases htail : tail = 0 + · simp [htail] + · rw [mul_comm, Polynomial.degree_mul_X, Polynomial.degree_eq_natDegree htail] + have := Polynomial.degree_eq_natDegree htail ▸ hdeg + exact_mod_cast Nat.succ_lt_succ (by exact_mod_cast this) + +/-- The coefficient-vector version of `degree_sharingPolynomial_lt_succ`. -/ +theorem degree_sharingPolynomial_tailPolynomial_lt_succ + (secretValue : F) (n : ℕ) (coeffs : Fin n → F) : + (sharingPolynomial secretValue (tailPolynomial n coeffs)).degree < + (n + 1 : WithBot ℕ) := + degree_sharingPolynomial_lt_succ secretValue (tailPolynomial n coeffs) + (tailPolynomial_degree_lt n coeffs) + +variable {ι : Type*} [DecidableEq ι] + +/-- Reconstruct the secret from a coalition's share values by interpolating the +unique low-degree polynomial that matches them. -/ +def reconstruct (s : Finset ι) (x : ι → F) (σ : s → F) : F := + secret <| Lagrange.interpolate s.attach (fun i : s => x i) σ + +/-- If a polynomial of degree `< s.card` matches the observed share values on +the coalition `s`, reconstruction recovers its secret. -/ +theorem reconstruct_eq_secret_of_eval_eq + {s : Finset ι} {x : ι → F} {σ : s → F} {p : F[X]} + (hx : Set.InjOn x s) + (hvalues : ∀ i : s, σ i = p.eval (x i)) + (hdeg : p.degree < s.card) : + reconstruct s x σ = secret p := by + have hx' : Set.InjOn (fun i : s => x i) (s.attach : Finset s) := by + intro i _ j _ hij + apply Subtype.ext + exact hx i.property j.property hij + have hp : + p = Lagrange.interpolate s.attach (fun i : s => x i) σ := + Lagrange.eq_interpolate_of_eval_eq + (s := s.attach) + (v := fun i : s => x i) + (r := σ) + hx' + (by simpa using hdeg) + (by + intro i hi + simpa using (hvalues i).symm) + simpa [reconstruct, secret] using congrArg (fun q : F[X] => q.eval 0) hp.symm + +/-- Reconstruction succeeds on the values of a Shamir sharing polynomial once +the coalition is large enough. -/ +theorem reconstruct_sharingPolynomial_eq_secret + {s : Finset ι} {x : ι → F} {secretValue : F} {tail : F[X]} + (hx : Set.InjOn x s) + (hdeg : (sharingPolynomial secretValue tail).degree < s.card) : + reconstruct s x + (fun i : s => (sharingPolynomial secretValue tail).eval (x i)) = secretValue := by + rw [reconstruct_eq_secret_of_eval_eq + (σ := fun i : s => (sharingPolynomial secretValue tail).eval (x i)) + (p := sharingPolynomial secretValue tail) hx (by intro i; rfl) hdeg] + exact secret_sharingPolynomial secretValue tail + +end Cslib.Crypto.Protocols.SecretSharing.Shamir.Internal diff --git a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean new file mode 100644 index 000000000..130579f32 --- /dev/null +++ b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean @@ -0,0 +1,96 @@ +/- +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.Data.Finset.Basic +public import Mathlib.Probability.ProbabilityMassFunction.Monad + +@[expose] public section + +/-! +# Secret Sharing Schemes + +A secret-sharing scheme bundles both the deterministic sharing/reconstruction +interface and the distribution on randomness. Correctness is part of the scheme +interface; privacy is defined separately in +`Cslib.Crypto.Protocols.SecretSharing.Defs`. + +## Main definitions + +- `Cslib.Crypto.Protocols.SecretSharing.Scheme`: + a secret-sharing scheme with correctness +- `Cslib.Crypto.Protocols.SecretSharing.Scheme.view`: + the restricted shares seen by one coalition + +## References + +* [Adi Shamir, *How to Share a Secret*][Shamir1979] +* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020] +-/ + +namespace Cslib.Crypto.Protocols.SecretSharing + +/-- +A secret-sharing scheme over secret space `Secret`, randomness space +`Randomness`, party set `Party`, and share space `Share`. + +Correctness is deterministic: every authorized coalition reconstructs the +secret from the shares generated using any randomness seed. +-/ +structure Scheme (Secret Randomness Party Share : Type*) [DecidableEq Party] where + /-- The distribution used to sample the protocol's randomness. -/ + gen : PMF Randomness + /-- Sharing algorithm: one randomness seed determines one share per party. -/ + share : Randomness → Secret → Party → Share + /-- Reconstruction from a coalition's observed shares. -/ + reconstruct (s : Finset Party) : (s → Share) → Secret + /-- Authorized coalitions. -/ + authorized : Finset Party → Prop + /-- Authorization is monotone in the coalition. -/ + authorized_mono : + ∀ {s t : Finset Party}, s ⊆ t → authorized s → authorized t + /-- Authorized coalitions reconstruct the secret from the restricted view. -/ + correct : + ∀ (r : Randomness) (secret : Secret) (s : Finset Party), + authorized s → reconstruct s (fun i => share r secret i) = secret + +namespace Scheme + +variable {Secret Randomness Party Share : Type*} [DecidableEq Party] + +/-- The restricted shares observed by the coalition `s`. -/ +def view (scheme : Scheme Secret Randomness Party Share) (s : Finset Party) + (r : Randomness) (secret : Secret) : s → Share := + fun i => scheme.share r secret i + +@[simp] +theorem view_apply (scheme : Scheme Secret Randomness Party Share) (s : Finset Party) + (r : Randomness) (secret : Secret) (i : s) : + scheme.view s r secret i = scheme.share r secret i := + rfl + +/-- Authorized coalitions reconstruct the secret from the restricted view. -/ +theorem reconstruct_view_eq_secret + (scheme : Scheme Secret Randomness Party Share) + (r : Randomness) (secret : Secret) {s : Finset Party} + (hs : scheme.authorized s) : + scheme.reconstruct s (scheme.view s r secret) = secret := + scheme.correct r secret s hs + +/-- Any sub-coalition of an unauthorized coalition is unauthorized as well. -/ +theorem not_authorized_of_subset + (scheme : Scheme Secret Randomness Party Share) + {s t : Finset Party} (hst : s ⊆ t) + (ht : ¬ scheme.authorized t) : + ¬ scheme.authorized s := by + intro hs + exact ht (scheme.authorized_mono hst hs) + +end Scheme + +end Cslib.Crypto.Protocols.SecretSharing diff --git a/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean new file mode 100644 index 000000000..d0af9a44d --- /dev/null +++ b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean @@ -0,0 +1,220 @@ +/- +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.PerfectSecrecy.PMFUtilities +public import Cslib.Crypto.Protocols.SecretSharing.Scheme +public import Cslib.Crypto.Protocols.SecretSharing.Internal.ShamirAlgebra +public import Mathlib.Probability.Distributions.Uniform + +@[expose] public section + +/-! +# Shamir Secret Sharing + +This module presents a hardened API for finite-party Shamir secret sharing +through the abstract `SecretSharing.Scheme` interface. + +The secure public constructors require two pieces of data: + +- public parameters consisting of a threshold together with distinct, nonzero + evaluation points for a finite party set +- a translation-invariant sampler on the tail coefficients + +Translation invariance is exactly the symmetry used in the privacy proof. The +canonical finite-field instance is obtained by taking the sampler to be uniform. +For correctness-only arguments and tests, the internal namespace still exposes a +raw constructor with an arbitrary coefficient distribution. + +## Main definitions + +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.Params`: + the threshold and public evaluation points +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.Randomness`: + the vector of tail coefficients +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.TailSampler`: + a translation-invariant distribution on tail coefficients +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.schemeWith`: + Shamir's scheme with a privacy-preserving tail sampler +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.scheme`: + the corresponding finite-field scheme with uniform randomness + +## Main results + +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.reconstruct_view_eq_secret`: + any authorized coalition reconstructs the secret +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.authorized_univ`: + the full party set is always authorized + +## Notes + +The public share type is just the field `F`: the evaluation points are fixed in +`Params`, so one share consists only of the corresponding field value. + +## References + +* [Adi Shamir, *How to Share a Secret*][Shamir1979] +* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020] +-/ + +noncomputable section + +namespace Cslib.Crypto.Protocols.SecretSharing.Shamir + +open Polynomial + +variable {F Party : Type*} [Field F] [Fintype Party] [DecidableEq Party] + +/-- Public parameters for a finite Shamir secret-sharing instance. The threshold +is bundled with the evaluation points so the API can enforce the standard +non-vacuous `threshold < number of parties` side condition. -/ +structure Params (F : Type*) [Zero F] (Party : Type*) [Fintype Party] where + /-- A coalition of size `threshold + 1` is the first authorized size. -/ + threshold : ℕ + /-- Standard Shamir sharing requires `threshold < number of parties`. -/ + threshold_lt_card : threshold < Fintype.card Party + /-- The public evaluation point assigned to each party. -/ + point : Party → F + /-- Distinct parties receive distinct evaluation points. -/ + point_injective : Function.Injective point + /-- Standard Shamir sharing forbids the point `0`, which would reveal the + secret directly. -/ + point_nonzero : ∀ i : Party, point i ≠ 0 + +/-- The random coefficients of the degree-`threshold - 1` tail polynomial. -/ +abbrev Randomness (params : Params F Party) := Fin params.threshold → F + +/-- A coalition is authorized exactly when it contains at least +`params.threshold + 1` parties. -/ +def authorized (params : Params F Party) (s : Finset Party) : Prop := + params.threshold + 1 ≤ s.card + +/-- Because `params.threshold < |Party|`, the full party set can always +reconstruct the secret. -/ +theorem authorized_univ {F Party : Type*} [Field F] [Fintype Party] + (params : Params F Party) : + authorized params (Finset.univ : Finset Party) := by + simpa [authorized] using Nat.succ_le_of_lt params.threshold_lt_card + +namespace Internal + +/-- Correctness-only Shamir skeleton with an arbitrary coefficient sampler. This +constructor does not carry any privacy guarantee and is intended for internal +proofs and tests. -/ +noncomputable def rawSchemeWith (params : Params F Party) + (gen : PMF (Randomness params)) : + SecretSharing.Scheme F (Randomness params) Party F where + gen := gen + share coeffs secretValue i := + (sharingPolynomial secretValue (tailPolynomial params.threshold coeffs)).eval (params.point i) + reconstruct s σ := reconstruct s params.point σ + authorized := authorized params + authorized_mono := by + intro s u hsu hs + exact le_trans hs (Finset.card_le_card hsu) + correct coeffs secretValue s hs := by + have hdeg₀ : + (sharingPolynomial secretValue (tailPolynomial params.threshold coeffs)).degree < + (params.threshold + 1 : WithBot ℕ) := + degree_sharingPolynomial_tailPolynomial_lt_succ secretValue params.threshold coeffs + have hdeg : + (sharingPolynomial secretValue (tailPolynomial params.threshold coeffs)).degree < s.card := + lt_of_lt_of_le hdeg₀ (by exact_mod_cast hs) + simpa using + reconstruct_sharingPolynomial_eq_secret + (x := params.point) + (secretValue := secretValue) + (tail := tailPolynomial params.threshold coeffs) + (params.point_injective.injOn) + hdeg + +@[simp] +theorem rawSchemeWith_authorized_iff (params : Params F Party) + (gen : PMF (Randomness params)) (s : Finset Party) : + (rawSchemeWith params gen).authorized s ↔ params.threshold + 1 ≤ s.card := + Iff.rfl + +@[simp] +theorem rawSchemeWith_share_eq_eval (params : Params F Party) + (gen : PMF (Randomness params)) (coeffs : Randomness params) + (secretValue : F) (i : Party) : + (rawSchemeWith params gen).share coeffs secretValue i = + (sharingPolynomial secretValue + (tailPolynomial params.threshold coeffs)).eval (params.point i) := + rfl + +end Internal + +/-- A sampler on Shamir tail coefficients is privacy-compatible when its +distribution is invariant under translation by any coefficient vector. This is +the exact symmetry needed in the privacy proof. -/ +structure TailSampler (params : Params F Party) where + /-- The underlying coefficient distribution. -/ + gen : PMF (Randomness params) + /-- Translating the coefficients does not change the distribution. -/ + map_add_eq_self : ∀ δ : Randomness params, gen.map (fun coeffs => coeffs + δ) = gen + +private def coeffTranslate {params : Params F Party} (δ : Randomness params) : + Randomness params ≃ Randomness params where + toFun coeffs := coeffs + δ + invFun coeffs := coeffs - δ + left_inv coeffs := by simp + right_inv coeffs := by simp + +/-- Uniform tail coefficients form the canonical privacy-compatible sampler. -/ +noncomputable def uniformTailSampler (params : Params F Party) + [Fintype F] [Nonempty F] : TailSampler params where + gen := PMF.uniformOfFintype (Randomness params) + map_add_eq_self δ := by + simpa [coeffTranslate] using + (Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities.uniformOfFintype_map_equiv + (coeffTranslate (params := params) δ)) + +/-- Shamir's scheme built from a privacy-compatible tail sampler. -/ +noncomputable def schemeWith (params : Params F Party) (sampler : TailSampler params) : + SecretSharing.Scheme F (Randomness params) Party F := + Internal.rawSchemeWith params sampler.gen + +/-- The canonical finite-field Shamir scheme with uniformly sampled tail +coefficients. -/ +noncomputable def scheme (params : Params F Party) + [Fintype F] [Nonempty F] : + SecretSharing.Scheme F (Randomness params) Party F := + schemeWith params (uniformTailSampler params) + +@[simp] +theorem schemeWith_authorized_iff (params : Params F Party) + (sampler : TailSampler params) (s : Finset Party) : + (schemeWith params sampler).authorized s ↔ params.threshold + 1 ≤ s.card := + Iff.rfl + +@[simp] +theorem scheme_authorized_iff (params : Params F Party) + [Fintype F] [Nonempty F] (s : Finset Party) : + (scheme params).authorized s ↔ params.threshold + 1 ≤ s.card := + Iff.rfl + +@[simp] +theorem schemeWith_share_eq_eval (params : Params F Party) + (sampler : TailSampler params) (coeffs : Randomness params) + (secretValue : F) (i : Party) : + (schemeWith params sampler).share coeffs secretValue i = + (Internal.sharingPolynomial secretValue + (Internal.tailPolynomial params.threshold coeffs)).eval (params.point i) := + rfl + +/-- Any authorized coalition reconstructs the secret from the shares it sees. -/ +theorem reconstruct_view_eq_secret + (params : Params F Party) (sampler : TailSampler params) + (coeffs : Randomness params) (secretValue : F) {s : Finset Party} + (hs : (schemeWith params sampler).authorized s) : + (schemeWith params sampler).reconstruct s + ((schemeWith params sampler).view s coeffs secretValue) = secretValue := + SecretSharing.Scheme.reconstruct_view_eq_secret + (schemeWith params sampler) coeffs secretValue hs + +end Cslib.Crypto.Protocols.SecretSharing.Shamir diff --git a/Cslib/Crypto/Protocols/SecretSharing/ShamirPrivacy.lean b/Cslib/Crypto/Protocols/SecretSharing/ShamirPrivacy.lean new file mode 100644 index 000000000..f8e4b0656 --- /dev/null +++ b/Cslib/Crypto/Protocols/SecretSharing/ShamirPrivacy.lean @@ -0,0 +1,198 @@ +/- +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.SecretSharing.Basic +public import Cslib.Crypto.Protocols.SecretSharing.Shamir + +@[expose] public section + +/-! +# Shamir Secret Sharing: Privacy + +This file proves the standard privacy statement for the public +`SecretSharing.Scheme` interface instantiated by Shamir secret sharing. + +The key assumption is no longer “uniform coefficients” at the API boundary. +Instead, the public constructor `Shamir.schemeWith` accepts only +translation-invariant tail samplers, and that symmetry is exactly what the +privacy proof uses. The canonical finite-field construction arises by taking +the sampler to be uniform. + +## Main results + +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.schemeWith_viewIndist`: + unauthorized coalitions have secret-independent view distributions for any + translation-invariant sampler +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.viewIndist`: + the canonical finite-field scheme has secret-independent views +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.schemeWith_perfectlyPrivate`: + any translation-invariant Shamir instance has posterior privacy +- `Cslib.Crypto.Protocols.SecretSharing.Shamir.perfectlyPrivate`: + the canonical finite-field scheme has posterior privacy + +## References + +* [Adi Shamir, *How to Share a Secret*][Shamir1979] +* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020] +-/ + +noncomputable section + +namespace Cslib.Crypto.Protocols.SecretSharing.Shamir + +open Polynomial + +variable {F Party : Type*} [Field F] [Fintype Party] [DecidableEq Party] + +/-- The interpolation correction polynomial that compensates for changing the +secret from `secret₀` to `secret₁` on the observed coalition. -/ +private noncomputable def privacyCorrectionPolynomial + (params : Params F Party) (s : Finset Party) + (secret₀ secret₁ : F) : F[X] := + Lagrange.interpolate s.attach (fun i : s => params.point i) + (fun i : s => (secret₀ - secret₁) / params.point i) + +private theorem points_injOn_subtype {F Party : Type*} [Field F] [Fintype Party] + (params : Params F Party) (s : Finset Party) : + Set.InjOn (fun i : s => params.point i) (s.attach : Finset s) := by + intro i _ j _ hij + apply Subtype.ext + exact params.point_injective hij + +/-- The correction polynomial has the prescribed values on the observed +evaluation points. -/ +private theorem privacyCorrectionPolynomial_eval + (params : Params F Party) (s : Finset Party) + (secret₀ secret₁ : F) (i : s) : + (privacyCorrectionPolynomial (F := F) params s secret₀ secret₁).eval (params.point i) = + (secret₀ - secret₁) / params.point i := by + simpa using + (Lagrange.eval_interpolate_at_node + (s := s.attach) + (v := fun j : s => params.point j) + (r := fun j : s => (secret₀ - secret₁) / params.point j) + (points_injOn_subtype (F := F) params s) + (by simp)) + +private theorem privacyCorrectionPolynomial_degree_lt + (params : Params F Party) (s : Finset Party) + (secret₀ secret₁ : F) (hcard : s.card ≤ params.threshold) : + (privacyCorrectionPolynomial (F := F) params s secret₀ secret₁).degree < + params.threshold := by + refine lt_of_lt_of_le + (Lagrange.degree_interpolate_lt + (s := s.attach) + (v := fun i : s => params.point i) + (r := fun i : s => (secret₀ - secret₁) / params.point i) + (points_injOn_subtype (F := F) params s)) + ?_ + simpa using hcard + +/-- Re-encode the correction polynomial as a coefficient vector in the Shamir +randomness space. -/ +private noncomputable def privacyCorrection + (params : Params F Party) (s : Finset Party) + (hcard : s.card ≤ params.threshold) + (secret₀ secret₁ : F) : Randomness params := + Polynomial.degreeLTEquiv F params.threshold + ⟨privacyCorrectionPolynomial (F := F) params s secret₀ secret₁, + Polynomial.mem_degreeLT.2 + (privacyCorrectionPolynomial_degree_lt (F := F) params s secret₀ secret₁ hcard)⟩ + +private theorem tailPolynomial_add {F Party : Type*} [Field F] [Fintype Party] + (params : Params F Party) + (a b : Randomness params) : + Internal.tailPolynomial (F := F) params.threshold (a + b) = + Internal.tailPolynomial params.threshold a + + Internal.tailPolynomial params.threshold b := by + simp [Internal.tailPolynomial] + +private theorem tailPolynomial_privacyCorrection + (params : Params F Party) (s : Finset Party) + (hcard : s.card ≤ params.threshold) + (secret₀ secret₁ : F) : + Internal.tailPolynomial (F := F) params.threshold + (privacyCorrection (F := F) params s hcard secret₀ secret₁) = + privacyCorrectionPolynomial (F := F) params s secret₀ secret₁ := by + simp [privacyCorrection, Internal.tailPolynomial] + +/-- Changing the secret can be compensated by translating the tail coefficients, +so the observed coalition view is unchanged. -/ +private theorem view_eq_view_add_privacyCorrection + (params : Params F Party) (s : Finset Party) + (hcard : s.card ≤ params.threshold) + (sampler : TailSampler params) + (secret₀ secret₁ : F) (coeffs : Randomness params) : + (schemeWith params sampler).view s coeffs secret₀ = + (schemeWith params sampler).view s + (coeffs + privacyCorrection (F := F) params s hcard secret₀ secret₁) secret₁ := by + ext i + rw [SecretSharing.Scheme.view_apply, SecretSharing.Scheme.view_apply] + rw [schemeWith_share_eq_eval, schemeWith_share_eq_eval] + rw [Internal.sharingPolynomial_eval, Internal.sharingPolynomial_eval] + rw [tailPolynomial_add, eval_add, tailPolynomial_privacyCorrection] + rw [privacyCorrectionPolynomial_eval (F := F) params s secret₀ secret₁ i] + field_simp [params.point_nonzero i] + ring + +/-- Coalitions of size at most `params.threshold` have secret-independent view +distributions for any translation-invariant Shamir sampler. -/ +theorem schemeWith_viewIndist (params : Params F Party) + (sampler : TailSampler params) : + (schemeWith params sampler).ViewIndist := by + intro s hs secret₀ secret₁ + have hcard : s.card ≤ params.threshold := by + have hs' : ¬ params.threshold + 1 ≤ s.card := by + simpa [schemeWith_authorized_iff] using hs + exact Nat.lt_succ_iff.mp (Nat.not_le.mp hs') + unfold SecretSharing.Scheme.viewDist + calc + sampler.gen.map + (fun coeffs => (schemeWith params sampler).view s coeffs secret₀) = + sampler.gen.map + (fun coeffs => (schemeWith params sampler).view s + (coeffs + privacyCorrection (F := F) params s hcard secret₀ secret₁) + secret₁) := by + congr + funext coeffs + exact view_eq_view_add_privacyCorrection + (F := F) params s hcard sampler secret₀ secret₁ coeffs + _ = (sampler.gen.map + (fun coeffs => coeffs + privacyCorrection (F := F) params s hcard secret₀ secret₁)).map + (fun coeffs => (schemeWith params sampler).view s coeffs secret₁) := by + rw [PMF.map_comp] + rfl + _ = sampler.gen.map + (fun coeffs => (schemeWith params sampler).view s coeffs secret₁) := by + rw [sampler.map_add_eq_self] + +/-- The canonical finite-field Shamir scheme has secret-independent view +distributions for unauthorized coalitions. -/ +theorem viewIndist (params : Params F Party) + [Fintype F] [Nonempty F] : + (scheme params).ViewIndist := by + simpa [scheme] using + (schemeWith_viewIndist (F := F) params (uniformTailSampler params)) + +/-- Any translation-invariant Shamir instance is perfectly private against +unauthorized coalitions. -/ +theorem schemeWith_perfectlyPrivate (params : Params F Party) + (sampler : TailSampler params) : + (schemeWith params sampler).PerfectlyPrivate := + SecretSharing.Scheme.perfectlyPrivate_of_viewIndist + (schemeWith params sampler) (schemeWith_viewIndist (F := F) params sampler) + +/-- The canonical finite-field Shamir scheme is perfectly private against +unauthorized coalitions. -/ +theorem perfectlyPrivate (params : Params F Party) + [Fintype F] [Nonempty F] : + (scheme params).PerfectlyPrivate := + SecretSharing.Scheme.perfectlyPrivate_of_viewIndist + (scheme params) (viewIndist (F := F) params) + +end Cslib.Crypto.Protocols.SecretSharing.Shamir diff --git a/CslibTests.lean b/CslibTests.lean index 73292aef3..b98ac122d 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -12,3 +12,5 @@ public import CslibTests.ImportWithMathlib public import CslibTests.LTS public import CslibTests.LambdaCalculus public import CslibTests.Reduction +public import CslibTests.Shamir +public import CslibTests.ShamirPrivacy diff --git a/CslibTests/Shamir.lean b/CslibTests/Shamir.lean new file mode 100644 index 000000000..2d486dcbf --- /dev/null +++ b/CslibTests/Shamir.lean @@ -0,0 +1,67 @@ +import Cslib + +namespace CslibTests + +open Cslib +open Cslib.Crypto.Protocols.SecretSharing + +def trivialParams : Shamir.Params ℚ (Fin 1) where + threshold := 0 + threshold_lt_card := by decide + point _ := 1 + point_injective := by + intro i j _ + fin_cases i + fin_cases j + rfl + point_nonzero _ := by norm_num + +def rationalParams : Shamir.Params ℚ (Fin 2) where + threshold := 1 + threshold_lt_card := by decide + point i := (i : ℚ) + 1 + point_injective := by + intro i j hij + fin_cases i + · fin_cases j + · rfl + · simp at hij + · fin_cases j + · simp at hij + · rfl + point_nonzero i := by + fin_cases i <;> norm_num + +noncomputable def trivialRawScheme : + Scheme ℚ (Shamir.Randomness trivialParams) (Fin 1) ℚ := + Shamir.Internal.rawSchemeWith trivialParams (PMF.pure (fun i => nomatch i)) + +def rationalTail : Shamir.Randomness rationalParams := fun _ => 7 + +noncomputable def rationalRawScheme : + Scheme ℚ (Shamir.Randomness rationalParams) (Fin 2) ℚ := + Shamir.Internal.rawSchemeWith rationalParams (PMF.pure rationalTail) + +example : Shamir.authorized trivialParams (Finset.univ : Finset (Fin 1)) := by + exact Shamir.authorized_univ trivialParams + +example : ¬ Shamir.authorized rationalParams ({0} : Finset (Fin 2)) := by + simp [Shamir.authorized, rationalParams] + +example : + trivialRawScheme.reconstruct + (Finset.univ : Finset (Fin 1)) + (trivialRawScheme.view (Finset.univ : Finset (Fin 1)) + (fun i => nomatch i) (5 : ℚ)) = 5 := by + exact Scheme.reconstruct_view_eq_secret + trivialRawScheme (fun i => nomatch i) (5 : ℚ) (Shamir.authorized_univ trivialParams) + +example : + rationalRawScheme.reconstruct + (Finset.univ : Finset (Fin 2)) + (rationalRawScheme.view (Finset.univ : Finset (Fin 2)) + rationalTail (5 : ℚ)) = 5 := by + exact Scheme.reconstruct_view_eq_secret + rationalRawScheme rationalTail (5 : ℚ) (Shamir.authorized_univ rationalParams) + +end CslibTests diff --git a/CslibTests/ShamirPrivacy.lean b/CslibTests/ShamirPrivacy.lean new file mode 100644 index 000000000..b881a1ac5 --- /dev/null +++ b/CslibTests/ShamirPrivacy.lean @@ -0,0 +1,66 @@ +import Cslib +import Mathlib.Algebra.Field.ZMod + +namespace CslibTests + +open Cslib +open Cslib.Crypto.Protocols.SecretSharing + +instance : Fact (Nat.Prime 5) := ⟨by decide⟩ + +def privacyParams : Shamir.Params (ZMod 5) (Fin 3) where + threshold := 1 + threshold_lt_card := by decide + point + | 0 => 1 + | 1 => 2 + | 2 => 3 + point_injective := by decide + point_nonzero i := by + fin_cases i <;> decide + +def zeroTail : Shamir.Randomness privacyParams := fun _ => 0 + +noncomputable def insecureRawScheme : + Scheme (ZMod 5) (Shamir.Randomness privacyParams) (Fin 3) (ZMod 5) := + Shamir.Internal.rawSchemeWith privacyParams (PMF.pure zeroTail) + +def singletonCoalition : Finset (Fin 3) := {0} + +example : ¬ Shamir.authorized privacyParams singletonCoalition := by + simp [singletonCoalition, Shamir.authorized, privacyParams] + +example : + insecureRawScheme.view singletonCoalition zeroTail (0 : ZMod 5) ≠ + insecureRawScheme.view singletonCoalition zeroTail (3 : ZMod 5) := by + intro h + have h0 := congrFun h ⟨0, by simp [singletonCoalition]⟩ + have h0' : (3 : ZMod 5) = 0 := by + simpa [insecureRawScheme, singletonCoalition, Shamir.Internal.tailPolynomial, + Shamir.Internal.sharingPolynomial_eval, privacyParams] using h0 + exact (by decide : (3 : ZMod 5) ≠ 0) h0' + +example : + (Shamir.scheme privacyParams).viewDist singletonCoalition (0 : ZMod 5) = + (Shamir.scheme privacyParams).viewDist singletonCoalition (3 : ZMod 5) := by + have hs : ¬ (Shamir.scheme privacyParams).authorized singletonCoalition := by + simp [Shamir.scheme_authorized_iff, singletonCoalition, privacyParams] + exact Shamir.viewIndist (F := ZMod 5) privacyParams + singletonCoalition hs 0 3 + +example (v : singletonCoalition → ZMod 5) + (hv : v ∈ ((PMF.uniformOfFintype (ZMod 5)).bind + ((Shamir.scheme privacyParams).viewDist singletonCoalition)).support) : + (Shamir.scheme privacyParams).posteriorSecretDist + singletonCoalition + (PMF.uniformOfFintype (ZMod 5)) + v + hv = + PMF.uniformOfFintype (ZMod 5) := by + have hs : ¬ (Shamir.scheme privacyParams).authorized singletonCoalition := by + simp [Shamir.scheme_authorized_iff, singletonCoalition, privacyParams] + exact Shamir.perfectlyPrivate (F := ZMod 5) privacyParams + singletonCoalition hs + (PMF.uniformOfFintype (ZMod 5)) v hv + +end CslibTests diff --git a/references.bib b/references.bib index 1f8c0dc51..706ae0f82 100644 --- a/references.bib +++ b/references.bib @@ -133,6 +133,19 @@ @book{ KatzLindell2020 isbn = {9780815354369} } +@article{ Shamir1979, + author = {Adi Shamir}, + title = {How to Share a Secret}, + journal = {Communications of the ACM}, + volume = {22}, + number = {11}, + pages = {612--613}, + year = {1979}, + month = nov, + url = {https://doi.org/10.1145/359168.359176}, + doi = {10.1145/359168.359176} +} + @inproceedings{ Kiselyov2015, author = {Kiselyov, Oleg and Ishii, Hiromi}, title = {Freer Monads, More Extensible Effects}, From 2f9d8554888fc9f2199a6ea7b11f0c81faedd6c2 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 22 Apr 2026 12:26:49 -0400 Subject: [PATCH 2/4] Address Shamir review comments --- .../Crypto/Protocols/SecretSharing/Basic.lean | 4 +- .../SecretSharing/Internal/ShamirAlgebra.lean | 117 +++++++++--------- .../Protocols/SecretSharing/Shamir.lean | 17 ++- 3 files changed, 71 insertions(+), 67 deletions(-) diff --git a/Cslib/Crypto/Protocols/SecretSharing/Basic.lean b/Cslib/Crypto/Protocols/SecretSharing/Basic.lean index 1c342fb67..de9a0f19d 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Basic.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Basic.lean @@ -46,7 +46,7 @@ theorem perfectlyPrivate_of_viewIndist (h : scheme.ViewIndist) : scheme.PerfectlyPrivate := by intro s hs secretDist v hv - exact Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities.posteriorDist_eq_prior_of_outputIndist + exact PerfectSecrecy.PMFUtilities.posteriorDist_eq_prior_of_outputIndist (p := secretDist) (f := scheme.viewDist s) (fun secret₀ secret₁ => h s hs secret₀ secret₁) v hv @@ -78,7 +78,7 @@ theorem viewIndist_of_perfectlyPrivate have hpost : scheme.posteriorSecretDist s μ v hv secret = μ secret := congrArg (fun q : PMF Secret => q secret) (h s hs μ v hv) rw [posteriorSecretDist_apply, - Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities.bind_pair_apply] at hpost + PerfectSecrecy.PMFUtilities.bind_pair_apply] at hpost have hpost' : (μ.bind (scheme.viewDist s)) v * μ secret = μ secret * (scheme.viewDist s secret) v := diff --git a/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean b/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean index 1e08455d6..99637f2c5 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean @@ -27,14 +27,6 @@ open Polynomial variable {F : Type*} [Field F] -/-- The secret carried by a sharing polynomial is its value at `0`. -/ -def secret (p : F[X]) : F := - p.eval 0 - -@[simp] -theorem secret_eq_coeff_zero (p : F[X]) : secret p = p.coeff 0 := - (Polynomial.coeff_zero_eq_eval_zero p).symm - /-- The tail polynomial determined by the first `n` coefficients. -/ def tailPolynomial (n : ℕ) (coeffs : Fin n → F) : F[X] := ↑((Polynomial.degreeLTEquiv F n).symm coeffs) @@ -60,29 +52,44 @@ theorem sharingPolynomial_eval (secretValue x : F) (tail : F[X]) : (sharingPolynomial secretValue tail).eval x = secretValue + x * tail.eval x := by simp [sharingPolynomial, mul_comm] -@[simp] theorem coeff_zero_sharingPolynomial (secretValue : F) (tail : F[X]) : (sharingPolynomial secretValue tail).coeff 0 = secretValue := by simp [sharingPolynomial] -theorem secret_sharingPolynomial (secretValue : F) (tail : F[X]) : - secret (sharingPolynomial secretValue tail) = secretValue := by - simp [secret_eq_coeff_zero] +@[simp] +theorem constantCoeff_sharingPolynomial (secretValue : F) (tail : F[X]) : + (sharingPolynomial secretValue tail).constantCoeff = secretValue := by + simpa [Polynomial.constantCoeff_apply] using coeff_zero_sharingPolynomial secretValue tail + +/-- If the tail polynomial has degree `< n`, then the sharing polynomial has +natural degree at most `n`. -/ +theorem natDegree_sharingPolynomial_le (secretValue : F) (tail : F[X]) {n : ℕ} + (hdeg : tail.degree < n) : + (sharingPolynomial secretValue tail).natDegree ≤ n := by + rw [sharingPolynomial] + refine (Polynomial.natDegree_add_le _ _).trans ?_ + rw [max_le_iff] + constructor + · rw [Polynomial.natDegree_C] + exact Nat.zero_le n + · by_cases htail : tail = 0 + · simp [htail] + · rw [Polynomial.natDegree_X_mul htail] + have htailDegree : tail.natDegree < n := by + have := hdeg + rw [Polynomial.degree_eq_natDegree htail] at this + exact_mod_cast this + exact Nat.succ_le_of_lt htailDegree /-- If the tail polynomial has degree `< n`, then the sharing polynomial has degree `< n + 1`. -/ theorem degree_sharingPolynomial_lt_succ (secretValue : F) (tail : F[X]) {n : ℕ} (hdeg : tail.degree < n) : (sharingPolynomial secretValue tail).degree < (n + 1 : WithBot ℕ) := by - have hadd := Polynomial.degree_add_le (C secretValue) ((X : F[X]) * tail) - simp only [sharingPolynomial] at hadd ⊢ - refine lt_of_le_of_lt hadd (max_lt ?_ ?_) - · exact lt_of_le_of_lt Polynomial.degree_C_le (by exact_mod_cast Nat.succ_pos n) - · by_cases htail : tail = 0 - · simp [htail] - · rw [mul_comm, Polynomial.degree_mul_X, Polynomial.degree_eq_natDegree htail] - have := Polynomial.degree_eq_natDegree htail ▸ hdeg - exact_mod_cast Nat.succ_lt_succ (by exact_mod_cast this) + by_cases hsharing : sharingPolynomial secretValue tail = 0 + · simp [hsharing] + · rw [Polynomial.degree_eq_natDegree hsharing] + exact_mod_cast Nat.lt_succ_of_le (natDegree_sharingPolynomial_le secretValue tail hdeg) /-- The coefficient-vector version of `degree_sharingPolynomial_lt_succ`. -/ theorem degree_sharingPolynomial_tailPolynomial_lt_succ @@ -92,49 +99,39 @@ theorem degree_sharingPolynomial_tailPolynomial_lt_succ degree_sharingPolynomial_lt_succ secretValue (tailPolynomial n coeffs) (tailPolynomial_degree_lt n coeffs) -variable {ι : Type*} [DecidableEq ι] - -/-- Reconstruct the secret from a coalition's share values by interpolating the -unique low-degree polynomial that matches them. -/ -def reconstruct (s : Finset ι) (x : ι → F) (σ : s → F) : F := - secret <| Lagrange.interpolate s.attach (fun i : s => x i) σ - -/-- If a polynomial of degree `< s.card` matches the observed share values on -the coalition `s`, reconstruction recovers its secret. -/ -theorem reconstruct_eq_secret_of_eval_eq - {s : Finset ι} {x : ι → F} {σ : s → F} {p : F[X]} - (hx : Set.InjOn x s) - (hvalues : ∀ i : s, σ i = p.eval (x i)) - (hdeg : p.degree < s.card) : - reconstruct s x σ = secret p := by - have hx' : Set.InjOn (fun i : s => x i) (s.attach : Finset s) := by - intro i _ j _ hij - apply Subtype.ext - exact hx i.property j.property hij +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Reconstruct the secret from finitely indexed share values by interpolating +the unique low-degree polynomial that matches them. -/ +def reconstruct (x σ : ι → F) : F := + (Lagrange.interpolate Finset.univ x σ).constantCoeff + +/-- Reconstruction recovers the constant coefficient of any low-degree +polynomial from its values at distinct points. -/ +theorem reconstruct_eq_constantCoeff_of_eval_eq + {x : ι → F} {p : F[X]} + (hx : Function.Injective x) + (hdeg : p.degree < Fintype.card ι) : + reconstruct x (fun i => p.eval (x i)) = p.constantCoeff := by have hp : - p = Lagrange.interpolate s.attach (fun i : s => x i) σ := - Lagrange.eq_interpolate_of_eval_eq - (s := s.attach) - (v := fun i : s => x i) - (r := σ) - hx' + p = Lagrange.interpolate Finset.univ x (fun i => p.eval (x i)) := + Lagrange.eq_interpolate + (s := Finset.univ) + (v := x) + hx.injOn (by simpa using hdeg) - (by - intro i hi - simpa using (hvalues i).symm) - simpa [reconstruct, secret] using congrArg (fun q : F[X] => q.eval 0) hp.symm + simpa [reconstruct] using congrArg Polynomial.constantCoeff hp.symm /-- Reconstruction succeeds on the values of a Shamir sharing polynomial once -the coalition is large enough. -/ +the finite index type is large enough. -/ theorem reconstruct_sharingPolynomial_eq_secret - {s : Finset ι} {x : ι → F} {secretValue : F} {tail : F[X]} - (hx : Set.InjOn x s) - (hdeg : (sharingPolynomial secretValue tail).degree < s.card) : - reconstruct s x - (fun i : s => (sharingPolynomial secretValue tail).eval (x i)) = secretValue := by - rw [reconstruct_eq_secret_of_eval_eq - (σ := fun i : s => (sharingPolynomial secretValue tail).eval (x i)) - (p := sharingPolynomial secretValue tail) hx (by intro i; rfl) hdeg] - exact secret_sharingPolynomial secretValue tail + {x : ι → F} {secretValue : F} {tail : F[X]} + (hx : Function.Injective x) + (hdeg : (sharingPolynomial secretValue tail).degree < Fintype.card ι) : + reconstruct x + (fun i => (sharingPolynomial secretValue tail).eval (x i)) = secretValue := by + rw [reconstruct_eq_constantCoeff_of_eval_eq + (p := sharingPolynomial secretValue tail) hx hdeg] + exact constantCoeff_sharingPolynomial secretValue tail end Cslib.Crypto.Protocols.SecretSharing.Shamir.Internal diff --git a/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean index d0af9a44d..58520ac63 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean @@ -111,7 +111,7 @@ noncomputable def rawSchemeWith (params : Params F Party) gen := gen share coeffs secretValue i := (sharingPolynomial secretValue (tailPolynomial params.threshold coeffs)).eval (params.point i) - reconstruct s σ := reconstruct s params.point σ + reconstruct s σ := reconstruct (fun i : s => params.point i) σ authorized := authorized params authorized_mono := by intro s u hsu hs @@ -122,14 +122,21 @@ noncomputable def rawSchemeWith (params : Params F Party) (params.threshold + 1 : WithBot ℕ) := degree_sharingPolynomial_tailPolynomial_lt_succ secretValue params.threshold coeffs have hdeg : - (sharingPolynomial secretValue (tailPolynomial params.threshold coeffs)).degree < s.card := - lt_of_lt_of_le hdeg₀ (by exact_mod_cast hs) + (sharingPolynomial secretValue (tailPolynomial params.threshold coeffs)).degree < + Fintype.card s := by + simpa using + (lt_of_lt_of_le hdeg₀ (by exact_mod_cast hs) : + (sharingPolynomial secretValue (tailPolynomial params.threshold coeffs)).degree < + s.card) + have hx : Function.Injective (fun i : s => params.point i) := by + intro i j hij + exact Subtype.ext (params.point_injective hij) simpa using reconstruct_sharingPolynomial_eq_secret - (x := params.point) + (x := fun i : s => params.point i) (secretValue := secretValue) (tail := tailPolynomial params.threshold coeffs) - (params.point_injective.injOn) + hx hdeg @[simp] From 8e9b27119af36613841ac20db911b3cd9bf91f8d Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 22 Apr 2026 16:07:17 -0400 Subject: [PATCH 3/4] Fix Shamir simp lint --- .../Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean b/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean index 99637f2c5..7cae5baeb 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean @@ -56,7 +56,7 @@ theorem coeff_zero_sharingPolynomial (secretValue : F) (tail : F[X]) : (sharingPolynomial secretValue tail).coeff 0 = secretValue := by simp [sharingPolynomial] -@[simp] +@[simp, nolint simpNF] theorem constantCoeff_sharingPolynomial (secretValue : F) (tail : F[X]) : (sharingPolynomial secretValue tail).constantCoeff = secretValue := by simpa [Polynomial.constantCoeff_apply] using coeff_zero_sharingPolynomial secretValue tail From 8fd090a06c4b544232de5e41b1f0fb9620223c55 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 22 Apr 2026 16:11:35 -0400 Subject: [PATCH 4/4] Fix Shamir simp normal form --- Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean b/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean index 7cae5baeb..5b7feb493 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Internal/ShamirAlgebra.lean @@ -56,7 +56,6 @@ theorem coeff_zero_sharingPolynomial (secretValue : F) (tail : F[X]) : (sharingPolynomial secretValue tail).coeff 0 = secretValue := by simp [sharingPolynomial] -@[simp, nolint simpNF] theorem constantCoeff_sharingPolynomial (secretValue : F) (tail : F[X]) : (sharingPolynomial secretValue tail).constantCoeff = secretValue := by simpa [Polynomial.constantCoeff_apply] using coeff_zero_sharingPolynomial secretValue tail