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.
I’ll have to read it more carefully. I am glad independent researchers are around to do this sort of work. Although I think it should be clarified that they’re proving the mathematical strength of the crypto and not necessarily it’s implementation. Even unbroken crypto can have implementation weaknesses. Relying on a trusted directory service is one such weakness.
This problem isn’t unique to imessage. E2E clients try to solve this in different ways. One approach is to get the user to manually verify the encryption keys. For example SSH asks the user to verify the keys for the first time. GPG tries to encourage users to exchange keys in person or at least through personal acquaintances. Unfortunately this confirmation process is cumbersome and people can take insecure shortcuts. The other approach is to obtain keys from a trusted source such as HTTPS certificate authorities. The E2E crypto doesn’t have to be broken for the CA to provide a compromised key. The same applies to imessage.
A formal verification gives credibility to the cryptographic algorithms, but it does not imply the integrity or infallibility of apple’s directory service. Hypothetically a privileged apple employee could provision a new phone on a customer’s account and start impersonating the customer on imessage. The E2E encryption, even when it’s working, doesn’t really prevent this.