International Association
for Cryptologic Research

In this talk, we describe PQXDH, a new post-quantum key agreement protocol deployed by Signal, its formal analysis using the ProVerif and CryptoVerif protocol analysis tools, and how this analysis influenced version 2 of PQXDH. We focus on the lessons learned in this process and how formal verification can be a powerful tool in an industrial setting. The talk will be given jointly by Rolfe Schmidt and Karthikeyan Bhargavan.