FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq
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.
Related
- Generalised Bit-Vector Abstractions for Formal Verification of Quantum Error-Detection and Entanglement Circuits over {H,X,C-NOT}: CSS Constructions, Soundness, and Mutation-Based Validation
- Security of quantum key distribution with passive basis choice and detection-efficiency mismatch for a realistic satellite setup
- Security framework for practical quantum key distribution with imperfect devices
- Numerical security analysis for practical quantum key distribution
- Fully integrated continuous-variable quantum key distribution with composable security over 100 km
BibTeX
@misc{deng2026fvqkd,
title = {{FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq}},
author = {Ruixuan Deng and Zhengfeng Ji and Jiayu Zhang and Li Zhou},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.30645},
eprint = {2610.30645},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.30645},
}
RIS
TY - UNPB
TI - FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq
AU - Ruixuan Deng
AU - Zhengfeng Ji
AU - Jiayu Zhang
AU - Li Zhou
PY - 2026
DA - 2026/10/27
PB - arXiv
DO - 10.48550/arxiv.2610.30645
UR - https://arxiv.org/abs/2610.30645
AB - 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.
ER -