Navigation
Search
|
A formal analysis of Apple’s iMessage PQ3 protocol
Saturday May 10, 2025. 12:42 AM , from OS News
We present the formal verification of Apple’s iMessage PQ3, a highly performant, device-to-device messaging protocol offering strong security guarantees even against an adversary with quantum computing capabilities. PQ3 leverages Apple’s identity services together with a custom, post-quantum secure initialization phase and afterwards it employs a double ratchet construction in the style of Signal, extended to provide post-quantum, post-compromise security.
We present a detailed formal model of PQ3, a precise specification of its fine-grained security properties, and machine-checked security proofs using the TAMARIN prover. Particularly novel is the integration of post-quantum secure key encapsulation into the relevant protocol phases and the detailed security claims along with their complete formal analysis. Our analysis covers both key ratchets, including unbounded loops, which was believed by some to be out of scope of symbolic provers like TAMARIN (it is not!). ↫ Felix Linker and Ralf Sasse Weekend, light reading, you know how this works by now. Light some candles, make some tea, get comfy.
https://www.osnews.com/story/142328/a-formal-analysis-of-apples-imessage-pq3-protocol/
Related News |
25 sources
Current Date
May, Sat 10 - 04:44 CEST
|