Formal Security & Verification of Cryptographic Protocol Implementations in Rust

Paper 2025/980

Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust

Karthikeyan Bhargavan, Cryspen

Lasse Letager Hansen, Aarhus University

Franziskus Kiefer, Cryspen

Jonas Schneider-Bensch, Cryspen

Bas Spitters, Aarhus University

Abstract

We present an effective methodology for the formal verification of practical cryptographic protocol implementations written in Rust. Within a single proof framework, we show how to develop machine-checked proofs of diverse properties like runtime safety, parsing correctness, and cryptographic protocol security. All analysis tasks are driven by the software developer who writes annotations in the Rust source code and chooses a backend prover for each task, ranging from a generic proof assistant like F$\star$ to dedicated crypto-oriented provers like ProVerif and SSProve Our main contribution is a demonstration of this methodology on Bert13, a portable, post-quantum implementation of TLS 1.3 written in Rust and verified both for security and functional correctness. To our knowledge, this is the first security verification result for a protocol implementation written in Rust, and the first verified post-quantum TLS 1.3 library.

Note: Code and proofs https://github.com/cryspen/bertie