Formal verification proves quantum key distribution security end to end
FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq
Cryptography and SecurityLogic in Computer Science
Summary
Quantum key distribution (QKD) can securely share secret keys based on quantum physics, but its security proofs are very complex and usually checked by hand. The authors created a computer-checked system called FVQKD that rigorously verifies these proofs without skipping any details or assumptions. Their work includes fully verifying the widely used BB84 QKD protocol and finding missing parts in previous proofs. This makes the security claims more trustworthy by combining physics-based guarantees with machine-checked logic.
What this means in practice
- •For quantum communication engineers: Use FVQKD to obtain fully machine-checked security proofs for quantum key distribution protocols, ensuring correctness before deployment.
- •For cryptography software developers: Build reliable quantum cryptographic systems by leveraging FVQKD’s reusable quantum-information infrastructure to verify security properties of new protocols.
Authors
Ruixuan Deng, Zhengfeng Ji, Jiayu Zhang, Li Zhou
Abstract
Quantum key distribution (QKD), whose security is derived from quantum mechanics rather than computational assumptions, is moving into standardization and commercial deployment. Yet its security guarantees rest on technically delicate proofs checked by hand. Formal verification closes this gap, establishing a two-factor assurance: unconditional security from physical principles, and machine-checked proofs against reasoning errors. We present FVQKD, a Rocq library for machine-checking QKD security proofs. Its first result is a complete, end-to-end machine-checked proof of composable, finite-key security for BB84. The mechanization reconstructs the complete proof infrastructure from first principles, including the smooth entropy framework, the entropic uncertainty relation, and the Quantum Leftover Hash Lemma. It uncovers necessary side conditions that the published argument leaves unstated, one of which reveals a missing proof branch, and it grounds the information-theoretic bound in a formal semantics of protocol execution, which the pen-and-paper analysis lacks. The proof is entirely admit-free, relying only on the Rocq kernel and standard foundational axioms. To our knowledge, this is the first end-to-end formal verification of a QKD security proof. Built on MathComp, MathComp-Analysis, and CoqQ, the development provides quantum-information infrastructure designed for reuse across broader QKD variants and quantum cryptography applications.