Quantum key distribution provides secure communication by relying on physics principles and mathematical reasoning. Security proofs across the field can contain gaps, often between individually valid theorems integrated under mismatched assumptions. We produce an end-to-end security theorem formalized in the Lean proof assistant, eliminating hidden hypotheses by building only on Lean's standard axioms. Our proof covers composable security of the entanglement-based qubit BB84 protocol against coherent attacks by the postselection technique, accounting for finite block size, and is written in a language that enforces local operations and classical communication to help ensure a faithful representation of the protocol. The proof itself was enabled by LLM-based autoformalization, and with the proof complete, we used the same pipeline as a discovery machine, reducing the finite-size penalty on the key rate. Our work sets a reproducible standard for security arguments in quantum cryptography and shows how formal proof engines can accelerate discovery across quantum information science.
Quantum key distribution provides secure communication by relying on physics principles and mathematical reasoning. Security proofs across the field can contain gaps, often between individually valid theorems integrated under mismatched assumptions. We produce an end-to-end security theorem formalized in the Lean proof assistant, eliminating hidden hypotheses by building only on Lean's standard axioms. Our proof covers composable security of the entanglement-based qubit BB84 protocol against coherent attacks by the postselection technique, accounting for finite block size, and is written in a language that enforces local operations and classical communication to help ensure a faithful representation of the protocol. The proof itself was enabled by LLM-based autoformalization, and with the proof complete, we used the same pipeline as a discovery machine, reducing the finite-size penalty on the key rate. Our work sets a reproducible standard for security arguments in quantum cryptography and shows how formal proof engines can accelerate discovery across quantum information science.
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.
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.
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.
Quantum cryptography is an emerging field that ensures secure communication by leveraging principles of quantum mechanics. Unlike classical cryptography methods that rely on mathematical complexity, quantum cryptographic protocols, Quantum Key Distribution (QKD) protocols derive their security from the fundamental laws of physics. Among these, the BB84 protocol is widely recognized for enabling secure key exchange between communicating parties, with any eavesdropping attempts being inherently detectable. The invention of quantum computing poses a significant threat to classical encryption algorithms, and thereby necessitating both post-quantum cryptography and quantum-based approaches. This paper presents a comprehensive overview of quantum cryptography, emphasizing its theoretical principles foundations of quantum cryptography, emphasizing its advantages over traditional encryption methods, implementation challenges, and real-world application. It also outlines the limitations of quantum technology, e.g., hardware limitations and interference by noise, which restrict large-scale application. A detailed comparison between classical, quantum, and hybrid cryptographic approaches is presented to highlight the key advancement, including improved eavesdropping detection, enhanced key generation rates, and security through quantum entanglement. As quantum networks evolve rapidly, quantum cryptography is poised to become a cornerstone of nextgeneration ultra-secure communication systems.
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.
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.