Additive Secret Sharing over Finite Commutative Groups

This file defines generic additive secret sharing over any finite commutative group G ([AddCommGroup G] [Fintype G]):

• ProbComp.completeShares: deterministically completes m - 1 shares init : Fin (m - 1) → G to an m-tuple summing to target : G by setting the last coordinate ((⊤ : Fin m)) to target - ∑ j : Fin (m - 1), init j.
• ProbComp.sampleAdditiveShares: samples m - 1 uniform coordinates in G and completes the last coordinate so that ∑ i : Fin m, s i = target.
• ProbComp.eval_restrict_sampleAdditiveShares: for any proper coalition I ≠ Finset.univ, the marginal distribution of I's shares is uniform on (i : I) → G and independent of target.
• ProbComp.completeSharesErase and ProbComp.eq_eval_sampleAdditiveShares_of_sum_of_map_erase: recovering all m shares from the m - 1 coordinates outside any single party j₀ : Fin m, used when simulating protocols in which an honest party j₀ sets its share from the remaining m - 1 shares.

Main definitions

• Cslib.ProbComp.initOfShares
• Cslib.ProbComp.completeShares
• Cslib.ProbComp.sampleAdditiveShares
• Cslib.ProbComp.completeSharesErase

Main results

• Cslib.ProbComp.sum_completeShares
• Cslib.ProbComp.completeShares_initOfShares
• Cslib.ProbComp.completeShares_add
• Cslib.ProbComp.sum_sampleAdditiveShares
• Cslib.ProbComp.mem_support_sampleAdditiveShares_iff
• Cslib.ProbComp.eq_eval_sampleAdditiveShares_of_sum_of_map_init
• Cslib.ProbComp.eval_restrict_sampleAdditiveShares
• Cslib.ProbComp.eval_sampleAdditiveShares_eq_map_completeSharesErase
• Cslib.ProbComp.eq_eval_sampleAdditiveShares_of_sum_of_map_erase

References

• O. Goldreich, Foundations of Cryptography, Volume 2: Basic Applications, Section 7.5.2.3 (Construction 7.5.10, Step 1), print pp. 705–706.

def Cslib.ProbComp.initOfShares (m : ℕ) {G : Type} (s : Fin m → G) : Fin (m - 1) → G

Extract the first m - 1 coordinates of an m-tuple via Fin.castLE (Nat.sub_le m 1).

def Cslib.ProbComp.completeShares (m : ℕ) {G : Type} [AddCommGroup G] (target : G) (init : Fin (m - 1) → G) : Fin m → G

Deterministically complete m - 1 shares init : Fin (m - 1) → G to Fin m → G summing to target, setting the last coordinate to target - ∑ j : Fin (m - 1), init j.

@[simp]

theorem Cslib.ProbComp.completeShares_castLE (m : ℕ) {G : Type} [AddCommGroup G] (target : G) (init : Fin (m - 1) → G) (k : Fin (m - 1)) : completeShares m target init (Fin.castLE ⋯ k) = init k

@[simp]

theorem Cslib.ProbComp.initOfShares_completeShares (m : ℕ) {G : Type} [AddCommGroup G] (target : G) (init : Fin (m - 1) → G) : initOfShares m (completeShares m target init) = init

@[simp]

theorem Cslib.ProbComp.completeShares_top (m : ℕ) [NeZero m] {G : Type} [AddCommGroup G] (target : G) (init : Fin (m - 1) → G) : completeShares m target init ⊤ = target - ∑ j : Fin (m - 1), init j

@[simp]

theorem Cslib.ProbComp.sum_completeShares (m : ℕ) [NeZero m] {G : Type} [AddCommGroup G] (target : G) (init : Fin (m - 1) → G) : ∑ i : Fin m, completeShares m target init i = target

theorem Cslib.ProbComp.completeShares_initOfShares (m : ℕ) [NeZero m] {G : Type} [AddCommGroup G] {target : G} {s : Fin m → G} (hs : ∑ i : Fin m, s i = target) : completeShares m target (initOfShares m s) = s

Any m-tuple s summing to target is recovered from its first m - 1 coordinates by completeShares m target.

theorem Cslib.ProbComp.completeShares_add (m : ℕ) {G : Type} [AddCommGroup G] (target₁ target₂ : G) (init₁ init₂ : Fin (m - 1) → G) : completeShares m (target₁ + target₂) (init₁ + init₂) = completeShares m target₁ init₁ + completeShares m target₂ init₂

noncomputable def Cslib.ProbComp.sampleAdditiveShares (m : ℕ) {G : Type} [AddCommGroup G] [Fintype G] (target : G) : ProbComp (Fin m → G)

Sample uniform additive shares s : Fin m → G conditioned on ∑ i, s i = target.

theorem Cslib.ProbComp.sum_sampleAdditiveShares {m : ℕ} [NeZero m] {G : Type} [AddCommGroup G] [Fintype G] (target : G) {s : Fin m → G} (hs : s ∈ (sampleAdditiveShares m target).eval.support) : ∑ i : Fin m, s i = target

theorem Cslib.ProbComp.mem_support_sampleAdditiveShares_iff {m : ℕ} [NeZero m] {G : Type} [AddCommGroup G] [Fintype G] (target : G) (s : Fin m → G) : s ∈ (sampleAdditiveShares m target).eval.support ↔ ∑ i : Fin m, s i = target

theorem Cslib.ProbComp.eq_eval_sampleAdditiveShares_of_sum_of_map_init {m : ℕ} [NeZero m] {G : Type} [AddCommGroup G] [Fintype G] {target : G} {p : PMF (Fin m → G)} (hsum : ∀ s ∈ p.support, ∑ i : Fin m, s i = target) (hinit : PMF.map (initOfShares m) p = Probability.PMF.uniformOfFintype (Fin (m - 1) → G)) : p = (sampleAdditiveShares m target).eval

Any distribution p on Fin m → G supported on tuples summing to target whose first m - 1 coordinates are uniformly distributed equals eval (sampleAdditiveShares m target).

theorem Cslib.ProbComp.eval_restrict_sampleAdditiveShares {m : ℕ} [NeZero m] {G : Type} [AddCommGroup G] [Fintype G] (I : Finset (Fin m)) (hI : I ≠ Finset.univ) (target : G) : PMF.map I.restrict (sampleAdditiveShares m target).eval = Probability.PMF.uniformOfFintype (↥I → G)

For any proper coalition I ≠ Finset.univ, the marginal distribution of I's shares is uniform on (i : I) → G and independent of target.

def Cslib.ProbComp.completeSharesErase {m : ℕ} {G : Type} [AddCommGroup G] (j₀ : Fin m) (target : G) (sub : ↥(Finset.univ.erase j₀) → G) : Fin m → G

Deterministically complete shares on Finset.univ.erase j₀ to Fin m → G summing to target, setting coordinate j₀ to target - ∑ k : Finset.univ.erase j₀, sub k.

@[simp]

theorem Cslib.ProbComp.restrict_erase_completeSharesErase {m : ℕ} {G : Type} [AddCommGroup G] (j₀ : Fin m) (target : G) (sub : ↥(Finset.univ.erase j₀) → G) : (Finset.univ.erase j₀).restrict (completeSharesErase j₀ target sub) = sub

@[simp]

theorem Cslib.ProbComp.sum_completeSharesErase {m : ℕ} {G : Type} [AddCommGroup G] (j₀ : Fin m) (target : G) (sub : ↥(Finset.univ.erase j₀) → G) : ∑ i : Fin m, completeSharesErase j₀ target sub i = target

theorem Cslib.ProbComp.completeSharesErase_restrict_erase {m : ℕ} {G : Type} [AddCommGroup G] (j₀ : Fin m) {target : G} {s : Fin m → G} (hs : ∑ i : Fin m, s i = target) : completeSharesErase j₀ target ((Finset.univ.erase j₀).restrict s) = s

theorem Cslib.ProbComp.eval_sampleAdditiveShares_eq_map_completeSharesErase {m : ℕ} [NeZero m] {G : Type} [AddCommGroup G] [Fintype G] (j₀ : Fin m) (target : G) : (sampleAdditiveShares m target).eval = PMF.map (completeSharesErase j₀ target) (Probability.PMF.uniformOfFintype (↥(Finset.univ.erase j₀) → G))

For any party j₀ : Fin m, eval (sampleAdditiveShares m target) is the image of the uniform distribution on (i : Finset.univ.erase j₀) → G under completeSharesErase j₀ target.

theorem Cslib.ProbComp.eq_eval_sampleAdditiveShares_of_sum_of_map_erase {m : ℕ} [NeZero m] {G : Type} [AddCommGroup G] [Fintype G] (j₀ : Fin m) {target : G} {p : PMF (Fin m → G)} (hsum : ∀ s ∈ p.support, ∑ i : Fin m, s i = target) (herase : PMF.map (Finset.univ.erase j₀).restrict p = Probability.PMF.uniformOfFintype (↥(Finset.univ.erase j₀) → G)) : p = (sampleAdditiveShares m target).eval

Any distribution p on Fin m → G supported on tuples summing to target whose marginal on Finset.univ.erase j₀ is uniform equals eval (sampleAdditiveShares m target).