Formal Verification of the PQXDH Post-Quantum Key Agreement Protocol for End-to-End Secure Messaging

Explore a 15-minute conference talk from USENIX Security '24 that delves into the formal verification of Signal Messenger's PQXDH (PostQuantum Extended Diffie-Hellman) protocol. Learn how researchers used PROVERIF and CRYPTOVERIF tools to analyze the security implications of this new asynchronous key agreement protocol, which aims to provide post-quantum forward secrecy protection against harvest-now-decrypt-later attacks. Discover the identified flaws and potential vulnerabilities in the PQXDH specification, understand how Signal's implementation choices mitigated these issues, and examine the newly defined binding property of the KEM proven for Kyber. Follow the collaborative process between researchers and protocol designers that led to an improved protocol specification, while gaining insights into the challenges of upgrading protocols for post-quantum security and the importance of formal verification in protocol design.