Cryspen | Cryptographic protocol verification with hax
This blog post details an example of how to use our hax toolchain for verifying the security of cryptographic protocol implementations written in Rust.
One goal is to prove implementation correctness. In this case the code in question is proven to be free of panics, or that the optimizations that it uses preserve conformance to a higher-level mathematical specification. hax is well-suited to doing this type of verification, by extracting a model of the code in F*. A recent example of this approach is our verified implementation of ML-KEM (Kyber). You can read more details about the verification effort in a separate blog post.
Another flavor of verification is security verification, where we want to establish, beyond correctness, that a piece of code achieves specific properties even in the presence of an attacker. For example, we recently joined forces with Rolfe Schmidt and Charlie Jacomme to provide a protocol analysis of Signal’s new PQXDH post-quantum key agreement protocol. In this case, though we found no serious security issues, we made out a number of imprecisions and potential pitfalls in the original specification and Signal addressed these with a new version of the protocol specification. For the new specification we used the ProVerif and CryptoVerif protocol analysis tools to show among other results that security properties such as forward secrecy are preserved in the presence of a quantum attacker and that the protocol resists store-now-decrypt-later attacks.
The analysis of PQXDH was carried out in the traditional style, where a group of protocol verification experts diligently model a protocol by hand, based on its (more or less formal) specification.
