A Formal Analysis of Apple’s iMessage PQ3 Protocol

  • Felix Linker, ETH Zurich

We present the formal verification of Apple’s iMessage PQ3, a highly performant, device-to-device messaging protocol offering strong security guarantees even against an adversary with quantum computing capabilities. PQ3 leverages Apple’s identity services together with a custom, post-quantum secure initialization phase and afterwards it employs a double ratchet construction in the style of Signal, extended to provide post-quantum, post-compromise security. We present a detailed formal model of PQ3, a precise specification of its fine-grained security properties, and machine-checked security proofs using the TAMARIN prover. Particularly novel is the integration of post-quantum secure key encapsulation into the relevant protocol phases and the detailed security claims along with their complete formal analysis. Our analysis covers both key ratchets, including unbounded loops, which was believed by some to be out of scope of symbolic provers like TAMARIN (it is not!)

Speaker bio

Felix Linker just completed his Doctoral defense at ETH Zurich, where he will continue as a postdoc to formally verify the DNS. During his Doctorate, he researched security protocol design and analysis, in particular, with automated protocol verification tools such as the Tamarin prover. He collaborated with the International Committee of the Red Cross, Apple, and the Freedom of the Press Foundation. He is also active at the IETF in the Digital Emblems and Key Transparency working groups.

Watch Next