2. Secret Sharing Scheme🔗

We now define a general secret sharing scheme over a set of n participants \mathcal{P} = \{P_1, \dots, P_n\}. Let \mathcal{S} denote the domain of possible secrets, where |\mathcal{S}| \ge 2. Each participant P_i receives a share from a finite set \mathcal{V}_i.

The scheme is randomized, utilizing a finite set of random strings \mathcal{R} equipped with a probability distribution \mu. Unless otherwise stated, we assume \mu is the uniform distribution over \mathcal{R}.

We assume that the variable Secret has type u, while the random element Random has type v.

import Mathlib.Tactic
import Mathlib.Data.Fintype.Basic
import Mathlib.Probability.ProbabilityMassFunction.Basic
import Mathlib.Probability.Distributions.Uniform

The data structure for secret sharing scheme.

We define the API Secret Sharing Scheme in the namespace SecretSharingScheme.

For every unauthorized set B ∉ Γ, the shares held by B reveal no information about the secret.

Fix an unauthorized set B. For each secret s, (sharesofset S s r B) with r random gives a distribution on |B|-tuple of shares. Perfect security requires that this distribution is the same for all secret s. The equation in the condition becomes

\Pr(\Pi_T(s_1,r) = \langle s_j\rangle_{j\in T}) = \Pr(\Pi_T(s_2,r) = \langle s_j\rangle_{j\in T} )

To verify perfect security, we only need to verify the condition for maximally unauthorized set.