GLaDoS: Location-aware Denial-of-Service of Cellular Networks

A Formal Analysis of Apple's iMessage PQ3 Protocol

Authors: Felix Linker (ETH Zurich); Ralf Sasse (ETH Zurich); David Basin (ETH Zurich)

Conference: USENIX Security

YouTube: No public video available, based on peer-reviewed paper.

Overview

This article delves into the formal verification of Apple's iMessage PQ3 protocol, a cutting-edge device-to-device messaging protocol designed to offer robust security, even against adversaries equipped with future quantum computers. Authored by Felix Linker, Ralf Sasse, and David Basin from ETH Zurich, this research presents a detailed formal model of PQ3, specifies its fine-grained security properties, and provides machine-checked security proofs using the TAMARIN prover. The significance of this work lies in its rigorous validation of a widely deployed protocol used across billions of Apple devices, underpinning critical services like iMessage, FaceTime, HomeKit, and HomePod hand-off.

The core of PQ3's innovation stems from its hybrid cryptography approach, combining classical elliptic curve Diffie-Hellman (ECDH) primitives with post-quantum secure Module-Lattice-based Key Encapsulation Mechanisms (ML-KEM). This hybrid design ensures that the protocol's security does not solely rely on the nascent understanding of post-quantum primitives. Furthermore, PQ3 extends the widely adopted double ratchet construction, famously used in Signal, to provide enhanced post-quantum, post-compromise security (PQ-PCS) throughout its ratcheting phases, a significant improvement over prior protocols where post-quantum key encapsulation was typically limited to the initial setup.

A particularly novel aspect of this research is its demonstration that symbolic security protocol model checkers, specifically TAMARIN, are capable of verifying complex, real-world protocols featuring nested loops and unbounded runs. This challenges a previously held belief within the security community that such protocols were beyond the scope of symbolic provers without artificial restrictions. The authors not only provide a comprehensive analysis of PQ3 but also present a general methodology for tackling such intricate verification challenges, thereby advancing the state of the art in formal methods for protocol analysis.

Background

The landscape of secure instant messaging has evolved significantly over the past two decades. Early protocols like Off-the-Record Messaging (OTR) and later iterations such as Signal and iMessage have continually raised the bar for security guarantees. Modern messaging protocols are expected to maintain message secrecy and authenticity even against highly sophisticated adversaries, including nation-states, who are capable of compromising both messaging servers and end-user devices. This heightened threat model necessitated the development of advanced cryptographic constructions, such as ratcheting, which continuously generates new keys to limit the impact of key compromises.

Signal's double ratchet algorithm [32] pioneered a nested approach, combining an outer public-key ratchet with an inner symmetric-key ratchet. This mechanism ensures that symmetric encryption keys are updated with every message, while public-key ratchets allow recovery from past compromises on every round-trip. Crucially, this design provides forward secrecy (protecting past messages from future key compromise) and post-compromise security (allowing recovery from past compromises to secure future communication).

More recently, the advent of quantum computing has introduced a new and formidable threat: the "harvest now, decrypt later" adversary. Such an adversary can intercept and store encrypted communications today, intending to decrypt them in the future once sufficiently powerful quantum computers become available. This necessitates the integration of post-quantum cryptography (PQC). While protocols like PQXDH [24] (a post-quantum extension of Signal's X3DH key agreement protocol) introduced PQC into the initial key agreement phase, they typically did not extend post-quantum security into the subsequent ratcheting process. This meant that while initial session setup might be quantum-safe, the ongoing communication might still be vulnerable to a "harvest now, decrypt later" adversary if classical keys used in the ratchet were compromised.

Apple's PQ3 protocol addresses this gap by integrating post-quantum secure ML-KEM primitives not just into the initial setup but also into the public-key ratcheting phase. This fundamentally strengthens its post-compromise security against quantum adversaries. The formal analysis presented in this paper builds upon a rich history of protocol verification, comparing its symbolic approach (using TAMARIN) with computational proofs. While computational proofs offer detailed cryptographic assumptions and probabilistic security definitions, they are often complex, prone to human error in pen-and-paper arguments, and can be limited in handling complex protocols with unbounded interactions. Symbolic proofs, on the other hand, abstract away bit-string details, model messages as terms, and focus on possibilistic security definitions. They excel at machine-checked verification, handling unboundedly many participants and interleaved parallel sessions, and verifying fine-grained security properties, making them ideally suited for the comprehensive analysis of PQ3. This work directly contrasts with previous symbolic analyses of Signal, which were often limited to a fixed number of rounds or simplified protocol models, demonstrating the advancement in symbolic verification capabilities.

Key Findings

The formal analysis of Apple's iMessage PQ3 protocol by Linker, Sasse, and Basin yielded several critical findings and contributions:

• Machine-Checked Post-Quantum, Post-Compromise Security: The primary finding is the successful formalization and machine-checked verification of PQ3 using the TAMARIN prover. This rigorous analysis formally establishes that PQ3 provides strong post-quantum, post-compromise security (PQ-PCS) against a powerful active network adversary, including those with "harvest now, decrypt later" quantum computing capabilities. This provides a high degree of assurance for a protocol used across billions of devices.

• Pioneering Symbolic Verification of Complex Protocols: This work definitively demonstrates that symbolic security protocol model checkers, specifically TAMARIN, are capable of verifying substantial, real-world protocols featuring nested loops and unboundedly many parallel instances. This refutes a common belief that such complex structures were beyond the scope of symbolic provers, providing a novel methodology for future verification efforts.

• Fine-Grained Security Guarantees: The analysis provides a precise and fine-grained understanding of PQ3's security properties, detailing the exact implications of partial session state compromises on message secrecy and authenticity. The authors formulated a comprehensive secrecy lemma that captures message secrecy, forward secrecy, and post-compromise security simultaneously, explicitly listing which key compromises affect which guarantees.

• Hybrid Cryptography Effectiveness: The research formally confirms that PQ3's hybrid cryptography design (combining classical ECDH with post-quantum ML-KEM) means its security is at least as strong as using classical cryptography alone. Crucially, the repeated integration of KEM encapsulation into the ratcheting process is shown to strictly enhance the protocol's post-compromise security against "harvest now, decrypt later" adversaries.

• Identification of Session Handling Requirements: During the verification of injective agreement (replay protection), the authors identified a nuanced limitation: PQ3 cannot provide injective agreement for session-start messages due to the reuse of pre-keys. This finding highlights that the application's session-handling layer (e.g., iMessage's specific implementation) must actively address this case to ensure full replay protection, providing precise assumptions for secure deployment.

• Detailed Compromise Analysis: The study provides an exhaustive list of forward secrecy and post-compromise security guarantees for various key types under different adversary capabilities, including the scenario where a quantum computer breaks all non-ML-KEM keys. This granular insight is invaluable for guiding secure implementations and understanding the impact of potential key compromises.

Technical Deep Dive

Apple's iMessage PQ3 is architected as an asynchronous, device-to-device messaging protocol, allowing participants to exchange messages independently of their peer's online status. Its robust security framework is built upon a sophisticated interplay of key material, derivation mechanisms, and a hybrid double ratchet construction.

PQ3 Protocol Architecture

At its high level, PQ3 operates through a series of steps:

1. IDS Query: A client (e.g., Alice) queries Apple’s IDentity Services (IDS) for the recipient's (e.g., Bob's) pre-key material and long-term identity public key. The IDS is assumed to be secure, only distributing authentic public keys.
2. Initial Key Derivation: Alice derives an initial root key, chain key, and message key. She encrypts her first message and sends it with a signature and the necessary key material for Bob to derive the same keys.
3. Session Establishment: Bob verifies Alice's identity, uses the received material to derive his own initial root, chain, and message keys, and decrypts the message. A shared session is now established.
4. Symmetric Ratcheting: As long as the conversation direction remains unchanged (current sender keeps sending), both parties perform symmetric ratcheting. Each message uses a new message key derived from the current chain key, which is then ratcheted forward from the previous chain key. This provides per-message forward secrecy.
5. Public-Key Ratcheting: When the conversation direction changes (current receiver wants to reply), both parties perform public-key ratcheting. This involves using the old root key and newly sampled asymmetric key material (ephemeral ECDH and ML-KEM keys) to derive a new root key. This is crucial for post-compromise security.

Key Material and Derivation

PQ3 utilizes a diverse set of cryptographic keys:

• Long-term Identity Keys: P-256 ECDSA public/private key pairs used to authenticate messages and other key material. These are distributed and authenticated via the IDS and are critical for overall trust.
• Ephemeral Keys: Short-lived, session-specific ECDH and ML-KEM public/private key pairs.
• Pre-Keys: ECDH and ML-KEM public pre-keys uploaded to the IDS in timestamped bundles, signed with the long-term identity key. These enable asynchronous session initiation without the peer being online. PQ3 uses ML-KEM 768 for ephemeral KEM keys and ML-KEM 1024 for KEM pre-keys.
• Symmetric Keys: Message keys (for encryption), chain keys (derived from previous chain keys or root keys), and root keys (maintaining entropy from public-key ratchets).

Root and initial chain keys are derived from three entropy sources using a Key Derivation Function (KDF), specifically HKDF:

1. The session's previous root key (or a zero-byte sequence for the initial root key).
2. An ECDH shared secret, established by combining a peer's ECDH public key with one's own ECDH private key.
3. An optional KEM shared secret, established either by encapsulating it for the peer (using their KEM public key) or decapsulating it (using one's own KEM private key). The KEM shared secret is replaced with a zero-byte sequence when omitted.

This hybrid construction is paramount. All key derivations incorporating a KEM shared secret also involve classical secrets, ensuring that PQ3's security is at least as strong as using classical cryptography alone. The repeated use of KEM encapsulation in the public-key ratchet provides post-compromise security even against a "harvest now, decrypt later" adversary who manages to compromise some KEM shared secrets.

A custom heuristic determines when a client refreshes its KEM keys during public-key ratcheting. For example, as per iOS 17.4, PQ3 clients send a fresh KEM public key approximately every 50 messages or if no fresh KEM public key has been sent within a week.

Threat Model

The formal analysis considers a powerful active network adversary capable of reading, reordering, intercepting, replaying, and sending any message. This adversary also possesses a future quantum computer, enabling them to break all non-post-quantum-secure primitives (e.g., ECDH) after a specific point in time. This is modeled as a "harvest now, decrypt later" adversary: they store data now and decrypt it later. The model assumes strong randomness in devices and that, pre-quantum, classical primitives are secure. Crucially, the adversary can access any participant's key material by default, unless explicitly forbidden by a security lemma, allowing for a fine-grained analysis of compromise impact.

TAMARIN Model and Security Properties

The authors modeled PQ3 in its full complexity using TAMARIN, a state-of-the-art security protocol model checker operating in the symbolic model of cryptography. The model uses labeled multiset rewriting rules to represent protocol actions and adversary capabilities. Persistent facts store crucial information like generated keys.

Secrecy Lemma (Figure 4)

The core of the secrecy proof is a single, comprehensive TAMARIN lemma that combines message secrecy, forward secrecy, and post-compromise security. It states that a message msg sent at time t remains secret (i.e., not Ex #x. K(msg) @ x – the adversary does not know msg), unless the adversary achieves one of the following compromises:

1. Message Key Compromise: The adversary learns the specific message key used for encryption from either the sender or receiver (lines 5-7).
2. Chain Key Compromise: The adversary learns one of the chain keys used to derive the message key from either party (lines 6-7).
3. Recipient's Long-Term Identity Key Compromise: The adversary learns the recipient's long-term identity key before the message was sent (line 8). This allows the adversary to impersonate the recipient and carry out communication in their stead. This explicitly captures forward secrecy for identity keys.
4. Combined Asymmetric Key Compromise: The adversary compromises both the ephemeral ECDH secret key (or the ECDH pre-key if used for session initiation) and the KEM shared secret used to establish the root key for that message (lines 9-15).

• ECDH secret keys can be compromised directly (lines 10-11) or via a quantum computing attack after PQAttack() is initiated (line 9).
• KEM shared secrets can be compromised by revealing the KEM secret key used for encapsulation/decapsulation (lines 12-13) or by revealing a root key derived after that KEM shared secret was established (lines 14-15). This latter case, combined with a subsequent ECDH secret key compromise, allows the adversary to derive initial chain keys.

This lemma's structure precisely defines the conditions under which messages remain secret, establishing fine-grained forward secrecy and post-compromise security guarantees. For example, ML-KEM keys provide post-quantum forward secrecy and post-compromise security unconditionally, as do chain and message keys (with chain key PCS established upon the next public-key ratchet), even if a quantum computer breaks all non-ML-KEM keys. This resilience stems from their dependence on KEM-encapsulated secrets.

Agreement Lemmas (Figures 7 & 8)

Authentication in PQ3 relies on long-term identity keys to sign every message. The analysis formalizes agreement with two lemmas:

1. Agreement Lemma (Figure 7): If a participant receives a message m from s with counter i, then s must have previously sent m with counter i, unless s's long-term identity key was compromised.
2. Injective Agreement Lemma (Figure 8): For any two honest receive events of the same message m and authenticated data ad, these events must either be identical, or they were sent using the recipient's pre-key (rather than an ephemeral key), or one of the senders' identity keys was compromised. This lemma ensures replay protection. Crucially, the proof identified that PQ3 cannot provide injective agreement for session-start messages when pre-keys are reused, necessitating handling by the application's session-handling layer.

Proof Methodology

Verifying PQ3 presented two main challenges for TAMARIN:

1. Nested Loops: The protocol's nested loops (outer public-key ratchet, inner symmetric ratchet) cause non-termination if unrolled infinitely. TAMARIN's induction mechanism was employed, but required non-trivial auxiliary lemmas.
2. Synthetic Key Material: The leakage of derived ("synthetic") key material (e.g., from HKDF) and the presence of "ghost sessions" (unrelated sessions from which TAMARIN might incorrectly deduce key knowledge) complicated proofs.

To overcome these, the authors developed a methodology utilizing three types of auxiliary lemmas:

• Loop-Jump Lemmas: Allow skipping steps in a loop to jump to relevant points (e.g., loop beginning, term introduction).
• Variable-Linking Lemmas: Establish relationships between variables across different facts, linking derived keys (message to chain to root) and shared secrets to asymmetric key material.
• Adversary-Construction Lemmas: Formalize how an adversary could construct a term, often showing that it implies a direct contradiction to the threat model (e.g., a key reveal).

This intricate network of lemmas (depicted in Figures 9, 10, 11) guided TAMARIN's backwards search and constraint solving process, enabling the machine-checked verification of PQ3's complex properties. The methodology is a significant contribution to the broader field of formal methods.

Demo / Proof of Concept

As this article is based on a peer-reviewed conference paper rather than a live talk, there was no traditional "demo" in the sense of a live software demonstration. Instead, the "proof of concept" is the comprehensive formal model of PQ3 and its machine-checked security proofs using the TAMARIN prover.

The entirety of the formal models and proofs are openly accessible on Zenodo [25], serving as the verifiable artifact of their research. This includes the TAMARIN specification for PQ3, the adversary model, and the formal definitions of the security properties. The authors report a significant proof effort, with their TAMARIN model comprising 32 lemmas, including the auxiliary lemmas essential for handling nested loops and synthetic key material.

The process involved developing custom Python-based proof heuristics to guide TAMARIN, highlighting the complexity and interactive nature of such advanced formal verification. The computational resources required were substantial: checking the proof for the injective agreement lemma alone took approximately 7 hours and consumed 20 GB of RAM. Other lemmas demanded up to 100 GB of RAM. In total, the authors estimate the entire verification process for PQ3 required around 2.5 person-months of dedicated work, underscoring the depth and rigor of this formal analysis. This rigorous, machine-checked output provides the highest level of assurance regarding PQ3's security claims.

Defensive Implications

The formal analysis of Apple's iMessage PQ3 protocol offers several critical insights for defenders and protocol implementers:

• Protect Long-Term Identity Keys at All Costs: The research unequivocally highlights that the compromise of a participant's long-term identity key (e.g., P-256 ECDSA key) fundamentally impacts all security guarantees, including authenticity and, indirectly, secrecy. These keys are paramount for establishing trust and signing messages. Therefore, they must be stored with the highest level of protection, ideally within a device's Secure Enclave or equivalent hardware security module, where they are isolated from the main operating system and direct extraction.

• Robust Session Handling is Essential: The finding regarding injective agreement for session-start messages is a crucial takeaway. While PQ3 provides the cryptographic primitives for replay protection, the reuse of pre-keys means that the application's session-handling layer (e.g., in iMessage) must actively manage when to accept new session-start messages from devices with existing sessions. Defenders should ensure their application-layer logic is designed to prevent replays and maintain a one-to-one mapping of receive-events to send-events, especially during session initiation.

• Embrace Hybrid Cryptography for Post-Quantum Resilience: PQ3's successful integration of hybrid cryptography (classical ECDH alongside post-quantum ML-KEM) into its double ratchet construction provides a robust model for future secure messaging protocols. This approach ensures security even if either classical or post-quantum primitives are individually broken, effectively hedging against uncertainties in the long-term security of new PQC algorithms. Defenders should advocate for and implement similar hybrid approaches in systems requiring long-term confidentiality against quantum threats.

• Regular Key Rotation is a Cornerstone of Security: The protocol's reliance on symmetric ratcheting for per-message forward secrecy and public-key ratcheting for post-compromise security underscores the importance of continuous key rotation. Defenders should ensure that systems leveraging similar principles correctly implement key deletion policies and ratchet mechanisms to limit the window of exposure if a key is compromised. The specific heuristics for KEM key refreshing (e.g., every 50 messages or weekly in iOS 17.4) provide concrete examples of how to balance security with performance.

• "Harvest Now, Decrypt Later" is Mitigated by Design: PQ3's integration of post-quantum KEMs into the public-key ratchet directly counters the "harvest now, decrypt later" quantum threat. This means that even if an adversary captures encrypted traffic today and gains a quantum computer in the future, past session keys (derived with PQC) remain secure, preventing retroactive decryption. This design choice is a critical defensive posture against anticipated quantum capabilities.

• Fine-Grained Analysis Informs Implementation Security: The detailed breakdown of how specific key compromises impact different security properties (e.g., ECDH ephemeral key forward secrecy, ML-KEM key post-quantum forward secrecy) provides invaluable guidance for secure implementation. This granular understanding allows developers to prioritize the protection of certain key materials and design resilient systems that can gracefully handle partial compromises.

Key Takeaways

• PQ3 Achieves Strong Post-Quantum, Post-Compromise Security: Apple's iMessage PQ3 protocol provides robust security guarantees, including forward secrecy and post-compromise security, even against adversaries with future quantum computing capabilities ("harvest now, decrypt later" threat).
• Formal Verification Proves Complex Protocol Security: The research demonstrates that machine-checked security proofs using the TAMARIN prover can effectively verify complex, real-world protocols featuring nested loops and unbounded runs, advancing the capabilities of formal methods.
• Hybrid Cryptography is Key to Resilience: PQ3's design leverages hybrid cryptography, combining classical ECDH with post-quantum ML-KEM, ensuring its security does not solely depend on the maturity of new post-quantum primitives and strengthening its resilience against diverse threats.
• Identity Keys are Paramount for Trust: The long-term identity keys used for authentication are critical; their compromise undermines all security guarantees, emphasizing the need for their utmost protection, ideally in hardware Secure Enclaves.
• Session Handling Complements Protocol Security: While PQ3 provides strong cryptographic foundations, external factors like the application's session-handling layer must correctly manage issues such as pre-key reuse to ensure full injective agreement (replay protection).
• PQ3's Ratcheting Design is Quantum-Resistant: The continuous integration of post-quantum KEMs into the public-key ratcheting mechanism is a fundamental design choice that provides post-quantum post-compromise security, safeguarding ongoing communications against future quantum attacks.

About the Speaker(s)

The authors of this paper are Felix Linker, Ralf Sasse, and David Basin, all affiliated with ETH Zurich. Their work is a testament to their expertise in the field of cybersecurity, particularly in formal methods and the rigorous analysis and verification of cryptographic protocols. ETH Zurich is a renowned institution globally recognized for its cutting-edge research in science and technology, including information security and cryptography. Their collective contributions highlight a deep understanding of complex protocol design and the application of advanced tools like the TAMARIN prover to provide high assurance for critical real-world systems.