iMessage PQ3: what two academic analyses say about its security

Short answer: PQ3 is the end-to-end encrypted messaging protocol Apple designed for iMessage, combining a post-quantum secure start-up phase with a Signal-style double ratchet. Two academic papers analyse it: one gives machine-checked proofs in the TAMARIN prover, the other a reductionist security analysis. Both are analyses of the protocol as specified, and neither is a guarantee about any particular product or device.

What is the core structure of the PQ3 protocol?

According to the authors of the papers, the iMessage PQ3 protocol is an end-to-end encrypted messaging protocol designed for exchanging data in long-lived sessions between two devices. It leverages Apple’s identity services together with a custom, post-quantum secure initialization phase. After this initial phase, the protocol employs a double ratchet construction in the style of Signal. This construction is extended to provide post-quantum, post-compromise security. The initial authenticated key exchange is constructed from digital signatures plus elliptic curve Diffie–Hellman and post-quantum key exchanges. To derive per-message keys on an ongoing basis, the protocol uses an adaptation of the Signal double ratchet that includes a post-quantum key encapsulation mechanism.

How do researchers verify the protocol’s security?

One 2024 paper presents a detailed formal model of PQ3, including a precise specification of its fine-grained security properties. They provide machine-checked security proofs using the TAMARIN prover. A particularly novel aspect of this work is the integration of post-quantum secure key encapsulation into the relevant protocol phases. The analysis covers both key ratchets, including unbounded loops. Some previously believed these unbounded loops were out of scope for symbolic provers like TAMARIN, but the formal verification shows they are within scope. That second paper gives a reductionist security analysis by adapting the multi-stage key exchange security analysis of Signal by Cohn-Gordon et al. A second paper gives the cryptographic details of the protocol.

What specific security properties does PQ3 guarantee?

According to the second paper, the protocol aims to provide classical and post-quantum confidentiality for forward secrecy and post-compromise secrecy, as well as classical authentication. The second paper's analysis says PQ3 provides confidentiality with forward secrecy and post-compromise security against both classical and quantum adversaries. These guarantees hold in both the initial key exchange and the subsequent messaging phases. The TAMARIN paper describes PQ3 as a highly performant, device-to-device protocol offering strong security guarantees even against an adversary with quantum computing capabilities. Those are the authors' claims about the protocol design, not about any ecosystem.

Why is the integration of key encapsulation significant?

The integration of post-quantum secure key encapsulation into the relevant protocol phases is identified as particularly novel in the formal analysis. The protocol uses an adaptation of the Signal double ratchet that includes a post-quantum key encapsulation mechanism to derive per-message keys on an ongoing basis. The authors say their formal model and detailed security claims cover this component.

FAQ

What is PQ3?

An end-to-end encrypted messaging protocol for long-lived sessions between two devices. It uses Apple's identity services with a custom post-quantum secure initialization, then a double ratchet in the style of Signal, extended for post-quantum, post-compromise security.

What did the 2024 TAMARIN paper do?

It presents a detailed formal model of PQ3, a specification of its security properties and machine-checked proofs using the TAMARIN prover. The authors say it covers both key ratchets, including unbounded loops that some believed out of scope for symbolic provers.

What did the second paper do?

It presents the cryptographic details and a reductionist security analysis, adapting the multi-stage key exchange analysis of Signal by Cohn-Gordon et al.

What does the second paper conclude?

That PQ3 provides confidentiality with forward secrecy and post-compromise security against both classical and quantum adversaries, in both the initial key exchange and the ongoing messaging phase.

Does this prove everything about iMessage?

No. The papers analyse the protocol design and its stated properties. They are not audits of any implementation.