Cryptographic protocol verification with hax

Using hax’s new ProVerif backend to extract security models directly from Rust code, applied to the TLS 1.3 handshake.

This blog post details an example of how to use our hax toolchain for verifying the security of cryptographic protocol implementations written in Rust. When building high-assurance software, we use …