mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekayandHanzo Dev
2dd030dd98
Each of these made the corpus unsound: from a false axiom every theorem in
it follows, so the 756 stated results meant nothing while they stood.
Crypto/Magnetar.lean carried two axioms of the shape
∀ (oracle : Nat → Nat), ∃ (x : Nat), oracle x ≠ x
which the identity function refutes, yielding `∃ x, x ≠ x`. Both were roots
of `lean_lib Crypto`, so both compiled. Neither had a user. Family
disjointness quantifies over adversaries and advantages; `Nat → Nat` cannot
state it, so it is prose until the advantage model exists.
Protocol/Handshake.lean defined the session KDF as integer addition and then
axiomatised that distinct transcripts give distinct keys. ⟨1,1,1⟩ and ⟨1,0,2⟩
both derive 3 with transcripts 1 ≠ 2. `deriveSessionKey` is now opaque, which
is what a hash is in a model, and collision resistance is the one assumed
property. `transcript_binding` followed from unfolding the addition; it now
follows from the assumption.
Consensus/Safety.lean `unique_threshold` counts `honestPreferring` over
`Finset.univ` — the whole validator set, not the k-sample — so it needs
`2 * alpha > n`. Legal counterexample without it: n = 1000, f = 100, k = 20,
alpha = 14, with 900 honest nodes split 450/450, satisfies every hypothesis
and concludes v1 = v2. The hypothesis is now stated and threaded through
`theorem safety`, which makes the real limitation visible in the type: with
alpha ≤ k ≤ n it forces sampling more than half the network every round. In
the sub-sampled regime the protocol runs, safety is probabilistic and no
theorem of this shape holds. Consensus.ThresholdProof already proves the
pigeonhole under exactly this hypothesis.
strict-e2e-pq cited ePrint 2024/1113 as "Corona: A Lattice-Based Threshold
Signature for Post-Quantum Consensus" with no authors. That paper is
Ringtail, by Boschini, Kaviani, Lai, Malavolta, Takahashi and Tibouchi.
Corona is our implementation of it. Restored their title and their names.
Verified with a local lake build over every library.
Co-authored-by: Hanzo Dev <[email protected]>
80 lines
2.7 KiB
Lean4
80 lines
2.7 KiB
Lean4
/-
|
||
Post-Quantum Key Exchange Handshake
|
||
|
||
Hybrid key exchange: X25519 + ML-KEM-768.
|
||
Both classical and post-quantum key exchange in parallel.
|
||
Session key derived from both shared secrets.
|
||
|
||
Maps to:
|
||
- lux/node: peer-to-peer connection setup
|
||
- lux/crypto: hybrid KEM
|
||
- HIP-0005: PQ security for AI infrastructure
|
||
|
||
Properties:
|
||
- Hybrid: both X25519 AND ML-KEM must succeed
|
||
- Forward secrecy: ephemeral keys per session
|
||
- Transcript binding: session key binds full handshake
|
||
- Quantum safe: ML-KEM protects if X25519 breaks
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Tactic
|
||
|
||
namespace Protocol.Handshake
|
||
|
||
/-- Handshake state machine -/
|
||
inductive State where
|
||
| initial
|
||
| sentHello (ephPK : Nat)
|
||
| receivedHello (sharedSecret : Nat)
|
||
| established (sessionKey : Nat)
|
||
| failed (reason : String)
|
||
deriving Repr
|
||
|
||
/-- Key exchange components -/
|
||
structure KeyExchange where
|
||
x25519SS : Nat -- X25519 shared secret
|
||
mlkemSS : Nat -- ML-KEM-768 shared secret
|
||
transcriptHash : Nat -- hash of full handshake transcript
|
||
|
||
/-- HKDF over both shared secrets and the transcript.
|
||
Opaque: a KDF is a hash, and its only modelled property is the
|
||
collision resistance assumed below. Any concrete definition here is a
|
||
different function with different properties — as `+` was, which made
|
||
`forward_secrecy` false by ⟨1,1,1⟩ and ⟨1,0,2⟩ colliding at 3. -/
|
||
opaque deriveSessionKey (kex : KeyExchange) : Nat
|
||
|
||
/-- FORWARD SECRECY: Each session uses fresh ephemeral keys.
|
||
Compromising long-term keys doesn't reveal past sessions. -/
|
||
axiom forward_secrecy :
|
||
∀ (session1 session2 : KeyExchange),
|
||
session1.transcriptHash ≠ session2.transcriptHash →
|
||
deriveSessionKey session1 ≠ deriveSessionKey session2
|
||
|
||
/-- TRANSCRIPT BINDING: Session key commits to full handshake -/
|
||
theorem transcript_binding (kex1 kex2 : KeyExchange)
|
||
(h : kex1.transcriptHash ≠ kex2.transcriptHash)
|
||
(h_same_key : deriveSessionKey kex1 = deriveSessionKey kex2) :
|
||
kex1.x25519SS + kex1.mlkemSS ≠ kex2.x25519SS + kex2.mlkemSS ∨
|
||
kex1.transcriptHash = kex2.transcriptHash :=
|
||
-- Distinct transcripts give distinct keys, so the hypotheses cannot both
|
||
-- hold. Previously this unfolded the KDF and closed the goal by `omega`,
|
||
-- which proved a fact about addition rather than about a hash.
|
||
absurd h_same_key (forward_secrecy kex1 kex2 h)
|
||
|
||
/-- FAILED IS TERMINAL -/
|
||
theorem failed_terminal (reason : String) :
|
||
State.failed reason = State.failed reason := rfl
|
||
|
||
/-- ESTABLISHED HAS KEY -/
|
||
def sessionKey : State → Option Nat
|
||
| .established k => some k
|
||
| _ => none
|
||
|
||
theorem initial_no_key : sessionKey .initial = none := rfl
|
||
|
||
theorem established_has_key (k : Nat) :
|
||
sessionKey (.established k) = some k := rfl
|
||
|
||
end Protocol.Handshake
|