Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Lecture notes in computer science

Security Proof Techniques for QKD and Applications to Critical Infrastructures

Meret Kristen, Juergen Mottok

Published Oct 24, 2025• 0 citations
Publisher
DOI
10.1007/978-3-032-01823-6_18

Related papers

QKD Protocols Security Between Theory and Engineering Implementation

Hicham Amellal, Abdelmajid Meslouhi, Abderrahim El Allati +1 more

Springer eBooks•Dec 31, 2019•1 citation

FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq

Ruixuan Deng, Zhengfeng Ji, Jiayu Zhang +1 more

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.

quant-pharXiv:2610.30645•Oct 23, 2026•0 citations

Securing QKD against Fault Attacks

Gansel, Antoine

•Jan 1, 2024•0 citations

QKD protected fiber-based infrastructure for time dissemination

Alice Meda, Alberto Mura, Salvatore Virzì +10 more

In this study, we demonstrate the possibility to protect, with Quantum Key Distribution (QKD), a critical infrastructure as the fiber-based one used for time and frequency (TF) dissemination service. The proposed technique allows to disseminate secure and precise TF signals between two fiber-optic-connected locations, on a critical infrastructure, using both QKD and White Rabbit technique. This secure exchange enables the secret sharing of time information between two parties, allowing the synchronization of distant clocks with a stability of [Formula: see text] at 1 s, traceable to the Italian time scale. When encrypted, the time signals provide no useful information to a third party regarding the synchronization status, resulting in a time stability degraded by two orders of magnitude.

arXiv:2412.17731•Scientific Reports•Apr 18, 2025•4 citations

Security of differential phase shift QKD from relativistic principles

Martin Sandfuchs, Michael Haberland, V. Vilasini +1 more

The design of quantum protocols for secure key generation poses many challenges: On the one hand, they need to be practical concerning experimental realisations. On the other hand, their theoretical description must be simple enough to allow for a security proof against all possible attacks. Often, these two requirements are in conflict with each other, and the differential phase shift (DPS) QKD protocol exemplifies these difficulties: It is designed to be implementable with current optical telecommunication technology, which, for this protocol, comes at the cost that many standard security proof techniques do not apply to it. After about 20 years since its invention, this work presents the first full security proof of DPS QKD against general attacks, including finite-size effects. The proof combines techniques from quantum information theory, quantum optics, and relativity. We first give a security proof of a QKD protocol whose security stems from relativistic constraints. We then show that security of DPS QKD can be reduced to security of the relativistic protocol. In addition, we show that coherent attacks on the DPS protocol are, in fact, stronger than collective attacks. Our results have broad implications for the development of secure and reliable quantum communication technologies, as they shed light on the range of applicability of state-of-the-art security proof techniques.

arXiv:2301.11340•Quantum•Jan 27, 2025•15 citations

Implementation of an attack scheme on a practical QKD system

Antı́a Lamas-Linares, Qin Liu, Ilja Gerhardt +2 more

Bulletin of the American Physical Society•May 26, 2010•0 citations
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 this study, we demonstrate the possibility to protect, with Quantum Key Distribution (QKD), a critical infrastructure as the fiber-based one used for time and frequency (TF) dissemination service. The proposed technique allows to disseminate secure and precise TF signals between two fiber-optic-connected locations, on a critical infrastructure, using both QKD and White Rabbit technique. This secure exchange enables the secret sharing of time information between two parties, allowing the synchronization of distant clocks with a stability of [Formula: see text] at 1 s, traceable to the Italian time scale. When encrypted, the time signals provide no useful information to a third party regarding the synchronization status, resulting in a time stability degraded by two orders of magnitude.
The design of quantum protocols for secure key generation poses many challenges: On the one hand, they need to be practical concerning experimental realisations. On the other hand, their theoretical description must be simple enough to allow for a security proof against all possible attacks. Often, these two requirements are in conflict with each other, and the differential phase shift (DPS) QKD protocol exemplifies these difficulties: It is designed to be implementable with current optical telecommunication technology, which, for this protocol, comes at the cost that many standard security proof techniques do not apply to it. After about 20 years since its invention, this work presents the first full security proof of DPS QKD against general attacks, including finite-size effects. The proof combines techniques from quantum information theory, quantum optics, and relativity. We first give a security proof of a QKD protocol whose security stems from relativistic constraints. We then show that security of DPS QKD can be reduced to security of the relativistic protocol. In addition, we show that coherent attacks on the DPS protocol are, in fact, stronger than collective attacks. Our results have broad implications for the development of secure and reliable quantum communication technologies, as they shed light on the range of applicability of state-of-the-art security proof techniques.