A Formal Analysis of Apple's iMessage PQ3 Protocol
Felix Linker
34th USENIX Security Symposium (USENIX Security '25) · Day 2 · Crypto 3: Formal Methods and Private Computation
In 2024, Apple introduced iMessage PQ3, a significant evolution of its messaging protocol, heralded as the "new state-of-the-art in quantum secure messaging at scale." This talk, presented by Felix Linker, alongside his colleagues Ralph Zasa and David Basin, delves into a rigorous formal analysis of PQ3, aiming to verify Apple's ambitious security claims. The research utilizes the **Tamarin Prover**, a sophisticated protocol verifier, to ascertain whether iMessage PQ3 indeed delivers on its promises of secrecy, forward secrecy, post-compromise security, agreement, and replay protection against a formidable adversary, including one equipped with quantum computing capabilities.
AI review
Rigorous formal verification of a real-world, widely-deployed PQ messaging protocol using Tamarin — and the methodological contribution of making symbolic provers tractable for unbounded looping protocols is the actual headline. This is legitimate academic security research that advances both protocol assurance and formal methods tooling simultaneously.