From a42216be55b5defd4a90b486781511a8e2ad4754 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Thu, 23 Apr 2026 09:46:53 -0400 Subject: [PATCH 1/2] refactor(Probability): move PMF utilities --- Cslib.lean | 2 +- .../Crypto/Protocols/PerfectSecrecy/Defs.lean | 4 +- .../Internal/PerfectSecrecy.lean | 4 +- .../PMF.lean} | 59 ++++++++++++++++--- 4 files changed, 56 insertions(+), 13 deletions(-) rename Cslib/{Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean => Probability/PMF.lean} (56%) diff --git a/Cslib.lean b/Cslib.lean index 37a038ee4..89b98d35b 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -42,7 +42,6 @@ public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption 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.Foundations.Combinatorics.InfiniteGraphRamsey public import Cslib.Foundations.Control.Monad.Free public import Cslib.Foundations.Control.Monad.Free.Effects @@ -131,3 +130,4 @@ public import Cslib.Logics.LinearLogic.CLL.MLL public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic public import Cslib.Logics.Propositional.Defs public import Cslib.Logics.Propositional.NaturalDeduction.Basic +public import Cslib.Probability.PMF diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean index 03760e22d..e7d824dd6 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean @@ -7,7 +7,7 @@ Authors: Samuel Schlesinger module public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption -public import Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities +public import Cslib.Probability.PMF public import Mathlib.Probability.ProbabilityMassFunction.Constructions /-! @@ -58,7 +58,7 @@ the marginal distribution. -/ noncomputable def posteriorMsgDist (scheme : EncScheme M K C) (msgDist : PMF M) (c : C) (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) : PMF M := - PMFUtilities.posteriorDist msgDist scheme.ciphertextDist c hc + Cslib.Probability.PMF.posteriorDist msgDist scheme.ciphertextDist c hc @[simp] theorem posteriorMsgDist_apply (scheme : EncScheme M K C) diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean index 9f01fc479..66656e8ba 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean @@ -32,12 +32,12 @@ variable {M K C : Type u} theorem jointDist_eq (scheme : EncScheme M K C) (msgDist : PMF M) (m : M) (c : C) : scheme.jointDist msgDist (m, c) = msgDist m * scheme.ciphertextDist m c := - PMFUtilities.bind_pair_apply msgDist scheme.ciphertextDist m c + Cslib.Probability.PMF.bind_pair_apply msgDist scheme.ciphertextDist m c /-- Summing the joint distribution over messages gives the marginal ciphertext distribution. -/ theorem jointDist_tsum_fst (scheme : EncScheme M K C) (msgDist : PMF M) (c : C) : ∑' m, scheme.jointDist msgDist (m, c) = scheme.marginalCiphertextDist msgDist c := - PMFUtilities.bind_pair_tsum_fst msgDist scheme.ciphertextDist c + Cslib.Probability.PMF.bind_pair_tsum_fst msgDist scheme.ciphertextDist c /-- Perfect secrecy is equivalent to message-ciphertext independence. The two formulations are related by multiplying/dividing by `marginal(c)`. -/ diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean b/Cslib/Probability/PMF.lean similarity index 56% rename from Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean rename to Cslib/Probability/PMF.lean index b1ab748de..d20be22be 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean +++ b/Cslib/Probability/PMF.lean @@ -8,6 +8,7 @@ module public import Cslib.Init public import Mathlib.Probability.ProbabilityMassFunction.Monad +public import Mathlib.Probability.Distributions.Uniform /-! # PMF Utilities @@ -23,20 +24,25 @@ the Mathlib module instead. ## Main results -- `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.posterior_hasSum`: posterior probabilities sum to 1 -- `PMFUtilities.posteriorDist`: the posterior as a `PMF` +- `Cslib.Probability.PMF.bind_pair_apply`: the "pairing" bind at `(a, b)` equals `p a * f a b` +- `Cslib.Probability.PMF.bind_pair_tsum_fst`: marginalizing over the first component +- `Cslib.Probability.PMF.uniformOfFintype_map_equiv`: + a uniform distribution is invariant under equivalence +- `Cslib.Probability.PMF.posterior_hasSum`: posterior probabilities sum to 1 +- `Cslib.Probability.PMF.posteriorDist`: the posterior as a `PMF` +- `Cslib.Probability.PMF.posteriorDist_eq_prior_of_outputIndist`: + if the output distribution does not depend on the input, conditioning does + not change the prior -/ @[expose] public section -namespace Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities +namespace Cslib.Probability.PMF 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 -end Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities +/-- 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.Probability.PMF From e65b21418c50a1088f7b57cb1243e8bd80656099 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Thu, 23 Apr 2026 09:50:18 -0400 Subject: [PATCH 2/2] feat(Cryptography/SecretSharing): Shamir's secret sharing --- Cslib.lean | 4 + .../Crypto/Protocols/SecretSharing/Defs.lean | 104 ++++++ .../Protocols/SecretSharing/Scheme.lean | 107 ++++++ .../Protocols/SecretSharing/Shamir.lean | 327 ++++++++++++++++++ .../SecretSharing/Shamir/Polynomial.lean | 144 ++++++++ references.bib | 13 + 6 files changed, 699 insertions(+) create mode 100644 Cslib/Crypto/Protocols/SecretSharing/Defs.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/Shamir/Polynomial.lean diff --git a/Cslib.lean b/Cslib.lean index 89b98d35b..e178ae8cf 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -42,6 +42,10 @@ public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption 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.SecretSharing.Defs +public import Cslib.Crypto.Protocols.SecretSharing.Scheme +public import Cslib.Crypto.Protocols.SecretSharing.Shamir +public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial 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/SecretSharing/Defs.lean b/Cslib/Crypto/Protocols/SecretSharing/Defs.lean new file mode 100644 index 000000000..295b7fba6 --- /dev/null +++ b/Cslib/Crypto/Protocols/SecretSharing/Defs.lean @@ -0,0 +1,104 @@ +/- +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.Probability.PMF +public import Cslib.Crypto.Protocols.SecretSharing.Scheme + +@[expose] public section + +/-! +# Secret Sharing: Definitions + +Privacy for secret sharing is part of the `Scheme` interface. This file exposes +the corresponding view and posterior distributions, plus theorem-friendly +consequences of the built-in privacy field. + +## 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.PerfectlyPrivate`: + posterior equals prior for unauthorized coalitions +- `Cslib.Crypto.Protocols.SecretSharing.Scheme.perfectlyPrivate`: + every scheme has posterior privacy + +## 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*} + +/-- 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) := + viewDistOf scheme.gen scheme.share s secret + +/-- Unauthorized coalitions receive secret-independent view distributions. -/ +theorem viewDist_eq_of_not_authorized + (scheme : Scheme Secret Randomness Party Share) + {s : Finset Party} (hs : ¬ scheme.authorized s) + (secret₀ secret₁ : Secret) : + scheme.viewDist s secret₀ = scheme.viewDist s secret₁ := by + unfold viewDist + exact scheme.view_indist s hs secret₀ 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.Probability.PMF.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 + +/-- 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 + +/-- Every scheme has posterior privacy by definition of `Scheme`. -/ +theorem perfectlyPrivate + (scheme : Scheme Secret Randomness Party Share) : + scheme.PerfectlyPrivate := by + intro s hs secretDist v hv + exact Cslib.Probability.PMF.posteriorDist_eq_prior_of_outputIndist + (p := secretDist) (f := scheme.viewDist s) + (fun secret₀ secret₁ => scheme.viewDist_eq_of_not_authorized hs secret₀ secret₁) v hv + +end Scheme + +end Cslib.Crypto.Protocols.SecretSharing diff --git a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean new file mode 100644 index 000000000..0857e0b87 --- /dev/null +++ b/Cslib/Crypto/Protocols/SecretSharing/Scheme.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.Init +public import Mathlib.Data.Finset.Basic +public import Mathlib.Probability.ProbabilityMassFunction.Constructions + +@[expose] public section + +/-! +# Secret Sharing Schemes + +A secret-sharing scheme bundles the deterministic sharing/reconstruction +interface, the distribution on randomness, and privacy for unauthorized +coalitions. + +## Main definitions + +- `Cslib.Crypto.Protocols.SecretSharing.Scheme`: + a secret-sharing scheme with correctness and privacy +- `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 + +/-- The view distribution induced by raw sharing data. -/ +noncomputable def viewDistOf {Secret Randomness Party Share : Type*} + (gen : PMF Randomness) (share : Randomness → Secret → Party → Share) + (s : Finset Party) (secret : Secret) : PMF (s → Share) := + PMF.map (fun r : Randomness => (fun i : s => share r secret i : s → Share)) gen + +/-- +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. Privacy is +distributional: unauthorized coalitions have the same view distribution for all +secrets. +-/ +structure Scheme (Secret Randomness Party Share : Type*) 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 + /-- Unauthorized coalitions receive secret-independent view distributions. -/ + view_indist : + ∀ (s : Finset Party), ¬ authorized s → ∀ secret₀ secret₁ : Secret, + viewDistOf gen share s secret₀ = viewDistOf gen share s secret₁ + +namespace Scheme + +variable {Secret Randomness Party Share : Type*} + +/-- 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..ca4722885 --- /dev/null +++ b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean @@ -0,0 +1,327 @@ +/- +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.Scheme +public import Mathlib.Probability.Distributions.Uniform +public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial +import Cslib.Probability.PMF + +@[expose] public section + +/-! +# Shamir Secret Sharing + +This module presents a secure-by-construction API for finite-party Shamir secret +sharing through the abstract `SecretSharing.Scheme` interface. + +The 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. + +## 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 + +variable {F Party : Type*} [Field F] [Fintype 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 + +/-- The Shamir share value sent to one party. -/ +noncomputable def share (params : Params F Party) + (coeffs : Randomness params) (secretValue : F) (i : Party) : F := + (Polynomial.sharingPolynomial secretValue + (Polynomial.tailPolynomial params.threshold coeffs)).eval (params.point i) + +/-- Reconstruct the secret from one coalition's Shamir shares. -/ +noncomputable def reconstruct (params : Params F Party) + (s : Finset Party) (σ : s → F) : F := + Polynomial.reconstruct (fun i : s => params.point i) σ + +/-- 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.Probability.PMF.uniformOfFintype_map_equiv + (coeffTranslate (params := params) δ)) + +private noncomputable def privacyCorrectionPolynomial + (params : Params F Party) (s : Finset Party) + (secret₀ secret₁ : F) : _root_.Polynomial F := + by + classical + exact _root_.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 + +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 + classical + simpa using + (_root_.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 + classical + refine lt_of_lt_of_le + (_root_.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 + +private noncomputable def privacyCorrection + (params : Params F Party) (s : Finset Party) + (hcard : s.card ≤ params.threshold) + (secret₀ secret₁ : F) : Randomness params := + _root_.Polynomial.degreeLTEquiv F params.threshold + ⟨privacyCorrectionPolynomial (F := F) params s secret₀ secret₁, + _root_.Polynomial.mem_degreeLT.2 + (privacyCorrectionPolynomial_degree_lt (F := F) params s secret₀ secret₁ hcard)⟩ + +private theorem tailPolynomial_privacyCorrection + (params : Params F Party) (s : Finset Party) + (hcard : s.card ≤ params.threshold) + (secret₀ secret₁ : F) : + Polynomial.tailPolynomial (F := F) params.threshold + (privacyCorrection (F := F) params s hcard secret₀ secret₁) = + privacyCorrectionPolynomial (F := F) params s secret₀ secret₁ := by + simp [privacyCorrection, Polynomial.tailPolynomial] + +private theorem view_eq_view_add_privacyCorrection + (params : Params F Party) (s : Finset Party) + (hcard : s.card ≤ params.threshold) + (secret₀ secret₁ : F) (coeffs : Randomness params) : + (fun i : s => share params coeffs secret₀ i) = + (fun i : s => + share params + (coeffs + privacyCorrection (F := F) params s hcard secret₀ secret₁) + secret₁ i) := by + ext i + unfold share + rw [Polynomial.sharingPolynomial_eval, Polynomial.sharingPolynomial_eval] + rw [Polynomial.tailPolynomial_add, _root_.Polynomial.eval_add, tailPolynomial_privacyCorrection] + rw [privacyCorrectionPolynomial_eval (F := F) params s secret₀ secret₁ i] + field_simp [params.point_nonzero i] + ring + +/-- Translation-invariant Shamir tail samplers induce secret-independent views +for unauthorized coalitions. -/ +theorem view_indist_of_tailSampler (params : Params F Party) + (sampler : TailSampler params) : + ∀ (s : Finset Party), ¬ authorized params s → ∀ secret₀ secret₁ : F, + viewDistOf sampler.gen (share params) s secret₀ = + viewDistOf sampler.gen (share params) s secret₁ := by + intro s hs secret₀ secret₁ + have hcard : s.card ≤ params.threshold := by + have hs' : ¬ params.threshold + 1 ≤ s.card := by + simpa [authorized] using hs + exact Nat.lt_succ_iff.mp (Nat.not_le.mp hs') + unfold viewDistOf + calc + PMF.map (fun coeffs : Randomness params => + (fun i : s => share params coeffs secret₀ i : s → F)) sampler.gen = + PMF.map + (fun coeffs : Randomness params => (fun i : s => + share params + (coeffs + privacyCorrection (F := F) params s hcard secret₀ secret₁) + secret₁ i : s → F)) sampler.gen := by + congr 1 + funext coeffs + exact view_eq_view_add_privacyCorrection + (F := F) params s hcard secret₀ secret₁ coeffs + _ = PMF.map (fun coeffs : Randomness params => + (fun i : s => share params coeffs secret₁ i : s → F)) + (PMF.map + (fun coeffs => coeffs + privacyCorrection (F := F) params s hcard secret₀ secret₁) + sampler.gen) := by + rw [PMF.map_comp] + rfl + _ = PMF.map (fun coeffs : Randomness params => + (fun i : s => share params coeffs secret₁ i : s → F)) sampler.gen := by + rw [sampler.map_add_eq_self] + +/-- 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 := + { gen := sampler.gen + share := share params + reconstruct := reconstruct params + authorized := authorized params + authorized_mono := by + intro s u hsu hs + exact le_trans hs (Finset.card_le_card hsu) + correct := by + intro coeffs secretValue s hs + have hdeg₀ : + (Polynomial.sharingPolynomial secretValue + (Polynomial.tailPolynomial params.threshold coeffs)).degree < + (params.threshold + 1 : WithBot ℕ) := + Polynomial.degree_sharingPolynomial_tailPolynomial_lt_succ + secretValue params.threshold coeffs + have hdeg : + (Polynomial.sharingPolynomial secretValue + (Polynomial.tailPolynomial params.threshold coeffs)).degree < + Fintype.card s := by + simpa using + (lt_of_lt_of_le hdeg₀ (by exact_mod_cast hs) : + (Polynomial.sharingPolynomial secretValue + (Polynomial.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 [share, reconstruct] using + Polynomial.reconstruct_sharingPolynomial_eq_secret + (x := fun i : s => params.point i) + (secretValue := secretValue) + (tail := Polynomial.tailPolynomial params.threshold coeffs) + hx + hdeg + view_indist := view_indist_of_tailSampler params sampler } + +/-- 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 (params : Params F Party) + (sampler : TailSampler params) (coeffs : Randomness params) + (secretValue : F) (i : Party) : + (schemeWith params sampler).share coeffs secretValue i = + share params coeffs secretValue 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/Shamir/Polynomial.lean b/Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean new file mode 100644 index 000000000..6dacc9167 --- /dev/null +++ b/Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean @@ -0,0 +1,144 @@ +/- +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: Polynomial Utilities + +This file contains the Shamir-specific polynomial and interpolation utilities +used to prove correctness and privacy of the public scheme construction. +-/ + +noncomputable section + +namespace Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial + +variable {F : Type*} [Field F] + +/-- The tail polynomial determined by the first `n` coefficients. -/ +def tailPolynomial (n : ℕ) (coeffs : Fin n → F) : _root_.Polynomial F := + ↑((_root_.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 (_root_.Polynomial.degreeLTEquiv F n) coeffs) i + simpa [tailPolynomial, _root_.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 := + _root_.Polynomial.mem_degreeLT.1 + (((_root_.Polynomial.degreeLTEquiv F n).symm coeffs : + _root_.Polynomial.degreeLT F n)).2 + +/-- `tailPolynomial` is additive in its coefficient vector. -/ +theorem tailPolynomial_add (n : ℕ) (a b : Fin n → F) : + tailPolynomial (F := F) n (a + b) = tailPolynomial n a + tailPolynomial n b := by + simp [tailPolynomial] + +/-- The standard Shamir sharing polynomial `s + X * q(X)`. -/ +def sharingPolynomial (secretValue : F) (tail : _root_.Polynomial F) : _root_.Polynomial F := + _root_.Polynomial.C secretValue + _root_.Polynomial.X * tail + +@[simp] +theorem sharingPolynomial_eval (secretValue x : F) (tail : _root_.Polynomial F) : + (sharingPolynomial secretValue tail).eval x = secretValue + x * tail.eval x := by + simp [sharingPolynomial, mul_comm] + +theorem coeff_zero_sharingPolynomial (secretValue : F) (tail : _root_.Polynomial F) : + (sharingPolynomial secretValue tail).coeff 0 = secretValue := by + simp [sharingPolynomial] + +theorem constantCoeff_sharingPolynomial (secretValue : F) (tail : _root_.Polynomial F) : + (sharingPolynomial secretValue tail).constantCoeff = secretValue := by + simpa [_root_.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 : _root_.Polynomial F) {n : ℕ} + (hdeg : tail.degree < n) : + (sharingPolynomial secretValue tail).natDegree ≤ n := by + rw [sharingPolynomial] + refine (_root_.Polynomial.natDegree_add_le _ _).trans ?_ + rw [max_le_iff] + constructor + · rw [_root_.Polynomial.natDegree_C] + exact Nat.zero_le n + · by_cases htail : tail = 0 + · simp [htail] + · rw [_root_.Polynomial.natDegree_X_mul htail] + have htailDegree : tail.natDegree < n := by + have := hdeg + rw [_root_.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 : _root_.Polynomial F) {n : ℕ} + (hdeg : tail.degree < n) : + (sharingPolynomial secretValue tail).degree < (n + 1 : WithBot ℕ) := by + by_cases hsharing : sharingPolynomial secretValue tail = 0 + · simp [hsharing] + · rw [_root_.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 + (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*} [Fintype ι] + +/-- Reconstruct the secret from finitely indexed share values by interpolating +the unique low-degree polynomial that matches them. -/ +def reconstruct (x σ : ι → F) : F := + by + classical + exact (_root_.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 : _root_.Polynomial F} + (hx : Function.Injective x) + (hdeg : p.degree < Fintype.card ι) : + reconstruct x (fun i => p.eval (x i)) = p.constantCoeff := by + classical + have hp : + p = _root_.Lagrange.interpolate Finset.univ x (fun i => p.eval (x i)) := + _root_.Lagrange.eq_interpolate + (s := Finset.univ) + (v := x) + hx.injOn + (by simpa using hdeg) + simpa [reconstruct] using congrArg _root_.Polynomial.constantCoeff hp.symm + +/-- Reconstruction succeeds on the values of a Shamir sharing polynomial once +the finite index type is large enough. -/ +theorem reconstruct_sharingPolynomial_eq_secret + {x : ι → F} {secretValue : F} {tail : _root_.Polynomial F} + (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.Polynomial 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},