2-out-of-2 Additive Secret Sharing: Perfect Privacy

The 2-out-of-2 additive (XOR) secret-sharing scheme has perfect privacy: one share alone is uniformly distributed and independent of the shared secret, so an adversary holding a single share has advantage exactly 0 in distinguishing which secret was shared. Following Rosulek, The Joy of Cryptography (secret sharing).

This result is information-theoretic and self-contained — the cleanest possible instance of the bijection-coupling technique.

Overview

To share a secret bit s, sample a uniform bit k and hand out the two shares

share₁ = k        share₂ = k ⊕ s

Reconstruction is share₁ ⊕ share₂ = k ⊕ (k ⊕ s) = s, so the two shares together determine s. Privacy is the statement that either share on its own reveals nothing about s:

• share₁ = k is a uniform bit, manifestly independent of s;
• share₂ = k ⊕ s is XOR-by-s of a uniform key, hence again uniform and independent of s — exactly the one-time-pad argument.

The privacy game reveals the share held by the corrupted party (indexed by a bit i) for one of two adversarially chosen secrets s₀, s₁. For any fixed i, the two games couple through a single uniform sample — for i = true via XOR-by-(s₀ ⊕ s₁), for i = false via the identity — so advantage_zero_of_rHoare collapses the advantage to 0.

Main definitions

• shareXor — the 2-of-2 XOR sharing of a bit: k ↦ (k, k ⊕ s).
• revealShare — the share seen by the corrupted party i.
• SS_Privacy_Game / SS_Privacy_Adv — the one-share privacy game and its advantage.

Main results

• shareXor_reconstruct — the two shares reconstruct the secret.
• ss_privacy_coupling — the two privacy games are equidistributed.
• ss_perfect_privacy — perfect privacy: SS_Privacy_Adv i s₀ s₁ A = 0 for every corrupted party i, every pair of secrets, and every adversary A.

References

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

The 2-of-2 XOR Sharing

def CatCrypt.Examples.SecretSharing.revealShare (i k s : Bool) : Bool

The share held by corrupted party i, given key k and secret s: party false holds share₁ = k, party true holds share₂ = k ⊕ s.

Equations

• CatCrypt.Examples.SecretSharing.revealShare i k s = if i = true then k ^^ s else k

noncomputable def CatCrypt.Examples.SecretSharing.shareXor (s : Bool) : Core.SPComp (Bool × Bool)

The 2-out-of-2 additive (XOR) sharing of a secret bit s: sample a uniform key k; the shares are (k, k ⊕ s).

Equations

• CatCrypt.Examples.SecretSharing.shareXor s = do let k ← CatCrypt.Core.SPComp.sample Bool CatCrypt.Core.SPComp.pure (k, k ^^ s)

Reconstruction

theorem CatCrypt.Examples.SecretSharing.shareXor_reconstruct (k s : Bool) : (k ^^ (k ^^ s)) = s

The two shares reconstruct the secret: share₁ ⊕ share₂ = s.

The One-Share Privacy Game

noncomputable def CatCrypt.Examples.SecretSharing.SS_Privacy_Game (i s₀ s₁ b : Bool) : Core.SPComp Bool

Privacy game for 2-of-2 XOR sharing. The corrupted party i is handed its single share of one of two adversarially chosen secrets:

• SS_Privacy_Game i s₀ s₁ true shares s₀ (left/real)
• SS_Privacy_Game i s₀ s₁ false shares s₁ (right/ideal)

The adversary sees only party i's share and tries to tell the two apart.

Equations

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

noncomputable def CatCrypt.Examples.SecretSharing.SS_Privacy_Adv (i s₀ s₁ : Bool) (A : Bool → Core.SPComp Bool) : ENNReal

Privacy advantage: the corrupted party's distinguishing probability between a share of s₀ and a share of s₁.

Equations

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

Perfect Privacy

noncomputable def CatCrypt.Examples.SecretSharing.shareBij (i s₀ s₁ : Bool) : Bool ≃ Bool

The key-remap bijection coupling the two privacy games. For the corrupted party i, it maps the key used to share s₀ to the key sharing s₁ while keeping party i's revealed share fixed: XOR-by-(s₀ ⊕ s₁) when i = true, the identity when i = false.

Equations

• CatCrypt.Examples.SecretSharing.shareBij i s₀ s₁ = if i = true then CatCrypt.Prob.XorBij.boolXorBij (s₀ ^^ s₁) else Equiv.refl Bool

theorem CatCrypt.Examples.SecretSharing.ss_privacy_coupling (i s₀ s₁ : Bool) : Relational.rHoare Relational.eqPre (SS_Privacy_Game i s₀ s₁ true) (SS_Privacy_Game i s₀ s₁ false) Relational.eqPost

Coupling: for a fixed corrupted party, the two privacy games are equidistributed. The revealed share over a uniform key is equidistributed with a plain uniform sample (XOR-by-a-fixed-value is a bijection of the key, the identity when the plain share is revealed), so the two games couple by transitivity through the uniform sample.

theorem CatCrypt.Examples.SecretSharing.ss_perfect_privacy (i s₀ s₁ : Bool) (A : Bool → Core.SPComp Bool) : SS_Privacy_Adv i s₀ s₁ A = 0

2-of-2 XOR secret sharing has perfect privacy: for either corrupted party i, any two secrets s₀, s₁, and any adversary A, the one-share privacy advantage is exactly 0. A single share is uniform and independent of the secret.

Reflection into the Package / UC Stack

The shallow ss_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 is heap-independent, so the shallow coupling ss_privacy_coupling 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.SecretSharing.ssGameRaw (i s₀ s₁ b : Bool) : Deep.RawCode Bool

The reflected one-share privacy-game body for corrupted party i and bit b.

Equations

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

instance CatCrypt.Examples.SecretSharing.instValidSsGameRaw (i s₀ s₁ b : Bool) : Deep.IsValid ∅ (ssGameRaw i s₀ s₁ b)

theorem CatCrypt.Examples.SecretSharing.ssGameRaw_eval_shallow (i s₀ s₁ b : Bool) : (ssGameRaw i s₀ s₁ b).eval = SS_Privacy_Game i s₀ s₁ b

The reflected body evaluates back to the shallow privacy game.

theorem CatCrypt.Examples.SecretSharing.ss_game_isPure (i s₀ s₁ b : Bool) : (SS_Privacy_Game i s₀ s₁ b).IsPure

The privacy game is heap-independent (a uniform sample then a pure reveal).

theorem CatCrypt.Examples.SecretSharing.ssGameRaw_eval_eq (i s₀ s₁ : Bool) : (ssGameRaw i s₀ s₁ true).eval = (ssGameRaw i s₀ s₁ false).eval

The two reflected bodies (share of s₀ vs. s₁) have equal evaluations: the heap-independent coupling ss_privacy_coupling upgrades to SPComp equality.

noncomputable def CatCrypt.Examples.SecretSharing.ssGameTrue (i s₀ s₁ : Bool) : Deep.NomPackage

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

Equations

• CatCrypt.Examples.SecretSharing.ssGameTrue i s₀ s₁ = CatCrypt.Deep.NomPackage.ofOracle 1 Unit Bool fun (x : Unit) => CatCrypt.Examples.SecretSharing.ssGameRaw i s₀ s₁ true

noncomputable def CatCrypt.Examples.SecretSharing.ssGameFalse (i s₀ s₁ : Bool) : Deep.NomPackage

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

Equations

• CatCrypt.Examples.SecretSharing.ssGameFalse i s₀ s₁ = CatCrypt.Deep.NomPackage.ofOracle 1 Unit Bool fun (x : Unit) => CatCrypt.Examples.SecretSharing.ssGameRaw i s₀ s₁ false

theorem CatCrypt.Examples.SecretSharing.ss_deepnom_zero (i s₀ s₁ : Bool) (A : Deep.NomPackage) : Crypto.DeepNomAdvantage (ssGameTrue i s₀ s₁) (ssGameFalse i s₀ s₁) A = 0

Zero deep-nominal advantage against every adversary package.

theorem CatCrypt.Examples.SecretSharing.ss_sdist_zero (i s₀ s₁ : Bool) : (Crypto.sdist (fun (A : Deep.NomPackage) => Crypto.runPkg (A.pkg.link (ssGameTrue i s₀ s₁).pkg)) fun (A : Deep.NomPackage) => Crypto.runPkg (A.pkg.link (ssGameFalse i s₀ s₁).pkg)) = 0

Statistical distance zero between the two linked-game families.

theorem CatCrypt.Examples.SecretSharing.ss_nompkg_secure (i s₀ s₁ : Bool) : Crypto.NomPkgSecure (ssGameTrue i s₀ s₁) (ssGameFalse i s₀ s₁) fun (x : Deep.NomPackage) => 0

Package-level perfect privacy (NomPkgSecure).

theorem CatCrypt.Examples.SecretSharing.ss_uc (i s₀ s₁ : Bool) : 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 (ssGameTrue i s₀ s₁).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 (ssGameFalse i s₀ s₁).pkg))

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

theorem CatCrypt.Examples.SecretSharing.ss_deepnom_forward_eq_adv (i s₀ s₁ : Bool) : Crypto.DeepNomAdvantage (ssGameTrue i s₀ s₁) (ssGameFalse i s₀ s₁) Deep.forwardAdv = SS_Privacy_Adv i s₀ s₁ Core.SPComp.pure

Reflection mirrors the shallow game. Against the forwarding adversary, the deep-nominal advantage equals the shallow privacy advantage under the identity distinguisher — which is 0 by ss_perfect_privacy.