Verified correctness and security of mbed TLS HMAC-DRBG

Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

47 Scopus citations

Abstract

We have formalized the functional specication 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 specication. 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 satises our functional specication. Therefore, our functional specication can serve as a high-assurance reference.

Original languageEnglish (US)
Title of host publicationCCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security
PublisherAssociation for Computing Machinery
Pages2007-2020
Number of pages14
ISBN (Electronic)9781450349468
DOIs
StatePublished - Oct 30 2017
Event24th ACM SIGSAC Conference on Computer and Communications Security, CCS 2017 - Dallas, United States
Duration: Oct 30 2017Nov 3 2017

Publication series

NameProceedings of the ACM Conference on Computer and Communications Security
ISSN (Print)1543-7221

Other

Other24th ACM SIGSAC Conference on Computer and Communications Security, CCS 2017
Country/TerritoryUnited States
CityDallas
Period10/30/1711/3/17

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'Verified correctness and security of mbed TLS HMAC-DRBG'. Together they form a unique fingerprint.

Cite this