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
• J. Katz, Y. Lindell, Introduction to Modern Cryptography

noncomputable def Cslib.Crypto.Protocols.SecretSharing.viewDistOf {Secret : Type u_1} {Randomness : Type u_2} {Party : Type u_3} {Share : Type u_4} (gen : PMF Randomness) (share : Randomness → Secret → Party → Share) (s : Finset Party) (secret : Secret) : PMF (↥s → Share)

The view distribution induced by raw sharing data.

Equations

• Cslib.Crypto.Protocols.SecretSharing.viewDistOf gen share s secret = PMF.map (fun (r : Randomness) (i : ↥s) => share r secret ↑i) gen

structure Cslib.Crypto.Protocols.SecretSharing.Scheme (Secret : Type u_1) (Randomness : Type u_2) (Party : Type u_3) (Share : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

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.

• gen : PMF Randomness

  The distribution used to sample the protocol's randomness.

• share : Randomness → Secret → Party → Share

  Sharing algorithm: one randomness seed determines one share per party.

• reconstruct (s : Finset Party) : (↥s → Share) → Secret

  Reconstruction from a coalition's observed shares.

• authorized : Finset Party → Prop

  Authorized coalitions.

• authorized_mono {s t : Finset Party} : s ⊆ t → self.authorized s → self.authorized t

  Authorization is monotone in the coalition.

• correct (r : Randomness) (secret : Secret) (s : Finset Party) : self.authorized s → (self.reconstruct s fun (i : ↥s) => self.share r secret ↑i) = secret

  Authorized coalitions reconstruct the secret from the restricted view.

• view_indist (s : Finset Party) : ¬self.authorized s → ∀ (secret₀ secret₁ : Secret), viewDistOf self.gen self.share s secret₀ = viewDistOf self.gen self.share s secret₁

  Unauthorized coalitions receive secret-independent view distributions.

def Cslib.Crypto.Protocols.SecretSharing.Scheme.view {Secret : Type u_1} {Randomness : Type u_2} {Party : Type u_3} {Share : Type u_4} (scheme : Scheme Secret Randomness Party Share) (s : Finset Party) (r : Randomness) (secret : Secret) : ↥s → Share

The restricted shares observed by the coalition s.

Equations

• scheme.view s r secret i = scheme.share r secret ↑i

@[simp]

theorem Cslib.Crypto.Protocols.SecretSharing.Scheme.view_apply {Secret : Type u_1} {Randomness : Type u_2} {Party : Type u_3} {Share : Type u_4} (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

theorem Cslib.Crypto.Protocols.SecretSharing.Scheme.reconstruct_view_eq_secret {Secret : Type u_1} {Randomness : Type u_2} {Party : Type u_3} {Share : Type u_4} (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

Authorized coalitions reconstruct the secret from the restricted view.

theorem Cslib.Crypto.Protocols.SecretSharing.Scheme.not_authorized_of_subset {Secret : Type u_1} {Randomness : Type u_2} {Party : Type u_3} {Share : Type u_4} (scheme : Scheme Secret Randomness Party Share) {s t : Finset Party} (hst : s ⊆ t) (ht : ¬scheme.authorized t) : ¬scheme.authorized s

Any sub-coalition of an unauthorized coalition is unauthorized as well.