Post-Quantum Secure Messaging: Signal, MLS, and iMessage PQ3#
USENIX Security '25 (34th USENIX Security Symposium) digest Program Adjacent pick 13–15 August 2025
Multiple papers/teams — see below — Adjacent
- Why: A cluster of formal-methods papers rigorously analyzing post-quantum secure-messaging protocols already in production (Signal's PQXDH, Apple's iMessage PQ3, IETF-standardized MLS) — the identity/crypto-agility theme from the Netflix Enigma talk playing out at the protocol-design layer.
- What:
Bundled Authenticated Key Exchange(AIST/PQShield) formally shows Signal's X3DH and PQXDH don't achieve "optimal" security under a new unified model, and introduces RingXKEM, a fully post-quantum handshake that does. A companion paper does the same for deniability guarantees specifically, building an efficient deniable ring-signature scheme from NIST-standardized Falcon. A third paper machine-verifies Apple's iMessage PQ3 protocol in the TAMARIN prover, including previously-thought-infeasible unbounded-loop ratchet analysis. A fourth explores more efficient post-quantum authentication modes for IETF-standardized MLS group messaging, trading some security for up to 75x lower post-quantum communication overhead. (from abstract only) - How: Formal/symbolic verification (TAMARIN) and unified concrete-security models applied to already-deployed or standardized PQ messaging handshakes, rather than proposing yet another new protocol from scratch. (from abstract only)
- Where applicable: General for anyone implementing or evaluating post-quantum secure messaging; directly relevant given Signal, Apple, and IETF (MLS) are all production deployments, not research prototypes.