A Formal Analysis of Apple's iMessage PQ3 Protocol

Explore a comprehensive formal verification analysis of Apple's iMessage PQ3 protocol in this 16-minute conference presentation from USENIX Security '25. Discover how researchers from ETH Zurich conducted machine-checked security proofs using the TAMARIN prover to verify this post-quantum secure messaging protocol that provides strong security guarantees against quantum computing threats. Learn about PQ3's architecture, which combines Apple's identity services with a custom post-quantum secure initialization phase and employs an extended double ratchet construction similar to Signal's approach. Examine the detailed formal model presented by the researchers, including precise specifications of fine-grained security properties and the novel integration of post-quantum secure key encapsulation into relevant protocol phases. Understand how the analysis covers both key ratchets with unbounded loops, demonstrating capabilities previously thought to be beyond the scope of symbolic provers like TAMARIN, and gain insights into the protocol's post-quantum, post-compromise security features that ensure device-to-device messaging remains secure in a quantum computing era.