A Formal Analysis of Apple's iMessage PQ3 Protocol

Felix Linker, Ralf Sasse, David Basin

34th USENIX Security Symposium · Day 1

This article delves into the formal verification of Apple's **iMessage PQ3** protocol, a cutting-edge device-to-device messaging protocol designed to offer robust security, even against adversaries equipped with future quantum computers. Authored by Felix Linker, Ralf Sasse, and David Basin from ETH Zurich, this research presents a detailed formal model of PQ3, specifies its fine-grained security properties, and provides **machine-checked security proofs** using the **TAMARIN prover**. The significance of this work lies in its rigorous validation of a widely deployed protocol used across billions of Apple devices, underpinning critical services like iMessage, FaceTime, HomeKit, and HomePod hand-off.

AI review

This is the real deal — ETH Zurich formally verified Apple's production PQ3 protocol with TAMARIN and found it holds up. Machine-checked proofs of post-quantum post-compromise security on a protocol running on billions of devices. The methodology for handling nested loops in symbolic verification is a genuine contribution to the field.