Secret Sharing and Secure Distributed Matrix Multiplication

5.Β Distributed HierarchyπŸ”—

We define Linear Secret Sharing Schemes (LSSS) and use it perform Secure Distributed Matrix Multiplication (SDMM). This application is a canonical example of secure multiparty computation (MPC) with a linear functionality.

Consider a distributed computing system consisting of a master node and n worker nodes \mathcal{P} = \{P_1, \dots, P_n\}. The master holds a private matrix A \in \mathbb{F}^{m \times d} and a public vector x \in \mathbb{F}^d. The goal is to compute the matrix-vector product y = Ax \in \mathbb{F}^m distributedly, such that no unauthorized subset of workers can learn any information about the matrix A.

section DistributedHierarchy open AccessStructure SecretSharingScheme /-- ### Abstract Distributed Matrix Multiplication Protocol This structure defines the interface and correctness condition for any distributed matrix multiplication scheme, independent of how it is implemented. -/ structure DistributedMatrixMultiplication (n : β„•) (Ξ“ : AccessStructure n) (F : Type*) [Field F] where -- Types Secret : Type* Share : Fin n β†’ Type* Random : Type* -- We need Randomness for LSSS compatibility -- Protocol Functions encode : Secret β†’ Random β†’ (i : Fin n) β†’ Share i worker_compute : {d : β„•} β†’ (i : Fin n) β†’ (Fin d β†’ Share i) β†’ (Fin d β†’ F) β†’ Share i reconstruct : (B : Set (Fin n)) β†’ (hB : B ∈ Ξ“.auth) β†’ ((i : B) β†’ Share i) β†’ Secret -- Algebraic Structure needed [secret_add : AddCommMonoid Secret] [secret_module : Module F Secret] -- correctness h_distributed_correctness : βˆ€ {d : β„•} (A : Fin d β†’ Secret) (K : Fin d β†’ Random) (x : Fin d β†’ F) (B : Set (Fin n)) (hB : B ∈ Ξ“.auth), let shares (j : Fin d) (i : Fin n) := encode (A j) (K j) i let responses (i : B) := worker_compute i (fun j => shares j i) x reconstruct B hB responses = βˆ‘ j, x j β€’ A j

While the general definition of secret sharing allows for arbitrary reconstruction functions, efficient secure computation protocols typically rely on schemes with algebraic structure. The standard class of such schemes is the Linear Secret Sharing Scheme (LSSS), as introduced in the book Secure Multiparty Computation and Secret Sharing by Cramer et al. in 2015.

Let \mathbb{F} be a finite field. A secret sharing scheme over a set of participants \mathcal{P} = \{P_1, \dots, P_n\} is called linear over \mathbb{F} if:

  1. The shares for each participant form a vector space over \mathbb{F}.

  2. The distribution function (dealer) is a linear map.

  3. The reconstruction function for any authorized set is a linear map.

Formally, an LSSS is defined by a share-generating matrix M \in \mathbb{F}^{n \times d} and a function

\psi: \{1, \dots, n\} \to \mathcal{P}

mapping rows of M to participants. To share a secret s \in \mathbb{F}, the dealer chooses a random vector

\mathbf{r} = (r_1, \dots, r_{d-1})^\top \in \mathbb{F}^{d-1}

and computes the share vector \mathbf{v} \in \mathbb{F}^n as:

\mathbf{v} = M \cdot (s, r_1, \dots, r_{d-1})^\top.

The share for participant P_i consists of the component(s) of \mathbf{v} corresponding to the rows assigned to P_i by \psi.

The structure LinearSecretSharingScheme is defined as an extension of RealizedSecretSharingScheme, and hence it inherit all the attributes of a secret sharing scheme. We add the hypothesis of the linearity of the encoding and decoding.

/-! ### The Linear Secret Sharing Scheme (LSSS) -/ structure LinearSecretSharingScheme (n : β„•) (Ξ“ : AccessStructure n) (F : Type*) [Field F] extends RealizedSecretSharingScheme n Ξ“ where -- Algebraic Structures [secret_add : AddCommMonoid Secret] [random_add : AddCommMonoid Random] [share_add : βˆ€ i, AddCommMonoid (Share i)] [secret_module : Module F Secret] [random_module : Module F Random] [share_module : βˆ€ i, Module F (Share i)] -- Linearity of Dealer dealer_linear : (Secret Γ— Random) β†’β‚—[F] (Ξ  i, Share i) h_dealer_eq : βˆ€ s r, dealer_linear (s, r) = dealer s r -- Linearity of Reconstruction recon_linear : βˆ€ (B : Set (Fin n)) (_hB : B ∈ Ξ“.auth), ((i : B) β†’ Share i) β†’β‚—[F] Secret h_recon_eq : βˆ€ (B : Set (Fin n)) (hB : B ∈ Ξ“.auth) (shares : (i : B) β†’ Share i), recon_linear B hB shares = recon B hB shares namespace LinearSecretSharingScheme -- Register instances attribute [instance] secret_add random_add share_add attribute [instance] secret_module random_module share_module variable {n : β„•} {Ξ“ : AccessStructure n} variable {F : Type*} [Field F] variable (L : LinearSecretSharingScheme n Ξ“ F) -- Definition of the Worker's Computation def worker_compute_impl {d : β„•} (i : Fin n) (shares : Fin d β†’ L.Share i) (x : Fin d β†’ F) : L.Share i := βˆ‘ j, x j β€’ shares j -- Definition of Target and Keys (Helpers for the proof) def target_computation {d : β„•} (A : Fin d β†’ L.Secret) (x : Fin d β†’ F) : L.Secret := βˆ‘ j, x j β€’ A j def aggregate_key {d : β„•} (K : Fin d β†’ L.Random) (x : Fin d β†’ F) : L.Random := βˆ‘ j, x j β€’ K j

The master node utilizes an LSSS realizing an access structure \Gamma over a set of participants \mathcal{P}.

The protocol proceeds in three phases:

1. Encoding Phase (Share Generation) The master treats the matrix A as a collection of d column vectors A^{(1)}, \dots, A^{(d)}, where each A^{(j)} is in \mathbb{F}^m.

To protect the matrix, the master applies the LSSS independently to each column. For each j \in \{1, \dots, d\}:

  1. Generate a random key vector \rho^{(j)} \in \mathcal{K} (where \mathcal{K} is the randomness space of the LSSS).

  2. Compute the shares for the j-th column vector

\mathbf{c}^{(j)} = \text{Share}(A^{(j)}, \rho^{(j)}) \in (\mathbb{F}^m)^n.

Here, \mathbf{c}^{(j)} = (c_1^{(j)}, \dots, c_n^{(j)})^\top, where c_i^{(j)} is the share given to worker P_i.

After processing all d columns, the master constructs an encoded matrix C \in (\mathbb{F}^m)^{n \times d}, where the i-th row corresponds to the collection of shares held by worker P_i for all columns of A.

2. Computation Phase The master distributes the i-th row of C, denoted C_i \in (\mathbb{F}^m)^{1 \times d}, and the public vector $x$ to worker $Pi$. Each worker $Pi$ computes the local dot product

z_i = C_i \cdot x = \sum_{j=1}^d x_j c_i^{(j)} \in \mathbb{F}^m.

The worker returns the result z_i to the master. Since each c_i^{(j)} is a valid share of a secret column A^{(j)}, the worker learns nothing about the matrix A beyond what is revealed by its own shares (which is zero for unauthorized sets).

3. Reconstruction Phase The master collects the results \{z_i\}_{P_i \in B} from any authorized subset of workers B \in \Gamma. The correctness of the protocol relies on the linearity of the reconstruction function.

The security of the protocol follows directly from the perfect secrecy of the underlying LSSS. Since each column is shared independently with fresh randomness, the view of any unauthorized coalition T \notin \Gamma is statistically independent of A.

We need two helper lemmas used in the main proof of correctness.

lemma sum_prod_smul {n : β„•} {Ξ“ : AccessStructure n} {F : Type*} [Field F] (L : LinearSecretSharingScheme n Ξ“ F) {d : β„•} (x : Fin d β†’ F) (A : Fin d β†’ L.Secret) (K : Fin d β†’ L.Random) : βˆ‘ j, x j β€’ (A j, K j) = (βˆ‘ j, x j β€’ A j, βˆ‘ j, x j β€’ K j) := n:β„•Ξ“:AccessStructure nF:Type u_2inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•x:Fin d β†’ FA:Fin d β†’ L.SecretK:Fin d β†’ L.Random⊒ βˆ‘ j, x j β€’ (A j, K j) = (βˆ‘ j, x j β€’ A j, βˆ‘ j, x j β€’ K j) n:β„•Ξ“:AccessStructure nF:Type u_2inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•x:Fin d β†’ FA:Fin d β†’ L.SecretK:Fin d β†’ L.Random⊒ (βˆ‘ j, x j β€’ (A j, K j)).1 = (βˆ‘ j, x j β€’ A j, βˆ‘ j, x j β€’ K j).1n:β„•Ξ“:AccessStructure nF:Type u_2inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•x:Fin d β†’ FA:Fin d β†’ L.SecretK:Fin d β†’ L.Random⊒ (βˆ‘ j, x j β€’ (A j, K j)).2 = (βˆ‘ j, x j β€’ A j, βˆ‘ j, x j β€’ K j).2 n:β„•Ξ“:AccessStructure nF:Type u_2inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•x:Fin d β†’ FA:Fin d β†’ L.SecretK:Fin d β†’ L.Random⊒ (βˆ‘ j, x j β€’ (A j, K j)).1 = (βˆ‘ j, x j β€’ A j, βˆ‘ j, x j β€’ K j).1 All goals completed! πŸ™ n:β„•Ξ“:AccessStructure nF:Type u_2inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•x:Fin d β†’ FA:Fin d β†’ L.SecretK:Fin d β†’ L.Random⊒ (βˆ‘ j, x j β€’ (A j, K j)).2 = (βˆ‘ j, x j β€’ A j, βˆ‘ j, x j β€’ K j).2 All goals completed! πŸ™ -- The Homomorphism Lemma lemma worker_homomorphism {d : β„•} (A : Fin d β†’ L.Secret) (K : Fin d β†’ L.Random) (x : Fin d β†’ F) (i : Fin n) : L.worker_compute_impl i (fun j => L.dealer (A j) (K j) i) x = L.dealer (target_computation L A x) (aggregate_key L K x) i := n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin n⊒ L.worker_compute_impl i (fun j => L.dealer (A j) (K j) i) x = L.dealer (L.target_computation A x) (L.aggregate_key K x) i n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin nΞ¨:L.Secret Γ— L.Random β†’β‚—[F] (i : Fin n) β†’ L.Share i := L.dealer_linear⊒ L.worker_compute_impl i (fun j => L.dealer (A j) (K j) i) x = L.dealer (L.target_computation A x) (L.aggregate_key K x) i calc worker_compute_impl L i (fun j => L.dealer (A j) (K j) i) x -- 1. Definition of worker_compute = βˆ‘ j, x j β€’ L.dealer (A j) (K j) i := rfl -- 2. Convert L.dealer to Ξ¨ (the LinearMap) -- inside the sum _ = βˆ‘ j, x j β€’ (Ξ¨ (A j, K j) i) := n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin nΞ¨:L.Secret Γ— L.Random β†’β‚—[F] (i : Fin n) β†’ L.Share i := L.dealer_linear⊒ βˆ‘ j, x j β€’ L.dealer (A j) (K j) i = βˆ‘ j, x j β€’ Ξ¨ (A j, K j) i n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin nΞ¨:L.Secret Γ— L.Random β†’β‚—[F] (i : Fin n) β†’ L.Share i := L.dealer_linear⊒ βˆ€ x_1 ∈ Finset.univ, x x_1 β€’ L.dealer (A x_1) (K x_1) i = x x_1 β€’ Ξ¨ (A x_1, K x_1) i intro j n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin nΞ¨:L.Secret Γ— L.Random β†’β‚—[F] (i : Fin n) β†’ L.Share i := L.dealer_linearj:Fin da✝:j ∈ Finset.univ⊒ x j β€’ L.dealer (A j) (K j) i = x j β€’ Ξ¨ (A j, K j) i All goals completed! πŸ™ -- Use the consistency property -- 3. Pull the evaluation 'i' outside the -- scalar multiplication -- (c β€’ f) i = c β€’ (f i) _ = βˆ‘ j, (x j β€’ Ξ¨ (A j, K j)) i := rfl -- 4. Pull the evaluation 'i' outside the sum -- (βˆ‘ f) i = βˆ‘ (f i) _ = (βˆ‘ j, x j β€’ Ξ¨ (A j, K j)) i := n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin nΞ¨:L.Secret Γ— L.Random β†’β‚—[F] (i : Fin n) β†’ L.Share i := L.dealer_linear⊒ βˆ‘ j, (x j β€’ Ξ¨ (A j, K j)) i = (βˆ‘ j, x j β€’ Ξ¨ (A j, K j)) i All goals completed! πŸ™ -- 5. Use Linearity of Ξ¨: βˆ‘ c β€’ Ξ¨(v) = Ξ¨(βˆ‘ c β€’ v) _ = (Ξ¨ (βˆ‘ j, x j β€’ (A j, K j))) i := n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin nΞ¨:L.Secret Γ— L.Random β†’β‚—[F] (i : Fin n) β†’ L.Share i := L.dealer_linear⊒ (βˆ‘ j, x j β€’ Ξ¨ (A j, K j)) i = Ξ¨ (βˆ‘ j, x j β€’ (A j, K j)) i n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin nΞ¨:L.Secret Γ— L.Random β†’β‚—[F] (i : Fin n) β†’ L.Share i := L.dealer_linear⊒ (βˆ‘ j, x j β€’ Ξ¨ (A j, K j)) i = (βˆ‘ x_1, Ξ¨ (x x_1 β€’ (A x_1, K x_1))) i -- Move scalar multiplication inside the map simp_rw n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin nΞ¨:L.Secret Γ— L.Random β†’β‚—[F] (i : Fin n) β†’ L.Share i := L.dealer_linear⊒ (βˆ‘ j, x j β€’ Ξ¨ (A j, K j)) i = (βˆ‘ x_1, Ξ¨ (x x_1 β€’ (A x_1, K x_1))) imap_smul] -- 6. Combine the arguments inside the pair -- βˆ‘ (x β€’ A, x β€’ K) = (βˆ‘ x A, βˆ‘ x K) _ = (Ξ¨ (βˆ‘ j, x j β€’ A j, βˆ‘ j, x j β€’ K j)) i := n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin nΞ¨:L.Secret Γ— L.Random β†’β‚—[F] (i : Fin n) β†’ L.Share i := L.dealer_linear⊒ Ξ¨ (βˆ‘ j, x j β€’ (A j, K j)) i = Ξ¨ (βˆ‘ j, x j β€’ A j, βˆ‘ j, x j β€’ K j) i All goals completed! πŸ™ -- 7. Convert back to definitions of target_computation -- and aggregate_key _ = Ξ¨ (target_computation L A x, aggregate_key L K x) i := rfl -- 8. Convert back to L.dealer _ = L.dealer (target_computation L A x) (aggregate_key L K x) i := n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ Fi:Fin nΞ¨:L.Secret Γ— L.Random β†’β‚—[F] (i : Fin n) β†’ L.Share i := L.dealer_linear⊒ Ξ¨ (L.target_computation A x, L.aggregate_key K x) i = L.dealer (L.target_computation A x) (L.aggregate_key K x) i All goals completed! πŸ™

In the main theorem we prove that a linear secret sharing scheme (LSSS) correctly implements secure distributed matrix multiplication (SDMM). Since L is an LSSS, it is a perfectly secure secret sharing scheme. We utilize the linear encoding operation in L to perform matrix multiplication. The resulting distributed matrix multiplication scheme is thus provably secure.

theorem distributed_computing_correctness {d : β„•} (A : Fin d β†’ L.Secret) (K : Fin d β†’ L.Random) (x : Fin d β†’ F) (B : Set (Fin n)) (hB : B ∈ Ξ“.auth) : let worker_responses (i : B) := L.worker_compute_impl i (fun j => L.dealer (A j) (K j) i) x L.recon B hB worker_responses = target_computation L A x := n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ FB:Set (Fin n)hB:B ∈ Ξ“.auth⊒ let worker_responses := fun i => L.worker_compute_impl (↑i) (fun j => L.dealer (A j) (K j) ↑i) x; L.recon B hB worker_responses = L.target_computation A x have h_valid_shares : (fun i : B => L.worker_compute_impl i (fun j => L.dealer (A j) (K j) i) x) = shares_of_set L.toSecretSharingScheme (target_computation L A x) (aggregate_key L K x) B := n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ FB:Set (Fin n)hB:B ∈ Ξ“.auth⊒ let worker_responses := fun i => L.worker_compute_impl (↑i) (fun j => L.dealer (A j) (K j) ↑i) x; L.recon B hB worker_responses = L.target_computation A x n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ FB:Set (Fin n)hB:B ∈ Ξ“.authi:↑B⊒ L.worker_compute_impl (↑i) (fun j => L.dealer (A j) (K j) ↑i) x = L.shares_of_set (L.target_computation A x) (L.aggregate_key K x) B i All goals completed! πŸ™ n:β„•Ξ“:AccessStructure nF:Type u_1inst✝:Field FL:LinearSecretSharingScheme n Ξ“ Fd:β„•A:Fin d β†’ L.SecretK:Fin d β†’ L.Randomx:Fin d β†’ FB:Set (Fin n)hB:B ∈ Ξ“.authh_valid_shares:(fun i => L.worker_compute_impl (↑i) (fun j => L.dealer (A j) (K j) ↑i) x) = L.shares_of_set (L.target_computation A x) (L.aggregate_key K x) B⊒ let worker_responses := L.shares_of_set (L.target_computation A x) (L.aggregate_key K x) B; L.recon B hB worker_responses = L.target_computation A x All goals completed! πŸ™

Using LSSS, we can now define a structure SecureDistributedMatrixMultiplication that represents SDMM.

structure SecureDistributedMatrixMultiplication (n : β„•) (Ξ“ : AccessStructure n) (F : Type*) [Field F] extends LinearSecretSharingScheme n Ξ“ F where /- Construct the DistributedMatrixMultiplication instance using the definitions and theorems from LinearSecretSharingScheme. -/ toDistMatrixMul : DistributedMatrixMultiplication n Ξ“ F := { Secret := Secret Share := Share Random := Random -- Map LSSS functions to Protocol functions encode := dealer reconstruct := recon worker_compute := fun i shares x => worker_compute_impl toLinearSecretSharingScheme i shares x -- Instances secret_add := secret_add secret_module := secret_module -- Proof of correctness h_distributed_correctness := n✝:β„•Ξ“βœ:AccessStructure n✝F✝:Type u_1inst✝¹:Field F✝L:LinearSecretSharingScheme n✝ Ξ“βœ F✝n:β„•Ξ“:AccessStructure nF:Type u_2inst✝:Field FSecret:Type ?u.52Random:Type ?u.103hSecret:Fintype SecrethSecret_card:Fintype.card Secret β‰₯ 2Share:Fin n β†’ Type ?u.52hShare:(i : Fin n) β†’ Fintype (Share i)hRandom:Fintype RandomhRandomNonempty:Nonempty RandomΞΌ:PMF Randomdealer:Secret β†’ Random β†’ (i : Fin n) β†’ Share itoSecretSharingScheme:SecretSharingScheme n := { Secret := Secret, Random := Random, hSecret := hSecret, hSecret_card := hSecret_card, Share := Share, hShare := hShare, hRandom := hRandom, hRandomNonempty := hRandomNonempty, ΞΌ := ΞΌ, dealer := dealer }recon:toSecretSharingScheme.ReconstructionAlgorithm Ξ“h_correctness:toSecretSharingScheme.Correctness Ξ“ reconh_security:toSecretSharingScheme.PerfectSecurity Ξ“toRealizedSecretSharingScheme:RealizedSecretSharingScheme n Ξ“ := { toSecretSharingScheme := toSecretSharingScheme, recon := recon, h_correctness := h_correctness, h_security := h_security }secret_add:AddCommMonoid Secretrandom_add:AddCommMonoid Randomshare_add:(i : Fin n) β†’ AddCommMonoid (Share i)secret_module:Module F Secretrandom_module:Module F Randomshare_module:(i : Fin n) β†’ Module F (Share i)dealer_linear:Secret Γ— Random β†’β‚—[F] (i : Fin n) β†’ Share ih_dealer_eq:βˆ€ (s : Secret) (r : Random), dealer_linear (s, r) = dealer s rrecon_linear:(B : Set (Fin n)) β†’ B ∈ Ξ“.auth β†’ ((i : ↑B) β†’ Share ↑i) β†’β‚—[F] Secreth_recon_eq:βˆ€ (B : Set (Fin n)) (hB : B ∈ Ξ“.auth) (shares : (i : ↑B) β†’ Share ↑i), (recon_linear B hB) shares = recon B hB sharestoLinearSecretSharingScheme:LinearSecretSharingScheme n Ξ“ F := { toRealizedSecretSharingScheme := toRealizedSecretSharingScheme, secret_add := secret_add, random_add := random_add, share_add := share_add, secret_module := secret_module, random_module := random_module, share_module := share_module, dealer_linear := dealer_linear, h_dealer_eq := h_dealer_eq, recon_linear := recon_linear, h_recon_eq := h_recon_eq }⊒ βˆ€ {d : β„•} (A : Fin d β†’ Secret) (K : Fin d β†’ Random) (x : Fin d β†’ F) (B : Set (Fin n)) (hB : B ∈ Ξ“.auth), let shares := fun j i => dealer (A j) (K j) i; let responses := fun i => toLinearSecretSharingScheme.worker_compute_impl (↑i) (fun j => shares j ↑i) x; recon B hB responses = βˆ‘ j, x j β€’ A j n✝:β„•Ξ“βœ:AccessStructure n✝F✝:Type u_1inst✝¹:Field F✝L:LinearSecretSharingScheme n✝ Ξ“βœ F✝n:β„•Ξ“:AccessStructure nF:Type u_2inst✝:Field FSecret:Type ?u.52Random:Type ?u.103hSecret:Fintype SecrethSecret_card:Fintype.card Secret β‰₯ 2Share:Fin n β†’ Type ?u.52hShare:(i : Fin n) β†’ Fintype (Share i)hRandom:Fintype RandomhRandomNonempty:Nonempty RandomΞΌ:PMF Randomdealer:Secret β†’ Random β†’ (i : Fin n) β†’ Share itoSecretSharingScheme:SecretSharingScheme n := { Secret := Secret, Random := Random, hSecret := hSecret, hSecret_card := hSecret_card, Share := Share, hShare := hShare, hRandom := hRandom, hRandomNonempty := hRandomNonempty, ΞΌ := ΞΌ, dealer := dealer }recon:toSecretSharingScheme.ReconstructionAlgorithm Ξ“h_correctness:toSecretSharingScheme.Correctness Ξ“ reconh_security:toSecretSharingScheme.PerfectSecurity Ξ“toRealizedSecretSharingScheme:RealizedSecretSharingScheme n Ξ“ := { toSecretSharingScheme := toSecretSharingScheme, recon := recon, h_correctness := h_correctness, h_security := h_security }secret_add:AddCommMonoid Secretrandom_add:AddCommMonoid Randomshare_add:(i : Fin n) β†’ AddCommMonoid (Share i)secret_module:Module F Secretrandom_module:Module F Randomshare_module:(i : Fin n) β†’ Module F (Share i)dealer_linear:Secret Γ— Random β†’β‚—[F] (i : Fin n) β†’ Share ih_dealer_eq:βˆ€ (s : Secret) (r : Random), dealer_linear (s, r) = dealer s rrecon_linear:(B : Set (Fin n)) β†’ B ∈ Ξ“.auth β†’ ((i : ↑B) β†’ Share ↑i) β†’β‚—[F] Secreth_recon_eq:βˆ€ (B : Set (Fin n)) (hB : B ∈ Ξ“.auth) (shares : (i : ↑B) β†’ Share ↑i), (recon_linear B hB) shares = recon B hB sharestoLinearSecretSharingScheme:LinearSecretSharingScheme n Ξ“ F := { toRealizedSecretSharingScheme := toRealizedSecretSharingScheme, secret_add := secret_add, random_add := random_add, share_add := share_add, secret_module := secret_module, random_module := random_module, share_module := share_module, dealer_linear := dealer_linear, h_dealer_eq := h_dealer_eq, recon_linear := recon_linear, h_recon_eq := h_recon_eq }d:β„•A:Fin d β†’ SecretK:Fin d β†’ Randomx:Fin d β†’ FB:Set (Fin n)hB:B ∈ Ξ“.auth⊒ let shares := fun j i => dealer (A j) (K j) i; let responses := fun i => toLinearSecretSharingScheme.worker_compute_impl (↑i) (fun j => shares j ↑i) x; recon B hB responses = βˆ‘ j, x j β€’ A j All goals completed! πŸ™ } end LinearSecretSharingScheme end DistributedHierarchy