Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging
Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, Rolfe Schmidt
33rd USENIX Security Symposium · Day 1 · USENIX Security '24
This talk details the collaborative effort between Signal Messenger and academic researchers to formally verify PQXDH, a post-quantum key agreement protocol designed to augment the widely used Signal Protocol. Presented by Rolfe Schmidt, an engineer at Signal Messenger, the presentation underscores the critical role of **formal verification** in securing real-world cryptographic protocols, particularly as the industry navigates the complexities of migrating to **post-quantum cryptography (PQC)**. The core message is that even seemingly minor modifications to established protocols for post-quantum security can introduce subtle yet severe vulnerabilities, which formal methods are uniquely positioned to uncover and mitigate.
AI review
This talk presents critical formal verification work on Signal's PQXDH protocol, revealing a novel KEM re-encapsulation attack that undermines post-quantum security guarantees. The discovery of this attack, its elegant fix, and the definition of a new KEM property (SHCR) provide invaluable lessons for anyone designing or migrating to post-quantum cryptographic systems. This is real research with direct, high-stakes impact on billions of users' privacy.