Paper 2025/980 Original: eprint.iacr.org/2025/980 ↗
Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust
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.
Metadata
- Available format(s)
PDF- Category
- Implementation
- Publication info
- Preprint.
- History
- 2025-10-10: last updated
- 2025-05-28: published
- Short URL
- https://ia.cr/2025/980
- License
- https://creativecommons.org/licenses/by-sa/4.0/
BibTeX
@misc{cryptoeprint:2025/980,
author = {Karthikeyan Bhargavan and Lasse Letager Hansen and Franziskus Kiefer and Jonas Schneider-Bensch and Bas Spitters},
title = {Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/980},
year = {2025},
url = {https://eprint.iacr.org/2025/980}
}