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

Formal verification of the ETSI proposal on a standard QKD protocol

Thomas Prévost, Bruno Martin, Olivier Alibart

Published Jan 1, 2024• 0 citations
Publisher

Abstract

This article presents a formal verification by ProVerif of the ETSI proposal to standardize the use of a quantum key distribution protocol.
DOI
10.13140/rg.2.2.23844.69767

Related papers

Vérification formelle de la proposition de l’ETSI sur un protocole de QKD

Thomas Prévost, Bruno Martin, Olivier Alibart

Cet article présente une vérification formelle par ProVerif de la proposition de l’ETSI (European Telecommunications Standards Institute) pour standardiser l’utilisation d’un protocole de distribution quantique de clé.

•May 15, 2024•0 citations

Standardization of quantum key distribution and the ETSI standardization initiative ISG-QKD

Thomas Länger, Gaby Lenhart

CV multi-domain quantum networks

New Journal of Physics•May 27, 2009•58 citations

Standardization of Quantum Key Distribution in ETSI

Walter Weigel, Gaby Lenhart

Wireless Personal Communications•Apr 8, 2011•7 citations

QKD standardization at ETSI

Gaby Lenhart

The present document starts with a brief introduction of ETSI, followed by an overview of locations where QKD has already been deployed commercially. The various scenarios of QKD deployment lead to a strong need for standardization. Before going into detail about the work of the ETSI standardization group for QKD the paper gives some general information of the importance of standards for the industry and describes the working methods of the ETSI ISG on QKD.

AIP conference proceedings•Jan 1, 2012•7 citations

A Secret Key Spreading Protocol for Extending ETSI Quantum Key Distribution

Thomas Prévost, Bruno Martin, Olivier Alibart

This paper presents an information theoretic secure secret key transfer protocol by Quantum Key Distribution (QKD) in the case of multi-hops quantum links between the two correspondents. We aim to transmit a secret between two parties using existing quantum infrastructure in the case where half of the intermediate routers are evil. We recursively divide the secret into Shamir’s shares, which are transmitted through different routes. This protocol has been successfully verified with ProVerif, which grants the secrecy of the transmitted key. We also propose an on-the-fly route discovery algorithm, in case the network is too large for each node to know all possible routes, and provide a formal verification of this algorithm using Maude.

International Conference on Information Systems Security and Privacy (ICISSP)•Jan 1, 2025•0 citations

Beyond the Quantum Promise: A Security Analysis of Classical Control in Quantum Key Distribution

Ali Hamza Malik, Raja Hasnain Anwar, Muhammad Taqi Raza

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.

quant-pharXiv:2608.07626•Aug 10, 2026•0 citations
This paper presents an information theoretic secure secret key transfer protocol by Quantum Key Distribution (QKD) in the case of multi-hops quantum links between the two correspondents. We aim to transmit a secret between two parties using existing quantum infrastructure in the case where half of the intermediate routers are evil. We recursively divide the secret into Shamir’s shares, which are transmitted through different routes. This protocol has been successfully verified with ProVerif, which grants the secrecy of the transmitted key. We also propose an on-the-fly route discovery algorithm, in case the network is too large for each node to know all possible routes, and provide a formal verification of this algorithm using Maude.
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.