Shamir t-out-of-n Secret Sharing: Reconstruction and Perfect Privacy

Shamir's secret-sharing scheme over the finite field ZMod p (p prime): a secret s is shared by sampling a uniformly random polynomial f of degree < t with f(0) = s, and handing party i the point f(xᵢ) at a distinct, nonzero evaluation point xᵢ. Reconstruction from any t shares is Lagrange interpolation; perfect privacy says any t-1 shares are jointly uniform and independent of s.

We model a degree-< t polynomial by its constant coefficient s (the secret) together with d := t-1 free coefficients a : Fin d → ZMod p (the coefficients of X¹, …, X^d). Sharing at a point q is then shareVal s a q = s + ∑ᵢ aᵢ · q^{i+1}, which is exactly the evaluation of the polynomial build s a = C s + ∑ᵢ C aᵢ · X^{i+1} at q (shareVal_eq_eval).

Main definitions

• shareVal / build — the field-level share and the underlying polynomial.
• PrivGame / PrivAdv — the (t-1)-share privacy game and its advantage.

Main results

• shamir_reconstruct — reconstruction: for any t = d+1 distinct evaluation points, Lagrange interpolation through the shares recovers the secret f(0) = s. General t-out-of-n.
• shamir_perfect_privacy — perfect privacy: for any t-1 nonzero evaluation points, any two secrets s₀, s₁, and any adversary A, the (t-1)-share privacy advantage is exactly 0. General t-out-of-n.

The privacy coupling avoids inverting a Vandermonde matrix: the difference of the two secrets is absorbed by translating the free-coefficient vector by the free coefficients of (s₁ - s₀) · L, where L is the degree-< t polynomial that is 1 at 0 and 0 at every revealed point (vanishPoly). Since translation is a bijection of the sampling space, advantage_zero_of_rHoare collapses the advantage to 0. This mirrors the poly_bij construction of the SSProve-Rocq proof, adapted to a coefficient-vector coupling.

References

• [Rosulek, The Joy of Cryptography, §3.13 (Shamir secret sharing)]
• [Shamir, How to Share a Secret, CACM 1979]

The scheme

def CatCrypt.Examples.ShamirSecretSharing.shareVal {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (s : ZMod p) (a : Fin d → ZMod p) (q : ZMod p) : ZMod p

The share of a degree-< d+1 polynomial with constant term s and free coefficients a (the coefficients of X¹, …, X^d), evaluated at q.

Equations

• CatCrypt.Examples.ShamirSecretSharing.shareVal s a q = s + ∑ i : Fin d, a i * q ^ (↑i + 1)

noncomputable def CatCrypt.Examples.ShamirSecretSharing.build {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (s : ZMod p) (a : Fin d → ZMod p) : Polynomial (ZMod p)

The underlying polynomial C s + ∑ᵢ C aᵢ · X^{i+1}.

Equations

• CatCrypt.Examples.ShamirSecretSharing.build s a = Polynomial.C s + ∑ i : Fin d, Polynomial.C (a i) * Polynomial.X ^ (↑i + 1)

theorem CatCrypt.Examples.ShamirSecretSharing.shareVal_eq_eval {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (s : ZMod p) (a : Fin d → ZMod p) (q : ZMod p) : Polynomial.eval q (build s a) = shareVal s a q

shareVal is the evaluation of build.

theorem CatCrypt.Examples.ShamirSecretSharing.build_natDegree_le {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (s : ZMod p) (a : Fin d → ZMod p) : (build s a).natDegree ≤ d

The polynomial has degree at most d (i.e. < t = d+1).

theorem CatCrypt.Examples.ShamirSecretSharing.shareVal_zero {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (s : ZMod p) (a : Fin d → ZMod p) : shareVal s a 0 = s

The constant term is the secret: shareVal s a 0 = s.

Reconstruction (general t-out-of-n)

theorem CatCrypt.Examples.ShamirSecretSharing.shamir_reconstruct {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (x : Fin (d + 1) → ZMod p) (hx : Function.Injective x) (s : ZMod p) (a : Fin d → ZMod p) : Polynomial.eval 0 ((Lagrange.interpolate Finset.univ x) fun (j : Fin (d + 1)) => shareVal s a (x j)) = s

Reconstruction. For any t = d+1 distinct evaluation points x, Lagrange interpolation through the shares shareVal s a (x j) recovers the secret s = f(0). This is the correctness of Shamir reconstruction from any t shares.

The vanishing polynomial for the privacy coupling

noncomputable def CatCrypt.Examples.ShamirSecretSharing.vanishPoly {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) : Polynomial (ZMod p)

L: the degree-< t polynomial equal to 1 at 0 and 0 at every revealed point rp j. Built as (∏ⱼ (0 - rp j))⁻¹ · ∏ⱼ (X - rp j).

Equations

• CatCrypt.Examples.ShamirSecretSharing.vanishPoly rp = Polynomial.C (∏ j : Fin d, (0 - rp j))⁻¹ * ∏ j : Fin d, (Polynomial.X - Polynomial.C (rp j))

theorem CatCrypt.Examples.ShamirSecretSharing.vanishPoly_eval {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (q : ZMod p) : Polynomial.eval q (vanishPoly rp) = (∏ j : Fin d, (0 - rp j))⁻¹ * ∏ j : Fin d, (q - rp j)

theorem CatCrypt.Examples.ShamirSecretSharing.prod_zero_sub_ne {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) : ∏ j : Fin d, (0 - rp j) ≠ 0

theorem CatCrypt.Examples.ShamirSecretSharing.vanishPoly_eval_zero {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) : Polynomial.eval 0 (vanishPoly rp) = 1

theorem CatCrypt.Examples.ShamirSecretSharing.vanishPoly_coeff_zero {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) : (vanishPoly rp).coeff 0 = 1

theorem CatCrypt.Examples.ShamirSecretSharing.vanishPoly_eval_pt {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (k : Fin d) : Polynomial.eval (rp k) (vanishPoly rp) = 0

theorem CatCrypt.Examples.ShamirSecretSharing.vanishPoly_natDegree_le {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) : (vanishPoly rp).natDegree ≤ d

The free-coefficient sum identity

theorem CatCrypt.Examples.ShamirSecretSharing.freeSum {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (f : Polynomial (ZMod p)) (hf : f.natDegree ≤ d) (q : ZMod p) : ∑ i : Fin d, f.coeff (↑i + 1) * q ^ (↑i + 1) = Polynomial.eval q f - f.coeff 0

For a polynomial of degree ≤ d, the "free-coefficient sum" ∑ᵢ f.coeff (i+1) · q^{i+1} equals f(q) - f.coeff 0.

The translation vector and the share-equality identity

noncomputable def CatCrypt.Examples.ShamirSecretSharing.transVec {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (s0 s1 : ZMod p) : Fin d → ZMod p

The free-coefficient translation absorbing the secret difference s₁ - s₀.

Equations

• CatCrypt.Examples.ShamirSecretSharing.transVec rp s0 s1 i = (s1 - s0) * (CatCrypt.Examples.ShamirSecretSharing.vanishPoly rp).coeff (↑i + 1)

theorem CatCrypt.Examples.ShamirSecretSharing.shareVal_translate {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) (s0 s1 : ZMod p) (a : Fin d → ZMod p) (j : Fin d) : shareVal s1 (a + transVec rp s0 s1) (rp j) = shareVal s0 a (rp j)

Share-equality under translation. Sharing s₁ with the translated free coefficients a + transVec produces the same revealed shares as sharing s₀ with a. This is the information-theoretic core of privacy.

The privacy game

noncomputable def CatCrypt.Examples.ShamirSecretSharing.PrivGame {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (s0 s1 : ZMod p) (b : Bool) : Core.SPComp (Fin d → ZMod p)

The (t-1)-share privacy game. The corrupted parties hold their shares at the d = t-1 revealed points rp of one of two secrets: PrivGame rp s₀ s₁ true shares s₀, PrivGame rp s₀ s₁ false shares s₁.

Equations

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

noncomputable def CatCrypt.Examples.ShamirSecretSharing.PrivAdv {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (s0 s1 : ZMod p) (A : (Fin d → ZMod p) → Core.SPComp Bool) : ENNReal

Privacy advantage: the corrupted parties' distinguishing probability between (t-1) shares of s₀ and of s₁.

Equations

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

theorem CatCrypt.Examples.ShamirSecretSharing.priv_coupling {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) (s0 s1 : ZMod p) : Relational.rHoare Relational.eqPre (PrivGame rp s0 s1 true) (PrivGame rp s0 s1 false) Relational.eqPost

Coupling: for any t-1 nonzero revealed points, the two privacy games are equidistributed. Translating the uniformly sampled free-coefficient vector by transVec (a bijection of the sampling space) keeps every revealed share fixed while switching the secret from s₀ to s₁.

theorem CatCrypt.Examples.ShamirSecretSharing.shamir_perfect_privacy {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) (s0 s1 : ZMod p) (A : (Fin d → ZMod p) → Core.SPComp Bool) : PrivAdv rp s0 s1 A = 0

Shamir (t-1)-share perfect privacy. For any t-1 nonzero evaluation points, any two secrets s₀, s₁, and any adversary A, the privacy advantage is exactly 0: any t-1 shares are uniform and independent of the secret.

Reflection into the Package / UC Stack

The shallow shamir_perfect_privacy bounds a single distinguisher applied to the two privacy-game bodies. This section lifts it to a composable statement about deep nominal packages linked with an arbitrary adversary package, following the stack shallow game → rawCode% → NomPackage.ofOracle → DeepNomAdvantage → sdist → UC via the shared CatCryptCore.Deep.ReflectUCHelpers combinators. The privacy game samples a free-coefficient vector then returns the revealed shares (heap-independent), so the shallow coupling priv_coupling (for nonzero revealed points hrp) upgrades to a full SPComp equality of the two reflected bodies (spcomp_eq_of_isPure_coupling), and the whole stack follows with no purity bridge on the adversary.

noncomputable def CatCrypt.Examples.ShamirSecretSharing.shamirGameRaw {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (s0 s1 : ZMod p) (b : Bool) : Deep.RawCode (Fin d → ZMod p)

The reflected (t-1)-share privacy-game body for bit b: sample a uniform free-coefficient vector a and reveal the shares at the corrupted points.

Equations

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

instance CatCrypt.Examples.ShamirSecretSharing.instValidShamirGameRaw {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (s0 s1 : ZMod p) (b : Bool) : Deep.IsValid ∅ (shamirGameRaw rp s0 s1 b)

theorem CatCrypt.Examples.ShamirSecretSharing.shamirGameRaw_eval_shallow {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (s0 s1 : ZMod p) (b : Bool) : (shamirGameRaw rp s0 s1 b).eval = PrivGame rp s0 s1 b

The reflected body evaluates back to the shallow privacy game.

theorem CatCrypt.Examples.ShamirSecretSharing.shamir_game_isPure {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (s0 s1 : ZMod p) (b : Bool) : (PrivGame rp s0 s1 b).IsPure

The privacy game is heap-independent (a uniform coefficient sample then pure share reveals).

theorem CatCrypt.Examples.ShamirSecretSharing.shamirGameRaw_eval_eq {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) (s0 s1 : ZMod p) : (shamirGameRaw rp s0 s1 true).eval = (shamirGameRaw rp s0 s1 false).eval

The two reflected bodies (shares of s0 vs. s1) have equal evaluations: for nonzero revealed points the coupling priv_coupling upgrades to SPComp equality.

noncomputable def CatCrypt.Examples.ShamirSecretSharing.shamirGameTrue {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (s0 s1 : ZMod p) : Deep.NomPackage

Real privacy game as an oracle-exporting nominal package (shares s0).

Equations

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

noncomputable def CatCrypt.Examples.ShamirSecretSharing.shamirGameFalse {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (s0 s1 : ZMod p) : Deep.NomPackage

Ideal privacy game as an oracle-exporting nominal package (shares s1).

Equations

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

theorem CatCrypt.Examples.ShamirSecretSharing.shamir_deepnom_zero {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) (s0 s1 : ZMod p) (A : Deep.NomPackage) : Crypto.DeepNomAdvantage (shamirGameTrue rp s0 s1) (shamirGameFalse rp s0 s1) A = 0

Zero deep-nominal advantage against every adversary package (nonzero points).

theorem CatCrypt.Examples.ShamirSecretSharing.shamir_sdist_zero {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) (s0 s1 : ZMod p) : (Crypto.sdist (fun (A : Deep.NomPackage) => Crypto.runPkg (A.pkg.link (shamirGameTrue rp s0 s1).pkg)) fun (A : Deep.NomPackage) => Crypto.runPkg (A.pkg.link (shamirGameFalse rp s0 s1).pkg)) = 0

Statistical distance zero between the two linked-game families.

theorem CatCrypt.Examples.ShamirSecretSharing.shamir_nompkg_secure {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) (s0 s1 : ZMod p) : Crypto.NomPkgSecure (shamirGameTrue rp s0 s1) (shamirGameFalse rp s0 s1) fun (x : Deep.NomPackage) => 0

Package-level perfect privacy (NomPkgSecure).

theorem CatCrypt.Examples.ShamirSecretSharing.shamir_uc {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (rp : Fin d → ZMod p) (hrp : ∀ (j : Fin d), rp j ≠ 0) (s0 s1 : ZMod p) : Crypto.UCEmulates 0 { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool } (fun (A : { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (shamirGameTrue rp s0 s1).pkg))) fun (A : { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (shamirGameFalse rp s0 s1).pkg))

Perfect UC emulation of the linked-game families over the trivial-leak interface (out = Bool, leak = Empty) with the identity simulator (composition plumbing).