Skip to content

Commit 57e5054

Browse files
SamuelSchlesingerfmontesi
SamuelSchlesinger
and
fmontesi
authored
feat(Cryptography/SecretSharing): Shamir's secret sharing (#495)
Added a general definition of a secret sharing protocol along with privacy definitions: view indistinguishability and perfect privacy. Implemented Shamir's secret sharing as an instance, then proved view indistinguishability and perfect privacy of translation invariant tail polynomial distributions. Specialized to the uniform tail polynomial distribution as that is the typical setting. A few more PMF utilities were needed, I am planning to upstream those to Mathlib along with the existing ones from perfectly secret encryption schemes. --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>
1 parent ca0e27c commit 57e5054

9 files changed

Lines changed: 755 additions & 13 deletions

File tree

‎Cslib.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,10 @@ public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption
4242
public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.OneTimePad
4343
public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy
4444
public import Cslib.Crypto.Protocols.PerfectSecrecy.OneTimePad
45-
public import Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities
45+
public import Cslib.Crypto.Protocols.SecretSharing.Defs
46+
public import Cslib.Crypto.Protocols.SecretSharing.Scheme
47+
public import Cslib.Crypto.Protocols.SecretSharing.Shamir
48+
public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial
4649
public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
4750
public import Cslib.Foundations.Control.Monad.Free
4851
public import Cslib.Foundations.Control.Monad.Free.Effects
@@ -135,3 +138,4 @@ public import Cslib.Logics.Modal.Denotation
135138
public import Cslib.Logics.Propositional.Defs
136139
public import Cslib.Logics.Propositional.NaturalDeduction.Basic
137140
public import Cslib.MachineLearning.PACLearning.Defs
141+
public import Cslib.Probability.PMF

‎Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ Authors: Samuel Schlesinger
77
module
88

99
public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption
10-
public import Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities
10+
public import Cslib.Probability.PMF
1111
public import Mathlib.Probability.ProbabilityMassFunction.Constructions
1212

1313
/-!
@@ -58,7 +58,7 @@ the marginal distribution. -/
5858
noncomputable def posteriorMsgDist (scheme : EncScheme M K C)
5959
(msgDist : PMF M) (c : C)
6060
(hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) : PMF M :=
61-
PMFUtilities.posteriorDist msgDist scheme.ciphertextDist c hc
61+
Cslib.Probability.PMF.posteriorDist msgDist scheme.ciphertextDist c hc
6262

6363
@[simp]
6464
theorem posteriorMsgDist_apply (scheme : EncScheme M K C)

‎Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,12 +32,12 @@ variable {M K C : Type u}
3232
theorem jointDist_eq (scheme : EncScheme M K C) (msgDist : PMF M)
3333
(m : M) (c : C) :
3434
scheme.jointDist msgDist (m, c) = msgDist m * scheme.ciphertextDist m c :=
35-
PMFUtilities.bind_pair_apply msgDist scheme.ciphertextDist m c
35+
Cslib.Probability.PMF.bind_pair_apply msgDist scheme.ciphertextDist m c
3636

3737
/-- Summing the joint distribution over messages gives the marginal ciphertext distribution. -/
3838
theorem jointDist_tsum_fst (scheme : EncScheme M K C) (msgDist : PMF M) (c : C) :
3939
∑' m, scheme.jointDist msgDist (m, c) = scheme.marginalCiphertextDist msgDist c :=
40-
PMFUtilities.bind_pair_tsum_fst msgDist scheme.ciphertextDist c
40+
Cslib.Probability.PMF.bind_pair_tsum_fst msgDist scheme.ciphertextDist c
4141

4242
/-- Perfect secrecy is equivalent to message-ciphertext independence.
4343
The two formulations are related by multiplying/dividing by `marginal(c)`. -/

‎Cslib/Crypto/Protocols/SecretSharing/Defs.lean‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
/-
2+
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Samuel Schlesinger
5+
-/
6+
7+
module
8+
9+
public import Cslib.Probability.PMF
10+
public import Cslib.Crypto.Protocols.SecretSharing.Scheme
11+
12+
/-!
13+
# Secret Sharing: Definitions
14+
15+
Privacy for secret sharing is part of the `Scheme` interface. This file exposes
16+
the corresponding view and posterior distributions, plus theorem-friendly
17+
consequences of the built-in privacy field.
18+
19+
## Main definitions
20+
21+
- `Cslib.Crypto.Protocols.SecretSharing.Scheme.shareDist`:
22+
the full share distribution for one secret
23+
- `Cslib.Crypto.Protocols.SecretSharing.Scheme.viewDist`:
24+
the distribution of the restricted view for one coalition
25+
- `Cslib.Crypto.Protocols.SecretSharing.Scheme.posteriorSecretDist`:
26+
the posterior distribution on secrets after observing one view
27+
- `Cslib.Crypto.Protocols.SecretSharing.Scheme.PerfectlyPrivate`:
28+
posterior equals prior for unauthorized coalitions
29+
- `Cslib.Crypto.Protocols.SecretSharing.Scheme.perfectlyPrivate`:
30+
every scheme has posterior privacy
31+
32+
## References
33+
34+
* [Adi Shamir, *How to Share a Secret*][Shamir1979]
35+
* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020]
36+
-/
37+
38+
@[expose] public section
39+
40+
namespace Cslib.Crypto.Protocols.SecretSharing
41+
42+
namespace Scheme
43+
44+
variable {Secret Randomness Party Share : Type*}
45+
46+
/-- The distribution of the full share assignment for one secret. -/
47+
noncomputable def shareDist (scheme : Scheme Secret Randomness Party Share)
48+
(secret : Secret) : PMF (Party → Share) :=
49+
scheme.gen.map (fun r => scheme.share r secret)
50+
51+
/-- The view distribution induced on the coalition `s`. -/
52+
noncomputable def viewDist (scheme : Scheme Secret Randomness Party Share)
53+
(s : Finset Party) (secret : Secret) : PMF (s → Share) :=
54+
viewDistOf scheme.gen scheme.share s secret
55+
56+
/-- Unauthorized coalitions receive secret-independent view distributions. -/
57+
theorem viewDist_eq_of_not_authorized
58+
(scheme : Scheme Secret Randomness Party Share)
59+
{s : Finset Party} (hs : ¬ scheme.authorized s)
60+
(secret₀ secret₁ : Secret) :
61+
scheme.viewDist s secret₀ = scheme.viewDist s secret₁ := by
62+
unfold viewDist
63+
exact scheme.view_indist s hs secret₀ secret₁
64+
65+
/-- The posterior distribution on secrets after observing the coalition view
66+
`v`. -/
67+
noncomputable def posteriorSecretDist
68+
(scheme : Scheme Secret Randomness Party Share)
69+
(s : Finset Party) (secretDist : PMF Secret) (v : s → Share)
70+
(hv : v ∈ (secretDist.bind (scheme.viewDist s)).support) : PMF Secret :=
71+
Cslib.Probability.PMF.posteriorDist
72+
(p := secretDist) (f := scheme.viewDist s) v hv
73+
74+
@[simp]
75+
theorem posteriorSecretDist_apply
76+
(scheme : Scheme Secret Randomness Party Share)
77+
(s : Finset Party) (secretDist : PMF Secret) (v : s → Share)
78+
(hv : v ∈ (secretDist.bind (scheme.viewDist s)).support) (secret : Secret) :
79+
scheme.posteriorSecretDist s secretDist v hv secret =
80+
(secretDist.bind fun secret' =>
81+
(scheme.viewDist s secret').bind fun v' => PMF.pure (secret', v')) (secret, v) /
82+
(secretDist.bind (scheme.viewDist s)) v :=
83+
rfl
84+
85+
/-- Perfect privacy for unauthorized coalitions: conditioning on a view does not
86+
change the prior on secrets. -/
87+
def PerfectlyPrivate (scheme : Scheme Secret Randomness Party Share) : Prop :=
88+
∀ (s : Finset Party) (_hs : ¬ scheme.authorized s)
89+
(secretDist : PMF Secret) (v : s → Share)
90+
(hv : v ∈ (secretDist.bind (scheme.viewDist s)).support),
91+
scheme.posteriorSecretDist s secretDist v hv = secretDist
92+
93+
/-- Every scheme has posterior privacy by definition of `Scheme`. -/
94+
theorem perfectlyPrivate
95+
(scheme : Scheme Secret Randomness Party Share) :
96+
scheme.PerfectlyPrivate := by
97+
intro s hs secretDist v hv
98+
exact Cslib.Probability.PMF.posteriorDist_eq_prior_of_outputIndist
99+
(p := secretDist) (f := scheme.viewDist s)
100+
(fun secret₀ secret₁ => scheme.viewDist_eq_of_not_authorized hs secret₀ secret₁) v hv
101+
102+
end Scheme
103+
104+
end Cslib.Crypto.Protocols.SecretSharing

‎Cslib/Crypto/Protocols/SecretSharing/Scheme.lean‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
/-
2+
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Samuel Schlesinger
5+
-/
6+
7+
module
8+
9+
public import Cslib.Init
10+
public import Mathlib.Data.Finset.Basic
11+
public import Mathlib.Probability.ProbabilityMassFunction.Constructions
12+
13+
/-!
14+
# Secret Sharing Schemes
15+
16+
A secret-sharing scheme bundles the deterministic sharing/reconstruction
17+
interface, the distribution on randomness, and privacy for unauthorized
18+
coalitions.
19+
20+
## Main definitions
21+
22+
- `Cslib.Crypto.Protocols.SecretSharing.Scheme`:
23+
a secret-sharing scheme with correctness and privacy
24+
- `Cslib.Crypto.Protocols.SecretSharing.Scheme.view`:
25+
the restricted shares seen by one coalition
26+
27+
## References
28+
29+
* [Adi Shamir, *How to Share a Secret*][Shamir1979]
30+
* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020]
31+
-/
32+
33+
@[expose] public section
34+
35+
namespace Cslib.Crypto.Protocols.SecretSharing
36+
37+
/-- The view distribution induced by raw sharing data. -/
38+
noncomputable def viewDistOf {Secret Randomness Party Share : Type*}
39+
(gen : PMF Randomness) (share : Randomness → Secret → Party → Share)
40+
(s : Finset Party) (secret : Secret) : PMF (s → Share) :=
41+
PMF.map (fun r : Randomness => (fun i : s => share r secret i : s → Share)) gen
42+
43+
/--
44+
A secret-sharing scheme over secret space `Secret`, randomness space
45+
`Randomness`, party set `Party`, and share space `Share`.
46+
47+
Correctness is deterministic: every authorized coalition reconstructs the
48+
secret from the shares generated using any randomness seed. Privacy is
49+
distributional: unauthorized coalitions have the same view distribution for all
50+
secrets.
51+
-/
52+
structure Scheme (Secret Randomness Party Share : Type*) where
53+
/-- The distribution used to sample the protocol's randomness. -/
54+
gen : PMF Randomness
55+
/-- Sharing algorithm: one randomness seed determines one share per party. -/
56+
share : Randomness → Secret → Party → Share
57+
/-- Reconstruction from a coalition's observed shares. -/
58+
reconstruct (s : Finset Party) : (s → Share) → Secret
59+
/-- Authorized coalitions. -/
60+
authorized : Finset Party → Prop
61+
/-- Authorization is monotone in the coalition. -/
62+
authorized_mono :
63+
∀ {s t : Finset Party}, s ⊆ t → authorized s → authorized t
64+
/-- Authorized coalitions reconstruct the secret from the restricted view. -/
65+
correct :
66+
∀ (r : Randomness) (secret : Secret) (s : Finset Party),
67+
authorized s → reconstruct s (fun i => share r secret i) = secret
68+
/-- Unauthorized coalitions receive secret-independent view distributions. -/
69+
view_indist :
70+
∀ (s : Finset Party), ¬ authorized s → ∀ secret₀ secret₁ : Secret,
71+
viewDistOf gen share s secret₀ = viewDistOf gen share s secret₁
72+
73+
namespace Scheme
74+
75+
variable {Secret Randomness Party Share : Type*}
76+
77+
/-- The restricted shares observed by the coalition `s`. -/
78+
def view (scheme : Scheme Secret Randomness Party Share) (s : Finset Party)
79+
(r : Randomness) (secret : Secret) : s → Share :=
80+
fun i => scheme.share r secret i
81+
82+
@[simp]
83+
theorem view_apply (scheme : Scheme Secret Randomness Party Share) (s : Finset Party)
84+
(r : Randomness) (secret : Secret) (i : s) :
85+
scheme.view s r secret i = scheme.share r secret i :=
86+
rfl
87+
88+
/-- Authorized coalitions reconstruct the secret from the restricted view. -/
89+
theorem reconstruct_view_eq_secret
90+
(scheme : Scheme Secret Randomness Party Share)
91+
(r : Randomness) (secret : Secret) {s : Finset Party}
92+
(hs : scheme.authorized s) :
93+
scheme.reconstruct s (scheme.view s r secret) = secret :=
94+
scheme.correct r secret s hs
95+
96+
/-- Any sub-coalition of an unauthorized coalition is unauthorized as well. -/
97+
theorem not_authorized_of_subset
98+
(scheme : Scheme Secret Randomness Party Share)
99+
{s t : Finset Party} (hst : s ⊆ t)
100+
(ht : ¬ scheme.authorized t) :
101+
¬ scheme.authorized s := by
102+
intro hs
103+
exact ht (scheme.authorized_mono hst hs)
104+
105+
end Scheme
106+
107+
end Cslib.Crypto.Protocols.SecretSharing

0 commit comments

Comments
 (0)