Crypto is the top international conference on cryptography and is held every year (since 1981) in Santa Barbara, California. This year, Crypto invited Karthikeyan Bhargavan, our Chief Research Scientist, to give a talk on the use of formal methods in cryptography.

Karthik spoke about the state of the art in formal analysis techniques for crypto, and how we can use them to increase confidence in important protocols like PQXDH, TLS, and MLS. He also spoke about how we at Cryspen use hax to build verified post-quantum cryptographic libraries like libcrux.

The slides for Karthik’s invited talk are available here.

As Karthik says, if current trends hold, then in a few years, we can expect that all new protocols and cryptographic libraries will need to have machine-checked proofs by default. The time to adopt formal verification is now!

If you have any questions about formal methods, and on how they can help you to get higher assurance in your cryptographic software, send us an email.