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

Formal Verification of a Post-quantum Signal Protocol with Tamarin

Hugo Beguinet, Céline Chevalier, Thomas Ricosset, Hugo Senet

Published Dec 18, 2023• 3 citations
Publisher
DOI
10.1007/978-3-031-49737-7_8

Related papers

Formal Verification Techniques for Post-quantum Cryptography: A Systematic Review

Yuexi Xu, Zhenyuan Li, Naipeng Dong +3 more

Lecture notes in computer science•Sep 28, 2024•6 citations

Quantum Safety: How Do We Know? Formal Verification of Cryptographic Protocols

Ilias Cherkaoui

•Oct 27, 2026•0 citations

Formal verification of higher dimensional quantum communication protocols.

Ittoop Vergheese Puthoor

•Sep 26, 2024•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

Symbolic Formal Analysis of Quantum-Resistant Messaging Protocols Based on the Split KEM Mechanism

Katarina Boras, Ante Đerek

Quantum computers, growing only stronger with time, are threatening to break all asymmetric cryptography that is in use today. To mitigate such a devastating scenario, the cryptographic community is putting great effort into developing and evaluating quantum-resistant (post-quantum) primitives and protocols. An important part of the evaluation of such protocols is formal analysis using automated tools such as the Tamarin prover, used to formally prove security properties of a given protocol. Signal is an instant messaging protocol used by millions of people every day. In this paper, we use Tamarin to model and formally verify the security properties of Signal’s session-establishing subprotocol, X3DH, and two proposed post-quantum variants of X3DH, both based on a new notion of the split KEM mechanism. Using our new generic model for X3DH, we are able to construct and directly compare the security levels of the three protocols. We find that the protocols have differing levels of authentication and impersonation resistance; namely, the two proposed post-quantum solutions do not reach the levels of authentication of X3DH in the symbolic model. We discuss the reasons for this and offer solutions to mitigate the issue. We also explore and scrutinize the real-life consequences of these vulnerabilities.

IEEE Access•Jan 1, 2026•0 citations

Verification of Quantum Computation:An Overview of Existing Approaches

Alexandru Gheorghiu, Theodoros Kapourniotis, Elham Kashefi

Progress in mathematical physics•Jan 1, 2021•3 citations
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 computers, growing only stronger with time, are threatening to break all asymmetric cryptography that is in use today. To mitigate such a devastating scenario, the cryptographic community is putting great effort into developing and evaluating quantum-resistant (post-quantum) primitives and protocols. An important part of the evaluation of such protocols is formal analysis using automated tools such as the Tamarin prover, used to formally prove security properties of a given protocol. Signal is an instant messaging protocol used by millions of people every day. In this paper, we use Tamarin to model and formally verify the security properties of Signal’s session-establishing subprotocol, X3DH, and two proposed post-quantum variants of X3DH, both based on a new notion of the split KEM mechanism. Using our new generic model for X3DH, we are able to construct and directly compare the security levels of the three protocols. We find that the protocols have differing levels of authentication and impersonation resistance; namely, the two proposed post-quantum solutions do not reach the levels of authentication of X3DH in the symbolic model. We discuss the reasons for this and offer solutions to mitigate the issue. We also explore and scrutinize the real-life consequences of these vulnerabilities.