Shamir Secret Sharing

This module presents a secure-by-construction API for finite-party Shamir secret sharing through the abstract SecretSharing.Scheme interface.

The public constructors require two pieces of data:

• public parameters consisting of a threshold together with distinct, nonzero evaluation points for a finite party set
• a translation-invariant sampler on the tail coefficients

Translation invariance is exactly the symmetry used in the privacy proof. The canonical finite-field instance is obtained by taking the sampler to be uniform.

Main definitions

• Cslib.Crypto.Protocols.SecretSharing.Shamir.Params: the threshold and public evaluation points
• Cslib.Crypto.Protocols.SecretSharing.Shamir.Randomness: the vector of tail coefficients
• Cslib.Crypto.Protocols.SecretSharing.Shamir.TailSampler: a translation-invariant distribution on tail coefficients
• Cslib.Crypto.Protocols.SecretSharing.Shamir.schemeWith: Shamir's scheme with a privacy-preserving tail sampler
• Cslib.Crypto.Protocols.SecretSharing.Shamir.scheme: the corresponding finite-field scheme with uniform randomness

Main results

• Cslib.Crypto.Protocols.SecretSharing.Shamir.reconstruct_view_eq_secret: any authorized coalition reconstructs the secret
• Cslib.Crypto.Protocols.SecretSharing.Shamir.authorized_univ: the full party set is always authorized

Notes

The public share type is just the field F: the evaluation points are fixed in Params, so one share consists only of the corresponding field value.

References

• Adi Shamir, How to Share a Secret
• J. Katz, Y. Lindell, Introduction to Modern Cryptography

structure Cslib.Crypto.Protocols.SecretSharing.Shamir.Params (F : Type u_3) [Zero F] (Party : Type u_4) [Fintype Party] : Type (max u_3 u_4)

Public parameters for a finite Shamir secret-sharing instance. The threshold is bundled with the evaluation points so the API can enforce the standard non-vacuous threshold < number of parties side condition.

• threshold : ℕ

  A coalition of size threshold + 1 is the first authorized size.

• threshold_lt_card : self.threshold < Fintype.card Party

  Standard Shamir sharing requires threshold < number of parties.

• point : Party → F

  The public evaluation point assigned to each party.

• point_injective : Function.Injective self.point

  Distinct parties receive distinct evaluation points.

• point_nonzero (i : Party) : self.point i ≠ 0

  Standard Shamir sharing forbids the point 0, which would reveal the secret directly.

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.SecretSharing.Shamir.Randomness {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) : Type u_1

The random coefficients of the degree-threshold - 1 tail polynomial.

Equations

• Cslib.Crypto.Protocols.SecretSharing.Shamir.Randomness params = (Fin params.threshold → F)

def Cslib.Crypto.Protocols.SecretSharing.Shamir.authorized {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) (s : Finset Party) : Prop

A coalition is authorized exactly when it contains at least params.threshold + 1 parties.

Equations

• Cslib.Crypto.Protocols.SecretSharing.Shamir.authorized params s = (params.threshold + 1 ≤ s.card)

theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.authorized_univ {F : Type u_3} {Party : Type u_4} [Field F] [Fintype Party] (params : Params F Party) : authorized params Finset.univ

Because params.threshold < |Party|, the full party set can always reconstruct the secret.

noncomputable def Cslib.Crypto.Protocols.SecretSharing.Shamir.share {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) (coeffs : Randomness params) (secretValue : F) (i : Party) : F

The Shamir share value sent to one party.

Equations

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

noncomputable def Cslib.Crypto.Protocols.SecretSharing.Shamir.reconstruct {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) (s : Finset Party) (σ : ↥s → F) : F

Reconstruct the secret from one coalition's Shamir shares.

Equations

• Cslib.Crypto.Protocols.SecretSharing.Shamir.reconstruct params s σ = Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.reconstruct (fun (i : ↥s) => params.point ↑i) σ

structure Cslib.Crypto.Protocols.SecretSharing.Shamir.TailSampler {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) : Type u_1

A sampler on Shamir tail coefficients is privacy-compatible when its distribution is invariant under translation by any coefficient vector. This is the exact symmetry needed in the privacy proof.

• gen : PMF (Randomness params)

  The underlying coefficient distribution.

• map_add_eq_self (δ : Randomness params) : PMF.map (fun (coeffs : Randomness params) => coeffs + δ) self.gen = self.gen

  Translating the coefficients does not change the distribution.

noncomputable def Cslib.Crypto.Protocols.SecretSharing.Shamir.uniformTailSampler {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) [Fintype F] [Nonempty F] : TailSampler params

Uniform tail coefficients form the canonical privacy-compatible sampler.

Equations

• Cslib.Crypto.Protocols.SecretSharing.Shamir.uniformTailSampler params = { gen := PMF.uniformOfFintype (Cslib.Crypto.Protocols.SecretSharing.Shamir.Randomness params), map_add_eq_self := ⋯ }

theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.view_indist_of_tailSampler {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) (sampler : TailSampler params) (s : Finset Party) : ¬authorized params s → ∀ (secret₀ secret₁ : F), viewDistOf sampler.gen (share params) s secret₀ = viewDistOf sampler.gen (share params) s secret₁

Translation-invariant Shamir tail samplers induce secret-independent views for unauthorized coalitions.

noncomputable def Cslib.Crypto.Protocols.SecretSharing.Shamir.schemeWith {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) (sampler : TailSampler params) : Scheme F (Randomness params) Party F

Shamir's scheme built from a privacy-compatible tail sampler.

Equations

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

noncomputable def Cslib.Crypto.Protocols.SecretSharing.Shamir.scheme {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) [Fintype F] [Nonempty F] : Scheme F (Randomness params) Party F

The canonical finite-field Shamir scheme with uniformly sampled tail coefficients.

Equations

• Cslib.Crypto.Protocols.SecretSharing.Shamir.scheme params = Cslib.Crypto.Protocols.SecretSharing.Shamir.schemeWith params (Cslib.Crypto.Protocols.SecretSharing.Shamir.uniformTailSampler params)

@[simp]

theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.schemeWith_authorized_iff {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) (sampler : TailSampler params) (s : Finset Party) : (schemeWith params sampler).authorized s ↔ params.threshold + 1 ≤ s.card

@[simp]

theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.scheme_authorized_iff {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) [Fintype F] [Nonempty F] (s : Finset Party) : (scheme params).authorized s ↔ params.threshold + 1 ≤ s.card

@[simp]

theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.schemeWith_share_eq {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) (sampler : TailSampler params) (coeffs : Randomness params) (secretValue : F) (i : Party) : (schemeWith params sampler).share coeffs secretValue i = share params coeffs secretValue i

theorem Cslib.Crypto.Protocols.SecretSharing.Shamir.reconstruct_view_eq_secret {F : Type u_1} {Party : Type u_2} [Field F] [Fintype Party] (params : Params F Party) (sampler : TailSampler params) (coeffs : Randomness params) (secretValue : F) {s : Finset Party} (hs : (schemeWith params sampler).authorized s) : (schemeWith params sampler).reconstruct s ((schemeWith params sampler).view s coeffs secretValue) = secretValue

Any authorized coalition reconstructs the secret from the shares it sees.