A Formal Analysis of Apple’s iMessage PQ3 Protocol

In a 2024 release, Apple introduced the iMessage PQ3 protocol, aiming to set a new standard for quantum-secure messaging at scale. It is an end-to-end encrypted protocol with a robust set of security objectives.

Security Goals and Adversary Model

PQ3 is designed to achieve several key security guarantees:

• Secrecy: All messages exchanged between participants remain confidential.
• Forward Secrecy: If session secrets are compromised, messages exchanged before the compromise remain secure.
• Post-Compromise Security (PCS): Participants can recover secrecy and re-establish a secure channel after a compromise.
• Agreement and Replay Protection: Participants have a shared, accurate view of their conversation, and an adversary cannot resend old messages.

These guarantees are intended to hold against a powerful “harvest now, decrypt later” adversary. This adversary model assumes an attacker who:

1. Is an active network adversary, capable of intercepting, reordering, dropping, and injecting messages.
2. Possesses future quantum computing capabilities, allowing them to record current encrypted traffic and perform offline attacks later to break classical cryptography.
3. Can compromise various keys, with the formal proofs specifying which guarantees hold under which compromise scenarios.

Core Cryptography: A Hybrid Double Ratchet

To provide quantum resistance, iMessage PQ3 uses a hybrid cryptographic approach, combining the strengths of well-understood classical algorithms with modern post-quantum primitives.

• Classical Cryptography: Elliptic Curve Diffie-Hellman (ECDH), which is efficient and widely used.
• Post-Quantum Cryptography: Key Encapsulation Mechanisms (KEMs), which provide security against quantum computers but come with a higher bandwidth cost.

These primitives are integrated into a double ratchet construction, a mechanism popularized by the Signal protocol. The key innovation in PQ3 is the inclusion of a KEM within the ratchet, making it the first major protocol to do so and thereby enabling post-quantum post-compromise security.

The protocol’s key derivation schedule operates in two nested loops:

1. The Public Key Ratchet: This outer loop uses public-key cryptography (both ECDH and KEMs) to establish new shared secrets. It is activated whenever the direction of the conversation changes. To conserve bandwidth, the KEM is updated based on a heuristic (effectively, non-deterministically), while the ECDH exchange happens with each change in direction.
2. The Symmetric Ratchet: This inner loop uses a chain key from the public key ratchet to efficiently derive a unique encryption key for each individual message, along with a new chain key for the subsequent message from the same sender.

Formal Analysis with the Tamarin Prover

The research team conducted a formal verification of PQ3’s security claims using the Tamarin Prover, a tool for protocol analysis that operates in the symbolic model. This model abstracts cryptographic functions to their essential properties (e.g., decrypt(encrypt(m, k), k) = m), which allows for the analysis of large, complex systems.

A significant achievement of this work was overcoming a previously held belief that unbounded looping protocols like the double ratchet were “out of scope for symbolic provers.” The team successfully modeled and proved PQ3 secure without artificial restrictions, developing a general proof methodology for such protocols in the process.

The formal model was structured in three phases to accurately capture the threat model:

1. Setup: Participants generate keys and establish identities. Non-post-quantum secure key material is recorded on a conceptual transcript.
2. Protocol Execution: Participants exchange messages using the ratchet. Ephemeral classical keys are also added to the transcript.
3. Post-Quantum Phase: The model simulates the “decrypt later” scenario by allowing the adversary to access all the classical secret keys recorded on the transcript.

Verified Properties and Key Findings

The analysis successfully proved that iMessage PQ3 meets its security goals for secrecy (including forward secrecy and PCS), agreement, and replay protection. The core secrecy lemma is particularly insightful, formalizing that a message remains secret unless a specific combination of keys is compromised.

For a given message, its confidentiality is broken only if the adversary learns:

• The specific message encryption key itself.
• A chain key used to derive the message key.
• Both the ECDH shared secret and the KEM shared secret from the relevant public key ratchet step.
• The sender’s signing key (which would allow for impersonation).

This lemma demonstrates the hybrid security of the protocol. The quantum adversary can trivially compute the ECDH secret but cannot break the KEM secret. Therefore, to compromise the entire conversation, the adversary must repeatedly compromise the post-quantum KEM secrets, which is precisely the post-quantum post-compromise security guarantee PQ3 aims to provide.

Conclusion

The formal analysis found no attacks on iMessage PQ3. The collaboration resulted in formally specified security guarantees and minor refinements to the protocol specification. The project was a significant undertaking, requiring approximately 2.5 person-months of effort and 32 auxiliary lemmas. Most importantly, it serves as a powerful demonstration that the Tamarin Prover is capable of analyzing modern, complex, real-world security protocols with unbounded states, marking a notable advancement for the formal methods community.

• Tags:
• Feature
• IMessage
• PQ3
• Post-Quantum Cryptography
• Formal Verification
• Tamarin
• Security Protocol
• Double Ratchet
• Messaging