3. Shamir Scheme🔗

We describe the concrete instantiation of a threshold secret sharing scheme introduced by Shamir in 1979. We will prove at the end of this section that it is an instance of threshold access structure

shamirRealizedScheme

In particular, the Shamir scheme realizes the threshold access structure \Gamma_{t,n} = \{A \subseteq \mathcal{P} : |A| \ge t\} over a finite field \mathbb{F} with cardinality |\mathbb{F}| > n.

Construction. Let s \in \mathbb{F} be the secret to be shared among n participants. The dealer associates each participant P_i with a distinct non-zero field element x_i \in \mathbb{F} \setminus \{0\}.

Polynomial Encoding. Fix a threshold t. The dealer chooses t-1 coefficients a_1, \dots, a_{t-1} uniformly at random from \mathbb{F} and constructs the polynomial f(x) \in \mathbb{F}[x] of degree at most t-1:

f(x) = s + \sum_{j=1}^{t-1} a_j x^j.

Here, the constant term is the secret, i.e., f(0) = s. The share for participant P_i is the evaluation of the polynomial at their assigned point:

y_i = f(x_i).

The dealer distributes the share (x_i, y_i) to participant P_i.

Reconstruction via Interpolation. Reconstruction is guaranteed by the property that a polynomial of degree t-1 is uniquely determined by its values at t distinct points. For any authorized set of participants B with |B| \ge t, the secret s = f(0) can be recovered using Lagrange interpolation.

Let L_j(x) be the Lagrange basis polynomials associated with the set B:

L_j(x) = \prod_{\substack{k \in B \\ k \neq j}} \frac{x - x_k}{x_j - x_k}.

The polynomial f(x) can be expressed as

f(x) = \sum_{j \in B} y_j L_j(x).

To recover the secret, the participants simply evaluate the interpolation formula at x=0:

s = f(0) = \sum_{j \in B} y_j \Big( \prod_{\substack{k \in B \\ k \neq j}} \frac{0 - x_k}{x_j - x_k} \Big).

-- Import the library of Lagrange interpolation
-- from Linear Algebra
import Mathlib.LinearAlgebra.Lagrange

-- import AccessStructure and SecretSharing Scheme
import SecretSharingScheme.Section_1_Access_Structure
import SecretSharingScheme.Section_2_Secret_Sharing_Scheme

We put the Lean program for Shamir scheme inside a noncomputable section.

In addition to the definitions from AccessStructure and SecretSharingScheme, we also need the APIs from BigOperators, Finset, Matrix, Polynomial.

The variable F denotes a field.

The polynomial used in Shamir secret scheme is called shamir_poly t F. It is a polynomial in polynomial t over a finite field F.

A helper lemma showing that the size of a finite field is at least 2.

Define the Shamir secret sharing shceme.

Reconstruction in Shamir scheme.

Shamir polynomial as a linear map on the i-th coefficient.

The function shamir_linear_map n t x B maps an index i to an element in the field F.

The Shamir linear map is a surjective function.