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.
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.
The Signal Messenger recently introduced a new asynchronous key agreement protocol called PQXDH (Post-Quantum Extended Diffie-Hellman) that seeks to provide post-quantum forward secrecy, in addition to the authentication and confidentiality guarantees already provided by the previous X3DH (Extended Diffie-Hellman) protocol.More precisely, PQXDH seeks to protect the confidentiality of messages against harvest-now-decrypt-later attacks.In this work, we formally specify the PQXDH protocol and analyze its security using two formal verification tools, PROVERIF and CRYPTOVERIF.In particular, we ask whether PQXDH preserves the guarantees of X3DH, whether it provides post-quantum forward secrecy, and whether it can be securely deployed alongside X3DH.Our analysis identifies several flaws and potential vulnerabilities in the PQXDH specification, although these vulnerabilities are not exploitable in the Signal application, thanks to specific implementation choices which we describe in this paper.To prove the security of the current implementation, our analysis notably highlighted the need for an additional binding property of the KEM, which we formally define and prove for Kyber.We collaborated with the protocol designers to develop an updated protocol specification based on our findings, where each change was formally verified and validated with a security proof.This work identifies some pitfalls that the community should be aware of when upgrading protocols to be post-quantum secure.It also demonstrates the utility of using formal verification hand-in-hand with protocol design.
The Signal Protocol, underpinning secure messaging for billions, faces the challenge of migrating to a post-quantum world while preserving critical properties like asynchrony and deniability. While Signal’s PQXDH key exchange protocol addresses post-quantum confidentiality, full migration of the X3DH protocol remains elusive. Relying on a split KEM (K-Waay, USENIX ’24) offers a promising migration path, but it has so far suffered from size limitations compared to concurrent works leveragingring signatures. This work introduces Sparrow-KEM and Sym-Sparrow-KEM, novel asymmetric and symmetric split KEMs respectively, i.e. for which keys can be used interchangeably for sending and receiving, or only in one direction. They are designed to optimize the K-Waay protocol for size efficiency. Leveraging the MLWE assumption, these constructions reduce by a factor 5.1× the communication of prior post-quantum X3DH based on split KEMs, plus provides a 40× speedup. Additionally, Sym-Sparrow-KEM is the first symmetric split-KEM to offer deniability, IND-1KCA, and IND-1BatchCCA security, capturing implicit authentication properties. We provide formal security proofs for both schemes, including deniability. Our results demonstrate the feasibility of a compact and deniable post-quantum X3DH protocol based on split KEMs.
Classical cryptographic primitives such as RSA or Diffie-Hellman key exchange are based on computationally difficult mathematical problems for the solution of which no efficient algorithms are known. However, with the advent of practical quantum computers, quantum algorithms can be used to easily solve these problems and break the security of these algorithms. For this reason, post-quantum algorithms are being rapidly developed, evaluated, and optimized to resist quantum attacks in the hope that they will be used in secure instant messaging protocols such as the Signal protocol, in addition to other secure network protocols. This literature review provides an overview of efforts to develop quantum-resistant primitives for secure instant messaging protocols, with a particular focus on the Signal protocol.
Modern instant messaging systems require end-to-end (E2E) security guarantees while operating over server-mediated infrastructures that cannot be fully trusted. At the same time, the impending transition to post-quantum cryptography raises nontrivial challenges for the design of secure messaging protocols that preserve these guarantees. In this work, we present the design of a post-quantum end-to-end secure protocol for instant messaging applications under an untrusted relay model. The proposed construction relies on lattice-based primitives standardized by NIST, namely ML-KEM for key establishment and ML-DSA for authentication, and follows a Double-KEM pattern combined with explicit context binding to derive an E2E session key known only to the communicating clients. The server acts solely as an authenticated relay and never gains access to plaintext messages or session keys. In addition to the protocol design, we complement the protocol description with an automated symbolic verification using ProVerif, establishing injective mutual authentication and session-key secrecy under a Dolev–Yao adversary model. Finally, we characterize the computational cost of different authentication and verification policies and evaluate the performance of the handshake on heterogeneous cloud-based architectures. The results provide practical insight into the feasibility of deploying post-quantum end-to-end secure protocols within existing instant messaging infrastructures.
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.
The Signal protocol and its X3DH key exchange core are regularly used by billions of people in applications like WhatsApp but are unfortunately not quantum-secure. Thus, designing an efficient and post-quantum secure X3DH alternative is paramount. Notably, X3DH supports asynchronicity, as parties can immediately derive keys after uploading them to a central server, and deniability, allowing parties to plausibly deny having completed key exchange. To satisfy these constraints, existing post-quantum X3DH proposals use ring signatures (or equivalently a form of designated-verifier signatures) to provide authentication without compromising deniability as regular signatures would. Existing ring signature schemes, however, have some drawbacks. Notably, they are not generally proven secure in the quantum random oracle model (QROM) and so the quantum security of parameters that are proposed is unclear and likely weaker than claimed. In addition, they are generally slower than standard primitives like KEMs. In this work, we propose an efficient, deniable and post-quantum X3DH-like protocol that we call K-Waay, that does not rely on ring signatures. At its core, K-Waay uses a split-KEM, a primitive introduced by Brendel et al. [SAC 2020], to provide Diffie-Hellman-like implicit authentication and secrecy guarantees. Along the way, we revisit the formalism of Brendel et al. and identify that additional security properties are required to prove a split-KEM-based protocol secure. We instantiate split-KEM by building a protocol based on the Frodo key exchange protocol relying on the plain LWE assumption: our proofs might be of independent interest as we show it satisfies our novel unforgeability and deniability security notions. Finally, we complement our theoretical results by thoroughly benchmarking both K-Waay and existing X3DH protocols. Our results show even when using plain LWE and a conservative choice of parameters that K-Waay is significantly faster than previous work.