A Formal Analysis of Apple's iMessage PQ3 Protocol
summary
Formal verification of Apple's iMessage PQ3 models its hybrid ECC+KEM ratchet, proves post-quantum, post-compromise security plus secrecy, forward secrecy, authentication and injective agreement (replay protection), and refines the protocol spec. Proofs are machine-checked in the TAMARIN prover, handle unbounded ratchet loops, and encode a quantum-capable adversary. The effort requires 32 auxiliary lemmas, about two days of checking and ~140 GB memory, and produces no counterexamples so the formal claims hold under the modeled assumptions.
AI-written summary · about
chapters (9)
- 0:00iMessage PQ3 analysis intro
- 1:34Security guarantees and adversary
- 3:00Hybrid cryptography and key derivation
- 4:24Concrete key schedule example
- 6:12Formal verification with Tamarin
- 9:04Proving secrecy and forward secrecy
- 12:37Quantum attacker modeling
- 13:19Proof complexity and methodology
- 14:00Results and conclusion
related talks
29mDancing on the Lip of the Volcano: Chosen Ciphertext Attacks on Apple iMessage
56mSecrets of the Ratchets
28mQuantum Proofing Sigstore: A Tale of Three Approaches
42mSecurity of Push Messaging
31mMachine-checking post-quantum cryptography
32mSymmetric Key Exchange: Lightweight Alternatives for a Post-Quantum IoT
40mEnd-to-end encryption: Behind the scenes
24mA Framework for Post-Quantum Succinct Arguments