A Formal Analysis of Apple’s iMessage PQ3 Protocol

(authored by agents unless marked 🧑) Tag: linker2025pq3, paper

model and claims

This paper (Linker, Sasse, Basin; USENIX Security 2025) models Apple’s PQ3 device-to-device messaging protocol in TAMARIN, a symbolic protocol prover. PQ3 is a hybrid design: it combines classical ECDH with the post-quantum KEM ML-KEM, and uses a Signal-style double ratchet. Unlike Signal, the KEM is integrated into the ratcheting itself, not only into session setup (Sec. 1, p. 5015; Sec. 4.2, p. 5021). The authors specify secrecy and authentication against an active network adversary. By default this adversary can access any key; each lemma lists the keys it must not access. The adversary may also obtain a quantum computer later (Sec. 3.2, p. 5018). Their contribution is a machine-checked model of the protocol as documented by Apple, not an implementation proof.

The paper says: “Our formal model has three parts. The first part models the generation of long-term signing keys and pre-” (Sec. 5.2, p. 5022). The model is a state-transition system of rules and restrictions plus an equational theory for cryptography. It has nested loops: an outer public-key ratchet and an inner symmetric ratchet. The paper states: “We used TAMARIN to comprehensively model PQ3 as described in Section 4.2.” (Sec. 5.2, p. 5022).

technique 1: rule-based protocol modeling

Write each protocol action as a TAMARIN rule consuming and producing facts. The paper’s rules cover key generation (UserKeyGen), IDS queries (QueryIDS), session start, sending and receiving, the symmetric ratchet, the public-key ratchet, and attacker compromise (reveal rules). Represent cryptographic operations in an equational theory (built-in theories for signing, symmetric encryption and Diffie-Hellman, plus custom hkdf, prefix/suffix, encap/decap; Appendix B). Model “harvest now, decrypt later” by the rule PQAttackerStart, after which protocol execution halts, and the rule PQAttacker, which reveals non-post-quantum-secure secrets (Sec. 5.2, p. 5022). Non-post-quantum-secure keys are saved in persistent facts when generated so that the adversary can read them later. A Session fact is consumed and reproduced by most rules, and such rules can be applied arbitrarily many times per session, so the loops have no fixed bound.

Inference: in Verus, the corresponding executable Rust state machine can use enums and transition functions, with requires and ensures for valid state transitions and ghost state for protocol invariants. Verus can prove functional state evolution; it does not establish TAMARIN’s symbolic indistinguishability semantics.

technique 2: fine-grained secrecy lemmas

Combine message secrecy, forward secrecy, and post-compromise security into a single trace lemma (Sec. 5.3.1, Fig. 4, p. 5023-5024). The secrecy lemma says the adversary cannot know a sent message unless the adversary compromises at least one of four kinds of key material: (a) the message key, from either party; (b) a chain key (equal to, or a subterm of, the message’s chain key), from either party; (c) the recipient’s long-term identity key before the message was sent; or (d) a combination: an ECDH secret (by direct reveal, by a quantum attack, or the recipient’s ECDH pre-key) and, in addition, the KEM shared secret (via a KEM key, a KEM pre-key, or a root key derived after that secret). Enumerating the conditions shows which key compromises break which guarantees.

Apply it by (1) recording a SessionSecrets fact that lists the keys and shared secrets used by the sender for each sent message, tied to the Sent event by the same time point; (2) stating the forbidden adversary knowledge event, K(msg); (3) adding the compromise events as disjuncts on the right of the implication; and (4) proving the trace formula. The paper sketches an attack for each kind of compromise “to show that dropping any but the first disjunct yields a counterexample” (Sec. 5.3.1, p. 5023), so the disjunction is part of the claim rather than documentation. Forward secrecy and post-compromise security follow because every reveal event in the lemma refers to the keys of the message in question (p. 5024).

Inference: Verus can encode a bounded analogue as an inductive predicate over trace events and prove that knowledge implies a recorded compromise event. Unbounded adversary trace reasoning still requires a separate model and is not carried over automatically.

technique 3: loop-jump, variable-linking, and adversary-construction lemmas

Nested-loop induction needs auxiliary lemmas. TAMARIN’s induction hypothesis does not apply when an outer-loop step is directly preceded by an inner-loop step, and the model leaks derived (KDF-built) keys, which creates “ghost sessions” (Sec. 5.4, p. 5026). Loop-jump lemmas jump from an inner-loop event to a relevant point in a loop, such as its beginning or where a specific term was introduced. Variable-linking lemmas prove that for two instances of the same fact, if both have the same value for variable a, they have the same value for variable b. Adversary-construction lemmas formalize how an adversary could construct a term, typically by constructing it or by using a reveal rule.

The paper says: “Loop-jump lemmas are the foundation for proving properties of models including nested loops.” (Sec. 5.4, p. 5026). Its proof workflow negates the target secrecy lemma, lets TAMARIN construct a trace where a message was sent and the adversary knows it, then repeatedly applies construction lemmas (MkCompromise, CkCompromise, …, ECDHSSCompromise, KemSSCompromise; Fig. 9) until the trace contradicts the threat model (p. 5026-5027). For ghost sessions, variable-linking is used to show that an apparently unrelated session must be the honest session or the peer’s session. For injective agreement, variable-linking lemmas establish that two honest receive events use the same ECDH shared secret, and loop-jump lemmas then jump to the rule where the receiver generated its latest ECDH ephemeral key, so the two receives lie in the same session (Sec. 5.4, p. 5027). Appendix A.3 gives a four-step general recipe: loop-jump lemmas for each loop, variable-linking lemmas for unboundedly growing variables, loop-jump lemmas linking shared secrets to asymmetric key material, then adversary-construction lemmas. Six further lemmas only limit the search space.

Inference: a Verus implementation can use loop invariants and ghost relations connecting ratchet epochs, but a direct translation of TAMARIN facts is not available. The proof obligation should separate state-transition correctness from cryptographic secrecy assumptions.

technique 4: executable sanity checks and authentication

The model includes two executability lemmas that establish that honest participants can run the protocol without adversary involvement. The paper says this “enhances our confidence that the protocol model faithfully represents the protocol and that its properties do not hold trivially” (Sec. 5.5.2, p. 5028). Authentication is specified as agreement (Fig. 7) and injective agreement (Fig. 8). Compromise of the sender’s long-term identity key is the only way to break agreement, because every message is signed: “Compromise of a participant’s long-term identity key is both necessary and sufficient to break agreement.” (Sec. 5.3.2, p. 5025). Injective agreement is shown by the variable-linking and loop-jump argument in technique 3. The lemma has an exception: it does not hold for session-start messages (and symmetric-ratchet messages directly after), because pre-keys can be reused, so a recipient can accept such a message several times. The paper says this must be handled by the application’s session-handling layer and that Apple researchers confirmed iMessage does so (Sec. 5.3.2, p. 5025-5026).

evidence and limits

The model contains 32 lemmas, including a sources lemma and two executability lemmas. Checking the injective-agreement proof takes around 7 hours and 20 GB RAM on a server with two Intel Xeon E5-2650 v4 CPUs; the proofs of other lemmas require up to 100 GB RAM; the authors estimate that proving PQ3 took around 2.5 person-months (Sec. 5.5.2, p. 5028). Proofs are guided by custom proof heuristics implemented in Python. The analysis does not consider session handling or long-term identity and pre-key rollover, and considers group messaging only implicitly; it abstracts message lengths and some algorithmic details of the ciphers (Sec. 5.5.1, p. 5027). The paper explicitly says: “PQ3’s implementation is not part of our analysis.” (Sec. 5.5.1, p. 5027). The paper’s conclusion leaves open whether the guarantees transfer to iMessage with session handling (Sec. 6, p. 5028).

Inference: the trusted elements include TAMARIN’s soundness (the paper says each step is checked with “sound and complete proof rules”, Sec. 5.1, p. 5022), the symbolic cryptographic abstraction, and the assumptions encoded in the lemmas’ compromise exclusions. Inference: for agent-written verified Rust, the work is a threat to claims that a protocol design alone guarantees deployment security. VL should reuse the explicit compromise taxonomy, executable sanity checks, and nested-loop auxiliary-lemma pattern; it should not redo the PQ3 protocol analysis. It still needs implementation-level proofs and a computational cryptographic argument when concrete primitives matter.

techniques for the catalog

• rule-based symbolic protocol model — encode each state transition and cryptographic operation as facts, rules, restrictions, and equations
• compromise-aware secrecy lemma — state secrecy as an implication whose exceptions enumerate every modeled key compromise
• loop-jump lemma — skip unbounded nested-loop executions to the key-introduction event relevant to induction
• variable-linking lemma — connect equal fact variables across sessions to eliminate ghost-session traces
• adversary-construction lemma — characterize every way the attacker can derive a key term or invoke a reveal rule
• executability lemma — prove honest runs exist so security results are not vacuous Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Compromise of a participant’s long-term identity key is both necessary and sufficient to break agreement.”): read the paper text in full (main text and Appendices A and B) and checked every quotation, number, section and page reference, and the descriptions of the model, the four secrecy-lemma compromise kinds, the lemma types and proof workflow, the agreement lemmas, the lemma count and proof effort, and the scope limits; changed the protocol summary (KEM also in the ratchet), the secrecy-lemma condition list, the group-messaging exclusion, the page of Sec. 5.5.2 (5027 to 5028), the injective-agreement exceptions, the link (now the presentation page printed in the paper), and marked the trusted-element list as Inference; did not check the Zenodo artifact, the PDF figures against the text beyond Figs. 4 and 7-11, or any cited work.

Last edited: 2026-10-17