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.
Comments
87 pages: 12 pages of main text, 4 pages of references, and 71 pages of appendices. Artifact: https://github.com/fvqkd/FVQKD
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.
In recent years, quantum key distribution (QKD) has evolved from a scientific research field to a commercially available security solution, supported by mathematically formulated security proofs. However, since the knowledge required for a full understanding of a security proof is scattered across numerous publications, it has proven difficult to gain a comprehensive understanding of all steps involved in the process and their limitations without considerable effort and attention to detail. Our paper aims to address this issue by providing a rigorous and comprehensive security proof for the finite-size 1-decoy and 2-decoy BB84 protocols against coherent attacks within Renner's entropic uncertainty relation framework. We resolve important technical flaws found in previous works regarding the fixed-length treatment of protocols and the careful handling of acceptance testing. To this end, we provide various technical arguments, including an analysis accounting for the important distinction of the 1-decoy protocol where statistics are computed after error correction, along with a slight improvement of the secure-key length. We also explicitly clarify the aspect of conditioning on events, addressing a technical detail often overlooked and essential for rigorous proofs. We extensively consolidate and unify concepts from many works, thoroughly discussing the underlying assumptions and resolving technical inconsistencies. Therefore, our contribution represents a significant advancement towards a broader and deeper understanding of QKD security proofs.
Quantum Key Distribution (QKD) promises information-theoretic security, yet practical implementations ranging from point-to-point links to large-scale networks can introduce protocol and architectural vulnerabilities that undermine this guarantee. We present a formal verification framework based on QTPi, a process calculus for distributed quantum systems, to model and verify QKD protocols at the Quantum Link Layer (QLL). Using BB84 as a case study, we specify concurrent processes for Alice, Bob, and supporting components, and formally check functional requirements defined within the Innovate UK project QAssure, such as key agreement (QLL-EM-1). Our approach integrates symbolic simulation and formal assertions to automatically verify that critical QLL properties hold across executions. This establishes a systematic methodology for providing assurance of QKD protocols in realistic settings and lays the foundation for future quantitative verification of probabilistic security guarantees, including resilience to eavesdropping and bounded key failure rates.
We present a rigorous and complete security proof of the decoy-state BB84 quantum key distribution (QKD) protocol. Our analysis aims to achieve a high standard of mathematical rigour and completeness, thereby providing the necessary foundation for certification and standardization efforts. Beyond establishing the security of a specific protocol, this work develops a general and modular framework that can be readily adapted to a broad class of QKD protocols, including both prepare-and-measure and entanglement-based variants. Our framework unifies all major ingredients required for the analysis of realistic QKD protocols, including the analysis of classical authentication and classical processing, source-replacement schemes, finite-size analysis, source maps, squashing maps, and decoy-state techniques. In doing so, this work consolidates a diverse range of techniques scattered across the QKD literature into a unified formalism, representing a general and rigorous treatment of QKD security. Finally, it outlines a clear path towards incorporating practical imperfections within the same framework, thereby laying the groundwork for addressing implementation security in future analysis.
This thesis is concerned with rigorous security analyses of practical Quantum Key Distribution (QKD) protocols, using a variety of modern proof techniques. The main results are as follows. First, we establish a security proof for variable-length QKD protocols against IID collective attacks, and extend this result to coherent attacks using the postselection technique. In doing so, we resolve a long-standing flaw in the application of the postselection technique to QKD, thereby placing it on a rigorous mathematical footing. Second, we develop a method to bound phase error rates in entropic uncertainty relation-based and phase error rate-based proofs, using only the observed statistics of the protocol, even when detectors are imperfect and only approximately characterized. This removes a key assumption of identical detector behaviour and enables these techniques to be applied in realistic settings. Third, we present a very general security analysis based on the marginal-constrained entropy accumulation theorem. The resulting framework can be readily adapted to practical imperfections and side channels, and is suitable for certification efforts. Finally, we show that the security of QKD protocols under realistic authentication assumptions can be reduced to the standard idealized setting, where authentication is assumed to behave honestly, with only minor protocol modifications. A distinctive feature of this thesis is its unified presentation of several major QKD security proof frameworks using consistent protocol descriptions and notation. Consequently, this thesis is intended not only as a collection of new technical results, but also as a useful reference for understanding rigorous security analysis in quantum key distribution.
Post-quantum cryptography (PQC) and quantum key distribution (QKD) address the quantum threat from opposite directions: PQC replaces vulnerable public-key algorithms with schemes believed to resist quantum cryptanalysis, while QKD derives keys whose secrecy rests on physical assumptions rather than computational ones. Because each approach has a distinct failure mode, a growing body of work combines them so that a session key remains secure if either component holds. We first establish the deployed baseline, hybrid classical-plus-PQC key exchange, against which QKD-augmented designs must be judged. We then propose a taxonomy of hybrid PQC-QKD designs along eight dimensions (integration layer, combiner construction, authentication scope and source, QKD topology, trusted entities, key-delivery interface, classical component, and evidence type), and use it to compare published protocols, including Muckle and its successors, MACsec and TLS integrations, and IKEv2 mechanisms standardised in RFCs 8784, 9370, and 9867. We examine key-combiner constructions in light of the KEM-combiner literature and of NIST, ETSI, and ITU-T guidance, and map the security arguments for hybrid PQC-QKD protocols onto a common grid of security model, assumptions, permitted compromise, established guarantee, and limitations. We synthesise deployment evidence from metropolitan and national QKD networks, distinguishing the few testbeds that have run PQC in the key path from pure-QKD deployments, and summarise the standards and policy landscape, including the positions of national security agencies that recommend against relying on QKD alone. We close with open problems: authentication of the QKD classical channel, shared-infrastructure threat models, device certification versus formal proofs, formal verification of hybrid handshakes, and the lack of peer-reviewed deployment economics.
In contrast to classical public-key cryptosystems, where the security of encoded messages relies on on computational assumptions, Quantum Key Distribution (QKD) enables two distant parties to establish a shared secret key that, when combined with a one-time pad, provides information-theoretically secure encryption, provided that the QKD protocol is supported by a rigorous security proof. In the last decades, security proofs robust against a wide range of eavesdropping strategies have established the theoretical soundness of several QKD protocols. However, most proofs are based on idealized models of the physical systems involved in such protocols and often include assumptions that are not satisfied in practical implementations. This mismatch creates a gap between theoretical security guarantees and actual experimental realizations, making QKD protocols vulnerable to attacks. To ensure the security of real-world QKD systems, it is therefore essential to account for imperfections in security analyses. In this article, we present an overview of recent analytical and numerical developments in QKD security proofs, which provide a versatile approach for incorporating imperfections and re-establishing the security of quantum communication protocols under realistic conditions.