Welcome to the resource topic for 2025/980
Title:
Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust
Authors: Karthikeyan Bhargavan, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, Bas Spitters
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.
ePrint: https://eprint.iacr.org/2025/980
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .