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) 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.
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.
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 integrating QKD into existing protocols like TLS remains challenging due to its fundamentally different operational model. In this paper, we propose a hybrid QKD-KEM protocol with two distinct integration approaches: a client-initiated flow compatible with both ETSI 004 and 014 specifications, and a server-initiated flow similar to existing work but limited to stateless ETSI 014 APIs. Unlike previous implementations, our work specifically addresses the integration of stateful QKD key exchange protocols (ETSI 004) which is essential for production QKD networks but has remained largely unexplored. By adapting OpenSSL’s provider infrastructure to accommodate QKD’s pre-distributed key model, we maintain compatibility with current TLS implementations while offering dual layers of security. Performance evaluations demonstrate the feasibility of our hybrid scheme with acceptable overhead, showing that robust security against quantum threats is achievable while addressing the unique requirements of different QKD API specifications.
Abstract: This study advances a unifying systems perspective on quantum-safe network security by synthesizing recent progress in quantum cryptography with practical integration patterns across carrier-grade infrastructures. Concept analysis distinguishes the roles of quantum key distribution (QKD), device-independent variants, quantum authentication, and post-quantum cryptography (PQC) within zero-trust architectures. Building on this, a layered framework—spanning physical/entanglement resources, key management, crypto-agility, control plane orchestration, and policy/compliance—is articulated to support end-to-end, composable guarantees. The problem addressed is the realization of verifiable, quantum-resilient security under operational constraints involving latency, key-rate variability, and heterogeneous trust assumptions. Methodology combines a structured literature synthesis with formal composability mapping to universal composability principles, adversarial threat modeling for quantum-enabled attackers, and testbed/simulation evaluation of hybrid QKD–PQC pipelines across L2–L3 segments and 5G/6G backhaul scenarios. Key results indicate that (i) selective QKD deployment on high-value links coupled with PQC at endpoints enhances resilience while preserving crypto-agility; (ii) automated key-lifecycle orchestration reduces exposure windows; and (iii) device-independent assurances strengthen guarantees where trust relaxation is necessary. The impact is a deployment-ready reference architecture, measurable integration metrics, and guidance aligned with emerging standards for critical infrastructure and national networks. The implications extend to procurement, compliance, and roadmap planning for quantum-era network security. Keywords: quantum-safe cryptography, quantum key distribution (QKD), post-quantum cryptography (PQC), hybrid QKD–PQC, composable security, device-independent QKD, zero-trust networks, key management and orchestration, 5G/6G backhaul, network security architecture, standards and interoperability
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) protocols achieve information-theoretic security, but their security proofs assume authenticated classical channels. All current ETSI QKD 014-compliant deployments authenticate these channels using classical TLS with RSA or ECDSA certificates — primitives vulnerable to quantum attack via Shor's algorithm. We prove (Theorem 2) that any production QKD deployment using RSA/ECDSA authentication will be retroactively compromised once quantum computers become available. This affects all major QKD vendors (Nokia, ID Quantique, Toshiba, QuantumCTek) and national quantum testbeds worldwide. We present the Post-Quantum Transport Gateway (PQTG), an open-source software gateway that replaces classical TLS on QKD control channels with NIST-standardized post-quantum cryptography (ML-KEM-768, Falcon-512, SPHINCS+-256f). PQTG requires no vendor firmware modifications. Security properties are formally verified with 549 machine-checked theorems in Lean 4. Open source: https://github.com/Paraxiom/pq-transport-gateway (MIT license)