| Title | Verified Correctness and Security of mbedTLS HMAC-DRBG |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Ye, Katherine Q., Green, Matthew, Sanguansin, Naphat, Beringer, Lennart, Petcher, Adam, Appel, Andrew W. |
| Conference Name | Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4946-8 |
| Keywords | composability, compositionality, Computing Theory, formal verification, functional specification, hmac-drbg, pseudo-random generator, pubcrawl |
| Abstract | 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. |
| URL | http://doi.acm.org/10.1145/3133956.3133974 |
| DOI | 10.1145/3133956.3133974 |
| Citation Key | ye_verified_2017 |
Verified Correctness and Security of mbedTLS HMAC-DRBG