Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging

Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging

Speakers: Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, Rolfe Schmidt

Conference: USENIX Security '24

YouTube: https://www.youtube.com/watch?v=Zg9WJlQnXoc

Overview

This talk details the collaborative effort between Signal Messenger and academic researchers to formally verify PQXDH, a post-quantum key agreement protocol designed to augment the widely used Signal Protocol. Presented by Rolfe Schmidt, an engineer at Signal Messenger, the presentation underscores the critical role of formal verification in securing real-world cryptographic protocols, particularly as the industry navigates the complexities of migrating to post-quantum cryptography (PQC). The core message is that even seemingly minor modifications to established protocols for post-quantum security can introduce subtle yet severe vulnerabilities, which formal methods are uniquely positioned to uncover and mitigate.

The significance of this work extends beyond the specific implementation of PQXDH. It serves as a practical case study demonstrating how formal verification can accelerate development, clarify security guarantees, and foster robust protocol design in an era of evolving cryptographic threats. By sharing their experience, the speakers highlight the pitfalls inherent in integrating new cryptographic primitives and advocate for an iterative, highly collaborative approach between protocol designers, implementers, and proof engineers to ensure the integrity of critical communication systems protecting billions of users worldwide.

Background

▶ Watch: Introduction to PQXDH verification and talk goals (0:00)

The Signal Protocol, celebrating its tenth anniversary, stands as a cornerstone of secure end-to-end messaging, protecting the communications of billions globally. Developed by Moxie Marlinspike and Trevor Perrin, it comprises two main components: the X3DH handshake for initial session establishment and the Double Ratchet protocol for continuous key agreement. Together, these mechanisms provide essential security guarantees, including forward secrecy, post-compromise security (PCS), mutual authentication, and a form of cryptographic deniability. The protocol's foundational cryptographic primitive for key agreement is Curve25519, an elliptic curve Diffie-Hellman (DH) exchange.

While robust against classical adversaries, the Signal Protocol, like many existing cryptographic systems, was not designed with post-quantum security in mind. The reliance on elliptic curve cryptography makes it vulnerable to attacks by sufficiently powerful quantum computers capable of solving the discrete logarithm problem. Recognizing this future threat, Signal Messenger embarked on a project to introduce Harvest Now Decrypt Later (HNDL) protection for its users. This modest, yet crucial, goal aimed to prevent an adversary who records today's encrypted traffic from decrypting it in the future once a quantum computer or other discrete log solver becomes available. It's important to note that this was not an attempt at full post-quantum security for the entire protocol, but rather a targeted enhancement to protect against future decryption of recorded messages.

To achieve HNDL, Signal developed PQXDH (Post-Quantum X3DH), a minimal extension to the existing X3DH handshake. The core idea behind PQXDH is to introduce a post-quantum secure Key Encapsulation Mechanism (PQ KEM) alongside the traditional Diffie-Hellman key exchanges. In practice, Signal chose Kyber Round 3 (now ML-KEM, a NIST standard) for its PQ KEM. The protocol involves three or four Diffie-Hellman key agreements combined with the encapsulation of a shared secret (SS) using the PQ KEM public key, resulting in a KEM ciphertext (CT_KEM). All derived Diffie-Hellman shared secrets and the KEM shared secret are then concatenated and fed into a Key Derivation Function (KDF) to produce the final session key (SK). Key distribution is handled by an untrusted key distribution server, from which Alex (initiator) retrieves Blake's (responder) keys. Crucially, two of Blake's keys – the signed prekey (SPK) and the PQ KEM public key (PQK) – are signed by Blake's identity key, providing an important authentication link. The first message from Alex to Blake includes all necessary public keys, the CT_KEM, metadata, and an initial message encrypted with SK, critically incorporating Associated Data (AD) formed by the concatenation of encoded identity and public keys.

Key Findings

▶ Watch: PQXDH protocol: Integrating post-quantum key encapsulation (3:10)

The formal verification process of PQXDH, undertaken in collaboration with external experts, revealed that even seemingly minor modifications to a protocol for post-quantum security can introduce significant and non-obvious vulnerabilities. Despite the initial appearance of robustness, the iterative analysis identified several critical issues in the initial specification and implementation.

Two primary attacks were discovered:

1. Theoretical Key Confusion Attack: The initial protocol specification lacked a mechanism for Alex (the initiator) to differentiate between Blake's signed elliptic curve prekey (SPK) and the PQ KEM public key (PQK). This theoretical flaw meant an attacker could potentially swap these two keys, forcing Alex to perform an insecure computation. While the concrete implementation included "key type bytes" in key encodings that would prevent this in practice, the specification itself was ambiguous, highlighting the need for explicit detail in formal models. This issue was resolved by refining the specification to include specific key identifiers and by restricting the ranges of key encodings.

1. KEM Re-encapsulation Attack: This was a more profound discovery, demonstrating that assuming only Chosen Ciphertext Attack (CCA) indistinguishability for the KEM was insufficient to prove the security of PQXDH. The attack, identified using ProVerif, revealed a scenario where an adversary could re-encapsulate a shared secret from one session into another. In a simplified version, if Alex initiates a session with Robbie, Robbie can obtain the shared secret (SS_KEM). Robbie could then initiate a separate session with Blake, take the SS_KEM from the Alex-Robbie session, and re-encapsulate it using Blake's uncompromised PQ KEM public key (PQ_PK_B). This results in two distinct sessions sharing the same short-term material, violating session independence. A more sophisticated version of this attack, detailed in the accompanying paper, showed that compromising even a single KEM key could break the Harvest Now Decrypt Later (HNDL) protection for all future uncompromised KEM keys for a party, thus undermining the core security goal of PQXDH.

The root cause of the re-encapsulation attack was the lack of binding between the KEM ciphertext and the specific KEM public key used for its encapsulation. The critical fix involved using the Associated Data (AD) field within the Authenticated Encryption with Associated Data (AEAD) ciphertext of the first message. By explicitly including the KEM public key (PQ_PK) in this Associated Data, the protocol ensures that the KEM ciphertext is cryptographically bound to the specific public key it was intended for, thereby preventing an adversary from transparently re-encapsulating shared secrets into different contexts.

These findings necessitated a new protocol revision, which refined cryptographic assumptions, specified key identifiers, restricted encoding ranges, and crucially, mandated the use of Associated Data with the KEM public key. With these revisions, PQXDH was successfully proven to meet its classical and post-quantum security goals in both symbolic and computational models using ProVerif and CryptVerif.

Furthermore, the analysis led to the definition of a new KEM property called Semus Collision Resistance (SHCR). While not a property that KEM designers are necessarily asked to target generally, SHCR was identified as the specific property required for PQXDH to prove its security. Importantly, Kyber Round 3 (now ML-KEM), the KEM chosen by Signal, was proven to satisfy SHCR, thus validating its suitability for PQXDH. This work also contributed to the broader understanding of KEM binding properties, comparing SHCR to other notions like Ciphertext Collision Resistance and the rich set of properties introduced in the "Keeping Up With The KEMs" literature.

Technical Deep Dive

▶ Watch: Key distribution, types, and signature dependencies (4:00)

The PQXDH protocol is designed as a minimal, yet significant, extension to the existing X3DH handshake, specifically targeting Harvest Now Decrypt Later (HNDL) protection. The core idea is to integrate a Post-Quantum Key Encapsulation Mechanism (PQ KEM) into the key agreement process without disrupting the established security guarantees of Diffie-Hellman (DH) exchanges.

The protocol begins with the initiator, Alex, retrieving Blake's public keys from an untrusted key distribution server. These keys include Blake's identity key (IK), a signed prekey (SPK), and crucially, a PQ KEM public key (PQK). In Signal's implementation, the elliptic curve keys (IK, SPK) are based on Curve25519, while the PQK utilizes Kyber Round 3 (which has since become ML-KEM in the NIST PQC standards). It's critical that both the SPK and PQK are signed by Blake's identity key, providing an initial layer of authentication.

Upon receiving Blake's keys, Alex performs several key agreement steps:

1. Multiple Diffie-Hellman (DH) Key Agreements: Typically three or four DH exchanges occur using Alex's ephemeral key and Blake's identity, signed prekey, and one-time prekey (if available). These generate several shared secrets.
2. KEM Encapsulation: Alex uses Blake's PQK to encapsulate a randomly generated shared secret (SS_KEM). This process produces a KEM ciphertext (CT_KEM), which Alex will send to Blake.
3. Key Derivation: All DH shared secrets and the KEM shared secret (SS_KEM) are concatenated and fed into a Key Derivation Function (KDF). This KDF outputs the final session key (SK), which will be used to protect the subsequent communication.

Alex then sends the necessary public keys (including Alex's ephemeral public key), the CT_KEM, any metadata, and an initial message to Blake. This initial message is an AEAD (Authenticated Encryption with Associated Data) ciphertext, encrypted with SK (or a key derived from SK). A crucial element here, identified and solidified during formal verification, is the use of Associated Data (AD). The AD for this initial message is the concatenation of encodings of the identity key public keys and, importantly, the PQ KEM public key (PQK) used by Alex for encapsulation. This binding mechanism is central to preventing the KEM re-encapsulation attack.

The formal verification of PQXDH employed two distinct but complementary tools:

• ProVerif: This tool operates in the symbolic model, where cryptographic primitives are assumed to be perfect. ProVerif is highly automated and can efficiently find attacks or prove security claims for protocols. Its prior application to the Signal Protocol and TLS 1.3 provided a strong foundation for this analysis.
• CryptVerif: Operating in the more rigorous computational model, CryptVerif provides machine-checked, game-hopping proofs, similar to traditional pen-and-paper proofs. While often requiring manual proof guidance, its recent extension for post-quantum soundness was essential for analyzing PQXDH's post-quantum guarantees.

The verification process involved modeling an arbitrary number of communicating agents, out-of-band identity key verification (mirroring Signal's safety number checks), the untrusted key distribution server, and a connection as a single encrypted message. The threat model considered a sophisticated adversary capable of leaking identity, ephemeral, one-time, and post-quantum keys at any time. Crucially, it accounted for a quantum adversary emerging with discrete log capabilities and the possibility of KEM security breaking down in the future.

The most significant technical finding was the KEM Re-encapsulation Attack. The attack hinges on the fact that if a KEM only guarantees Chosen Ciphertext Attack (CCA) security, it typically means an adversary cannot distinguish valid ciphertexts or recover the encapsulated secret without the private key. However, CCA security alone does not prevent an adversary from taking a legitimately generated KEM ciphertext and re-encapsulating the same shared secret using a different public key belonging to the same or another party.

Consider the simplified attack scenario:

1. Alex wants to communicate with Robbie. Alex encapsulates a shared secret (SS_KEM) using Robbie's PQK, generating CT_KEM, and sends it to Robbie. Robbie decapsulates CT_KEM to get SS_KEM.
2. Now, Robbie (who could be a malicious or compromised party) wants to initiate a session with Blake. Robbie obtains Blake's legitimate, uncompromised PQ KEM public key (PQ_PK_B).
3. Robbie then takes the SS_KEM he just received from Alex and re-encapsulates it using Blake's PQ_PK_B, creating a new ciphertext (CT_KEM'). Robbie sends this CT_KEM' to Blake.
4. Blake decapsulates CT_KEM' to get SS_KEM.

The result is that the session between Alex and Robbie, and the session between Robbie and Blake, now share the same short-term KEM shared secret. This breaks session independence and, in the more severe variant, undermines the HNDL protection by allowing an attacker to link or compromise future sessions based on a single compromised KEM key.

The solution implemented was to include the PQ KEM public key (PQK) itself in the Associated Data (AD) of the AEAD ciphertext of the first message. When Blake receives the initial message, he uses the AD to verify that the KEM ciphertext he decapsulates was indeed generated for his specific PQK. If an attacker attempts a re-encapsulation attack, the AD would either not match (if a different PQK was used) or would be forged (which AEAD prevents), thus failing the authentication check and preventing the attack.

This discovery led the authors to define Semus Collision Resistance (SHCR). SHCR is a property that ensures if two KEM ciphertexts encapsulate the same shared secret, then the public keys used for their encapsulation must be "semantically close" or identifiable as such. While KEM designers don't necessarily target SHCR, the verification showed that it's the property PQXDH needs for its security proof. Crucially, Kyber Round 3 was formally proven to satisfy SHCR using CryptVerif, confirming its suitability. This work also compared SHCR to other KEM binding properties in literature, noting its logical independence from Ciphertext Collision Resistance but an implication from a property in "Keeping Up With The KEMs."

The iterative and close collaboration between Signal's protocol designers and the proof engineers was instrumental. This rapid feedback loop allowed for quick identification of problems, specification refinements, and verification of fixes, significantly speeding up the development of a secure PQXDH protocol.

Demo / Proof of Concept

▶ Watch: Scope of the formal model for analysis (7:00)

While the talk did not feature a live demonstration of a Proof of Concept tool or a working exploit, the speakers detailed how their formal verification process, utilizing tools like ProVerif and CryptVerif, effectively served as a rigorous "proof of concept" for identifying vulnerabilities in the initial PQXDH specification. The identification of attacks, such as the KEM re-encapsulation attack, directly resulted from running these analysis tools against the protocol models. The outputs of these tools, whether an identified attack trace or a security proof, constituted the practical demonstration of their methodology's efficacy.

Defensive Implications

▶ Watch: Threat model including quantum adversary capabilities (7:50)

The experience with PQXDH offers critical defensive implications for protocol designers, implementers, and security researchers working on post-quantum migration. The overarching lesson is that the integration of post-quantum cryptographic primitives is far from trivial; simply "dropping in" new crypto can introduce subtle vulnerabilities that undermine the intended security goals.

For protocol designers, the key takeaway is the absolute necessity of formal verification when updating existing protocols or designing new ones, especially in the context of post-quantum transitions. The PQXDH case demonstrates that even a seemingly small addition, like a KEM for HNDL, can introduce complex attack vectors like re-encapsulation that are not apparent from informal reasoning or standard security notions like CCA security. Designers must consider KEM binding properties beyond basic CCA security, ensuring that KEM ciphertexts are inextricably linked to the specific public keys and contexts they are intended for.

Implementers should pay meticulous attention to the details of protocol specifications. Ambiguities, such as the lack of explicit key type identifiers in the initial PQXDH spec, can lead to theoretical vulnerabilities even if the implementation happens to sidestep them. The proper and consistent use of Associated Data (AD) in AEAD modes is a powerful defensive mechanism. As demonstrated with PQXDH, including critical contextual information—like the KEM public key—in the AD can effectively bind cryptographic operations to their intended parameters, preventing re-encapsulation or key confusion attacks.

Furthermore, the success of the PQXDH verification highlights the value of close collaboration between protocol designers, implementers, and formal verification experts. This interdisciplinary approach fosters a rapid iterative cycle of design, analysis, and refinement, leading to more robust and secure protocols. Organizations migrating to post-quantum cryptography should embed formal methods into their development lifecycle, recognizing it as an essential tool for identifying and mitigating new classes of vulnerabilities specific to the post-quantum landscape. The specific fix for PQXDH—including the PQ KEM public key in the Associated Data of the first message's AEAD ciphertext—is a concrete defensive strategy that other protocols using KEMs in similar contexts should consider.

Key Takeaways

• PQ Migration is Complex: Even "small" additions of post-quantum cryptography to existing protocols can introduce significant and non-obvious vulnerabilities.
• Formal Verification is Essential: Tools like ProVerif (symbolic model) and CryptVerif (computational model with post-quantum soundness) are powerful and practical for identifying pitfalls and clarifying security guarantees in real-world protocols.
• KEM Security Beyond CCA: Standard CCA security for Key Encapsulation Mechanisms may be insufficient in complex protocols. Specific KEM binding properties, such as Semus Collision Resistance (SHCR) defined by the authors, are crucial to prevent attacks like re-encapsulation.
• KEM Re-encapsulation is a Threat: Adversaries can exploit the lack of binding between KEM ciphertexts and their public keys to re-encapsulate shared secrets, leading to a loss of session independence and undermining Harvest Now Decrypt Later (HNDL) protection.
• Associated Data is Critical: Leveraging Associated Data (AD) in AEAD ciphertexts, for example, by including the KEM public key, is an effective defensive measure to cryptographically bind cryptographic operations to their specific contexts and prevent re-encapsulation attacks.
• Collaboration Accelerates Security: Close, iterative collaboration between protocol designers, implementers, and formal verification engineers is key to rapidly developing and deploying secure post-quantum protocols.

About the Speaker(s)

Rolfe Schmidt is an engineer at Signal Messenger, playing a key role in the development and implementation of the Signal Protocol. He presented the joint work on the formal verification of PQXDH, highlighting the practical application of these methods in securing real-world messaging systems. Karthikeyan Bhargavan, Charlie Jacomme, and Franziskus Kiefer are academic researchers who collaborated with Signal Messenger on the formal verification effort, bringing their expertise in formal methods and cryptographic analysis to the project.