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

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

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

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

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