feat(Cryptography/SecretSharing): Shamir's secret sharing

Cslib.lean

@@ -42,7 +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.PerfectSecrecy.PMFUtilities
+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
@@ -131,3 +134,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

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)

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)`. -/

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

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