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

noncomputable def Cslib.Crypto.Protocols.SecretSharing.Scheme.shareDist {Secret : Type u_1} {Randomness : Type u_2} {Party : Type u_3} {Share : Type u_4} (scheme : Scheme Secret Randomness Party Share) (secret : Secret) : PMF (Party → Share)

The distribution of the full share assignment for one secret.

Equations

• scheme.shareDist secret = PMF.map (fun (r : Randomness) => scheme.share r secret) scheme.gen

noncomputable def Cslib.Crypto.Protocols.SecretSharing.Scheme.viewDist {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) (secret : Secret) : PMF (↥s → Share)

The view distribution induced on the coalition s.

Equations

• scheme.viewDist s secret = Cslib.Crypto.Protocols.SecretSharing.viewDistOf scheme.gen scheme.share s secret

theorem Cslib.Crypto.Protocols.SecretSharing.Scheme.viewDist_eq_of_not_authorized {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} (hs : ¬scheme.authorized s) (secret₀ secret₁ : Secret) : scheme.viewDist s secret₀ = scheme.viewDist s secret₁

Unauthorized coalitions receive secret-independent view distributions.

noncomputable def Cslib.Crypto.Protocols.SecretSharing.Scheme.posteriorSecretDist {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) (secretDist : PMF Secret) (v : ↥s → Share) (hv : v ∈ (secretDist.bind (scheme.viewDist s)).support) : PMF Secret

The posterior distribution on secrets after observing the coalition view v.

Equations

• scheme.posteriorSecretDist s secretDist v hv = Cslib.Probability.PMF.posteriorDist secretDist (scheme.viewDist s) v hv

@[simp]

theorem Cslib.Crypto.Protocols.SecretSharing.Scheme.posteriorSecretDist_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) (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' : Secret) => (scheme.viewDist s secret').bind fun (v' : ↥s → Share) => PMF.pure (secret', v')) (secret, v) / (secretDist.bind (scheme.viewDist s)) v

def Cslib.Crypto.Protocols.SecretSharing.Scheme.PerfectlyPrivate {Secret : Type u_1} {Randomness : Type u_2} {Party : Type u_3} {Share : Type u_4} (scheme : Scheme Secret Randomness Party Share) : Prop

Perfect privacy for unauthorized coalitions: conditioning on a view does not change the prior on secrets.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Crypto.Protocols.SecretSharing.Scheme.perfectlyPrivate {Secret : Type u_1} {Randomness : Type u_2} {Party : Type u_3} {Share : Type u_4} (scheme : Scheme Secret Randomness Party Share) : scheme.PerfectlyPrivate

Every scheme has posterior privacy by definition of Scheme.