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 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.
Many use messaging apps such as Signal to exercise their right to private communication. To cope with the advent of quantum computing, Signal employs a new initial handshake protocol called PQXDH for post-quantum confidentiality, yet keeps guarantees of authenticity and deniability classical. Compared to its predecessor X3DH, PQXDH includes a KEM encapsulation and a signature on the ephemeral key. In this work we show that PQXDH does not meet the same deniability guarantees as X3DH due to the signature on the ephemeral key. Our analysis relies on plaintext awareness of the KEM, which Signal's implementation of PQXDH does not provide. As for X3DH, both parties (initiator and responder) obtain different deniability guarantees due to the asymmetry of the protocol. For our analysis of PQXDH, we introduce a new model for deniability of key exchange that allows a more fine-grained analysis. Our deniability model picks up on the ideas of prior work and facilitates new combinations of deniability notions, such as deniability against malicious adversaries in the big brother model, i.e. where the distinguisher knows all secret keys. Our model may be of independent interest.
The Signal protocol relies on a handshake protocol, formerly X3DH and now PQXDH, to set up secure conversations. One of its privacy properties, of value to Signal, is , allowing users to deny participation in communications. Prior analyses of deniability for these protocols, including post-quantum variants, use models highly tailored to the individual protocols and generally make ad-hoc adaptations to "standard" AKE definitions, obscuring the concrete deniability guarantees and complicating comparisons across protocols.Building on Hashimoto, Katsumata, and Wigger's abstraction for Signal handshake protocols (USENIX'25), we address this gap by presenting a unified framework for analyzing their deniability. We analyze Signal's classically secure X3DH and harvest-now-decrypt-later-secure PQXDH, and show the settings for which PQXDH is (un)deniable against harvest-now--later attacks, where a quantum judge retrospectively assesses the participation of classical users. We further analyze post-quantum alternatives like RingXKEM, whose deniability relies on ring signatures (RS). By introducing a novel metric inspired by differential privacy, we provide relaxed, pragmatic guarantees for deniability. Lastly, we also use this metric to define for RS, a relaxation of anonymity, allowing us to build an efficient RS from NIST-standardized Falcon (and MAYO), which is not anonymous, but is provably deniable. We believe this relaxation to have independent interest outside of the Signal handshake protocol.
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 rapid development of quantum computers is emerging as a significant threat to end to end encryption protocols such as Signal. To address this issue, this paper enhances the Signal protocol by integrating Post Quantum Cryptography(PQC) algorithms. Specifically, this project integrates the PQXDH algorithm, which is the combination of X3DH and Kyber Key Encapsulation Mechanism to provide quantum resistant key exchange and encryption. A distinctive contribution of this work is the architectural shift from centralized client-server models to a fully decentralized peer-to-peer (P2P) communication model. This ensures greater resilience, fault tolerance, and preservation of privacy. To validate the feasibility of the proposed design, a real-world IoT use case is presented, highlighting the applicability of the system in resource-constrained environments where computational efficiency and low communication overhead are critical. The implementation is developed on Linux and leverages modern cryptographic libraries, ensuring compatibility with emerging PQC standards and integration into existing security infrastructures. Overall, this work demonstrates the combination of the E2E protocol Signal with quantum resistant Kyber to provide a quantum resistant cryptographic algorithm that can be used in decentralized architecture demonstrated using the IoT use case. The result is a robust, scalable, and future-proof framework for quantum-secure distributed communication.
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.
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.