# Verified Correctness and Security of mbedTLS HMAC-DRBG

arXiv: https://arxiv.org/abs/1708.08542 · HTML: https://mlsanity.com/paper/1708.08542/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Aug 2017.

## Built on by (most cited first, 1 of 1)

- [An AI Approach to Verified Production Cryptographic Libraries](https://mlsanity.com/paper/2608.00965/) (2026)

## Abstract (arXiv)

We have formalized the functional specification of HMAC-DRBG (NIST 800-90A), and we have proved its cryptographic security--that its output is pseudorandom--using a hybrid game-based proof. We have also proved that the mbedTLS implementation (C program) correctly implements this functional specification. That proof composes with an existing C compiler correctness proof to guarantee, end-to-end, that the machine language program gives strong pseudorandomness. All proofs (hybrid games, C program verification, compiler, and their composition) are machine-checked in the Coq proof assistant. Our proofs are modular: the hybrid game proof holds on any implementation of HMAC-DRBG that satisfies our functional specification. Therefore, our functional specification can serve as a high-assurance reference.