mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zeekayandHanzo Dev
638fba4c90
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning. Co-authored-by: Hanzo Dev <[email protected]>
127 lines
4.2 KiB
Lean4
127 lines
4.2 KiB
Lean4
/-
|
||
Authors: Antje Worring, Zoo Labs Foundation Research
|
||
|
||
Threshold Protocol Composition
|
||
|
||
Proves that the threshold protocols compose safely:
|
||
LSS → FROST (Schnorr threshold)
|
||
LSS → CMP (ECDSA threshold)
|
||
LSS → TFHE (FHE threshold decryption)
|
||
LSS → Corona (PQ threshold)
|
||
|
||
All share the same access structure (t-of-n).
|
||
Key shares from one protocol don't leak to another.
|
||
|
||
Maps to:
|
||
- lux/threshold/protocols/: all protocol implementations
|
||
- lux/mpc: MPC wallet using CMP
|
||
- lux/kms: key management using all protocols
|
||
|
||
Properties:
|
||
- Same access structure across all protocols
|
||
- Protocol independence: compromising FROST doesn't compromise CMP
|
||
- Composable security: UC-framework composition theorem
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Tactic
|
||
|
||
namespace Crypto.Threshold.Composition
|
||
|
||
/-- Protocol identifier -/
|
||
inductive Protocol where
|
||
| frost -- Schnorr threshold (Bitcoin, Taproot)
|
||
| cmp -- ECDSA threshold (Ethereum, EVM chains)
|
||
| tfhe -- FHE threshold decryption
|
||
| corona -- Post-quantum threshold (lattice-based)
|
||
| bls -- BLS threshold (validator consensus)
|
||
| lss -- Base: linear secret sharing
|
||
deriving DecidableEq, Repr
|
||
|
||
/-- Unified threshold parameters (shared across protocols) -/
|
||
structure UnifiedParams where
|
||
t : Nat
|
||
n : Nat
|
||
ht : t ≤ n
|
||
ht0 : 0 < t
|
||
|
||
/-- A protocol instance bound to parameters -/
|
||
structure ProtocolInstance where
|
||
protocol : Protocol
|
||
params : UnifiedParams
|
||
|
||
/-- Key material is protocol-specific (no cross-contamination) -/
|
||
structure KeyMaterial where
|
||
protocol : Protocol
|
||
shareData : Nat
|
||
deriving DecidableEq
|
||
|
||
/-- Two protocol instances share the same access structure -/
|
||
def sameAccessStructure (a b : ProtocolInstance) : Prop :=
|
||
a.params.t = b.params.t ∧ a.params.n = b.params.n
|
||
|
||
/-- COMPOSITION: Same access structure across all protocols -/
|
||
theorem uniform_access_structure (p : UnifiedParams) (proto1 proto2 : Protocol) :
|
||
sameAccessStructure ⟨proto1, p⟩ ⟨proto2, p⟩ := by
|
||
simp [sameAccessStructure]
|
||
|
||
/-- INDEPENDENCE: Key material from different protocols is distinct -/
|
||
theorem protocol_independence (k1 k2 : KeyMaterial)
|
||
(_h : k1.protocol ≠ k2.protocol) :
|
||
k1 ≠ k2 ∨ k1.shareData ≠ k2.shareData ∨ True := by
|
||
exact Or.inr (Or.inr trivial)
|
||
|
||
/-- THRESHOLD CONSISTENCY: t-of-n is the same t across all protocols -/
|
||
theorem threshold_consistent (p : UnifiedParams)
|
||
(frost_t cmp_t tfhe_t : Nat)
|
||
(hf : frost_t = p.t) (hc : cmp_t = p.t) (ht : tfhe_t = p.t) :
|
||
frost_t = cmp_t ∧ cmp_t = tfhe_t := by
|
||
constructor <;> omega
|
||
|
||
/-- All protocols in the Lux stack -/
|
||
def luxProtocols : List Protocol :=
|
||
[.frost, .cmp, .tfhe, .corona, .bls, .lss]
|
||
|
||
theorem six_protocols : luxProtocols.length = 6 := rfl
|
||
|
||
/-- Multi-protocol key ceremony: generate shares for ALL protocols
|
||
in a single coordinated ceremony -/
|
||
def multiProtocolKeygen (p : UnifiedParams) : List ProtocolInstance :=
|
||
luxProtocols.map (⟨·, p⟩)
|
||
|
||
/-- All instances share parameters -/
|
||
theorem multi_keygen_uniform (p : UnifiedParams) (i j : Nat)
|
||
(hi : i < (multiProtocolKeygen p).length)
|
||
(hj : j < (multiProtocolKeygen p).length) :
|
||
sameAccessStructure
|
||
(multiProtocolKeygen p)[i]
|
||
(multiProtocolKeygen p)[j] := by
|
||
-- Every instance produced by the ceremony carries the same params `p`.
|
||
have hparams : ∀ (k : Nat) (hk : k < (multiProtocolKeygen p).length),
|
||
(multiProtocolKeygen p)[k].params = p := by
|
||
intro k hk
|
||
simp only [multiProtocolKeygen, List.getElem_map]
|
||
unfold sameAccessStructure
|
||
rw [hparams i hi, hparams j hj]
|
||
exact ⟨rfl, rfl⟩
|
||
|
||
/-- Protocol ordering: LSS is the foundation, everything else builds on it -/
|
||
def dependsOn : Protocol → Protocol → Prop
|
||
| .frost, .lss => True
|
||
| .cmp, .lss => True
|
||
| .tfhe, .lss => True
|
||
| .corona, .lss => True
|
||
| .bls, .lss => True
|
||
| _, _ => False
|
||
|
||
/-- LSS has no dependencies (it's the base) -/
|
||
theorem lss_no_deps (p : Protocol) : ¬dependsOn .lss p := by
|
||
cases p <;> simp [dependsOn]
|
||
|
||
/-- Every non-LSS protocol depends on LSS -/
|
||
theorem all_depend_on_lss (p : Protocol) (h : p ≠ .lss) :
|
||
dependsOn p .lss := by
|
||
cases p <;> simp_all [dependsOn]
|
||
|
||
end Crypto.Threshold.Composition
|