Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
Hybrid Crypto QKD + PQ-KEM • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
Can we build a key establishment protocol that survives both quantum and classical attacks? Neither QKD alone (vulnerable to implementation side-channels) nor post-quantum KEMs alone (relying on unproven hardness assumptions) provide unconditional security. This project formalizes a UC composable hybrid combining both: security holds as long as at least one component remains unbroken — the “either breaks” property. References the X-Wing hybrid KEM and aligns with NIST FIPS 203.
Key Verified Results
either_breaksSecurity holds if QKD OR PQ-KEM is unbroken
EitherBreaks.lean
uc_realizes_idealHybrid protocol UC-realizes ideal key establishment
UCFramework.lean
simulator_soundnessSimulator indistinguishable from real execution
UCFramework.lean
composition_secureHybrid composes securely with arbitrary protocols
Composition.lean
Hybrid Protocol Architecture
| Component | Threat Model | Role in Hybrid |
|---|---|---|
| QKD | Information-theoretic | Unconditional key if channel is authentic |
| PQ-KEM | Computational (lattice) | Backup key if QKD channel compromised |
| Hybrid | Either-breaks | XOR of both keys: secure if either holds |