A Formal Analysis of Apple’s iMessage PQ3 Protocol

A detailed overview of the formal verification of Apple's iMessage PQ3 protocol using the Tamarin prover. The talk covers PQ3's hybrid cryptographic design, its post-quantum security goals like forward secrecy and post-compromise security, the powerful adversary model it resists, and the successful formal analysis of its unbounded double ratchet structure.