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.
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.
Quantum Key Distribution (QKD) protocols provide information-theoretic security by using quantum mechanical principles. Yet QKD is fundamentally a hybrid protocol: its security depends on the correct integration of the quantum phase with classical post-processing. While ETSI and ITUT specifications standardize QKD architectures and interfaces, they evaluate protocol security in isolation, leaving cross-layer interactions as an underexplored attack surface. This paper introduces a formal verification framework that holistically models QKD protocols based on ETSI and ITUT QKD specifications. Our model is the first hybrid QKD protocol model that supports automated analysis of protocollevel security focusing on how classical operations influence the security guarantees provided by the quantum phase of the QKD protocol. We formalize a comprehensive symbolic model of QKD protocols, based on ETSI and ITU-T QKD specifications, in Tamarin, an automated protocol verifier. Applying this framework, we obtain formal evidence of three specification-level vulnerabilities in ETSI- and ITU-T-grounded protocol models under adversary Eve+: subverted entanglement injection, basis-deferred measurement, and message reflection. Each arises from a classical control-plane omission in the procedure text and is established under a symbolic abstraction rather than as a claim about all practical deployments. We introduce two protocol improvements: measurement commitment and identitybound message authentication codes (MACs). Tamarin verification confirms that these countermeasures eliminate the identified vulnerabilities under Eve+. We have communicated our results and recommendations to relevant standardization organizations.
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.
The promise of unconditional security in the Quantum Key Distribution (QKD) depends on the availability of an authenticated classical channel. However, practical implementations often overlook this requirement or rely on computational assumptions that compromise long-term security. To overcome these challenges, this paper presents Entanglement-Based Authenticated Quantum Key Distribution (EAQKD), a novel protocol that addresses critical security and practical limitations in quantum cryptographic key exchange. Our approach integrates quantum entanglement distribution with information-theoretic authentication. We evaluate EAQKD's performance through a comprehensive discrete-event simulation framework modeled on realistic channel characteristics and experimental device parameters. Our modeling incorporates parameters from practical quantum optics setups, including SPDC entanglement sources, superconducting nanowire detectors, and fiber channel imperfections. Our results show quantum bit error rates consistently below the 11% security threshold (ranging from 1.86% at 10 km to 9.27% at 200 km), with secure key rates achieving 1.12×105 bits/s at short distances and maintaining practical rates of 9.8 bits/s at 200 km. When integrated with quantum repeater architectures, our analysis projects that EAQKD can extend secure communication beyond 500 km while providing information-theoretic security guarantees. Comparative analysis against the BB84, E91, and Twin-Field QKD protocols demonstrates EAQKD's superior balance of security, practical performance, and implementation robustness. This work advances quantum cryptography by providing a rigorously analyzed engineering reference for secure key distribution in future quantum communication networks.
Quantum Key Distribution (QKD) enables information-theoretically secure cryptographic key exchange by exploiting quantum mechanical properties -- photon polarisation, entanglement, and the no-cloning theorem -- to detect any eavesdropping attempt. Scaling QKD from point-to-point laboratory demonstrations to large-scale metropolitan and wide-area networks requires addressing three engineering challenges: photon loss over long fibre distances (limiting practical QKD to ~100-150 km without quantum repeaters), network topology design for multi-party key delivery, and integration of QKD with classical network infrastructure. This paper proposes the Quantum Key Distribution Network Architecture (QKDNA) framework, a systematic evaluation of five QKD protocol families (BB84, E91, MDI-QKD, Twin-Field QKD, and CV-QKD) across four network topology models (star, ring, mesh, and hierarchical trusted-node) on 16 real-world metropolitan network scenarios. QKDNA achieves maximum secure key rate of 18.4 Mbps (Twin-Field QKD, 80 km fibre, mesh topology) and demonstrates scalable QKD delivery to 48 simultaneous users. The framework contributes a Network QKD Deployment Index (NQDI) and quantitative guidance for national quantum network infrastructure planning.
Quantum Information Processing, which is an exciting area of research at the intersection of physics and computer science, has great potential for influencing the future development of information processing systems. The building of practical, general purpose Quantum Computers may be some years into the future. However, Quantum Communication and Quantum Cryptography are well developed. Commercial Quantum Key Distribution systems are easily available and several QKD networks have been built in various parts of the world. The security of the protocols used in these implementations rely on information-theoretic proofs, which may or may not reflect actual system behaviour. Moreover, testing of implementations cannot guarantee the absence of bugs and errors. This paper presents a novel framework for modelling and verifying quantum protocols and their implementations using the proof assistant Coq. We provide a Coq library for quantum bits (qubits), quantum gates, and quantum measurement. As a step towards verifying practical quantum communication and security protocols such as Quantum Key Distribution, we support multiple qubits, communication and entanglement. We illustrate these concepts by modelling the Quantum Teleportation Protocol, which communicates the state of an unknown quantum bit using only a classical channel.
Quantum protocols such as the BB84 Quantum Key Distribution protocol exchange qubits to achieve information-theoretic security guarantees. Many variants thereof were proposed, some of them being already deployed. Existing security proofs in that field are mostly tedious, error-prone pen-and-paper proofs of the core protocol only that rarely account for other crucial components such as authentication. This calls for formal and automated verification techniques that exhaustively explore all possible intruder behaviors and that scale well. The symbolic approach offers rigorous, mathematical frameworks and automated tools to analyze security protocols. Based on well-designed abstractions, it has allowed for large-scale formal analyses of real-life protocols such as TLS 1.3 and mobile telephony protocols. Hence a natural question is: Can we use this successful line of work to analyze quantum protocols? This paper proposes a first positive answer and motivates further research on this unexplored path.