Building Confidence in Cryptographic Protocols

In this paper, we present an overview of our work on formally verifying the security properties of KEMTLS, a post-quantum secure key exchange protocol that is being proposed for standardization by the Internet Engineering Task Force (IETF). We describe how we modeled the KEMTLS protocol in Tamarin, a symbolic model checker. We then present some of the challenges we faced while performing this verification work and discuss our strategies for overcoming them. Finally, we provide an overview of our proof that KEMTLS achieves its security goals. Reference(s): [1] "Why does cryptographic software fail?: a case study and open problems" by David Lazar, Haogang Chen, Xi Wang and Nickolai Zeldovich [2] "SoK: Computer-Aided Cryptography" by Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao and Bryan Parno [3] "Post-quantum TLS without handshake signatures" by Peter Schwabe and Douglas Stebila and Thom Wiggers [4] "A comprehensive symbolic analysis of TLS 1.3." by Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe [5] "A Logic of Authentication" by Michael Burrows, Martin Abadi, and Roger M. Needham