mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
ee09768de4
6 files passed under Lean's default but failed under the project's
`autoImplicit := false`: they relied on auto-bound implicits (FunctionalAgent's
α/β/γ/δ; Consensus/{Safety,Liveness} p:Params; Warp/{Ordering,Delivery} s';
Crypto/FROST Share index). Added explicit variable/binder declarations
(declaration-only; no proof meaning changed). Whole lean/ library now verifies
at 0 errors under `lake env lean -D autoImplicit=false` (88/88 files).
Co-authored-by: Hanzo Dev <[email protected]>
104 lines
3.6 KiB
Lean4
104 lines
3.6 KiB
Lean4
/-
|
|
Authors: Antje Worring, Zach Kelling
|
|
|
|
FROST Threshold Signature Correctness
|
|
|
|
Models the FROST precompile (src/precompiles/frost/).
|
|
|
|
FROST: Flexible Round-Optimized Schnorr Threshold signatures.
|
|
t-of-n threshold: any t participants can produce a valid Schnorr signature,
|
|
fewer than t cannot.
|
|
|
|
Maps to:
|
|
- src/precompiles/frost/contract.go: Verify function
|
|
- src/precompiles/frost/IFROST.sol: Solidity interface
|
|
- luxfi/threshold/protocols/frost: Keygen, Sign, Verify
|
|
|
|
Properties:
|
|
- Correctness: signature produced by t honest signers verifies
|
|
- Unforgeability: t-1 signers cannot forge (in random oracle model)
|
|
- Robustness: t honest signers always produce valid output
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace Crypto.FROST
|
|
|
|
/-- Threshold parameters -/
|
|
structure ThresholdParams where
|
|
t : Nat -- threshold
|
|
n : Nat -- total participants
|
|
ht : t ≤ n -- threshold <= total
|
|
ht0 : 0 < t -- need at least 1 signer
|
|
|
|
/-- Abstract Schnorr signature model -/
|
|
structure SchnorrSig where
|
|
R : Nat -- nonce commitment (32 bytes)
|
|
s : Nat -- response scalar (32 bytes)
|
|
|
|
/-- Verification (abstract Schnorr): s*G = R + H(R,pk,msg)*pk -/
|
|
axiom schnorr_verify : SchnorrSig → Nat → Nat → Bool
|
|
|
|
/-- Share: each participant holds a secret share (index among `n` participants) -/
|
|
structure Share (n : Nat) where
|
|
index : Fin n
|
|
value : Nat
|
|
|
|
/-- FROST correctness: if t honest participants execute the protocol,
|
|
the resulting signature verifies under the aggregate public key. -/
|
|
axiom frost_correctness :
|
|
∀ (p : ThresholdParams) (shares : List (Share p.n))
|
|
(msg : Nat) (aggPK : Nat),
|
|
shares.length ≥ p.t →
|
|
-- All shares are valid (from DKG)
|
|
∃ (sig : SchnorrSig), schnorr_verify sig aggPK msg = true
|
|
|
|
/-- FROST unforgeability: with fewer than t shares,
|
|
cannot produce a valid signature (in ROM). -/
|
|
axiom frost_unforgeability :
|
|
∀ (p : ThresholdParams) (compromised : Nat),
|
|
compromised < p.t →
|
|
-- Cannot forge: fewer than t shares cannot produce a valid signature
|
|
-- (discrete log hardness in random oracle model)
|
|
∀ (msg : Nat) (aggPK : Nat) (sig : SchnorrSig),
|
|
schnorr_verify sig aggPK msg = false
|
|
|
|
/-- Threshold property: exactly t signers suffice -/
|
|
theorem threshold_exact (p : ThresholdParams)
|
|
(signers : Nat) (h : signers ≥ p.t) :
|
|
signers > 0 := by
|
|
have := p.ht0; omega
|
|
|
|
/-- t-of-n: t must be at most n -/
|
|
theorem threshold_bounded (p : ThresholdParams) : p.t ≤ p.n := p.ht
|
|
|
|
/-- Security margin: compromising t-1 is safe -/
|
|
theorem security_margin (p : ThresholdParams) (compromised : Nat)
|
|
(h : compromised < p.t) : compromised + 1 ≤ p.n := by
|
|
have := p.ht; omega
|
|
|
|
/-- Robustness: if we have n participants and at most f < n-t+1 fail,
|
|
we still have t honest participants to sign -/
|
|
theorem robustness (p : ThresholdParams) (failures : Nat)
|
|
(h : failures ≤ p.n - p.t) :
|
|
p.n - failures ≥ p.t := by
|
|
have := p.ht; omega
|
|
|
|
/-- Optimal threshold: t = ceil(n/2)+1 for majority threshold -/
|
|
theorem majority_threshold_safe (n : Nat) (hn : n > 0)
|
|
(t : Nat) (ht : t = n / 2 + 1) :
|
|
t ≤ n ∧ t > n / 2 := by
|
|
constructor <;> omega
|
|
|
|
/-- Key share refresh: after refresh, old shares are invalidated.
|
|
This is a protocol property: the refreshed polynomial has the
|
|
same constant term (same secret) but different shares. -/
|
|
axiom share_refresh_correctness :
|
|
∀ (p : ThresholdParams) (_old_shares new_shares : List (Share p.n))
|
|
(aggPK msg : Nat),
|
|
new_shares.length ≥ p.t →
|
|
∃ (sig : SchnorrSig), schnorr_verify sig aggPK msg = true
|
|
|
|
end Crypto.FROST
|