THE NOTORIOUS PRG:FORMAL VERIFICATION OF THE HMAC-DRBG PSEUDORANDOM NUMBER GENERATOR

Abstract

We have proved, with machine-checked proofs, that the output produced by HMAC-DRBG is indistinguishable from random by a computationally bounded adversary. We proved this about a high-level specification of a simplified version of HMAC-DRBG written in the probabilistic language provided by the Foundational Cryptography Framework (FCF), which is embedded in the Coq proof assistant. We have also proven on paper that HMAC-DRBG is backtrackingresistant. Our work comprises the first formal verification of a real-world PRG. Our functional specification can be then linked to a proof of functional correctness of mbedTLS’s C implementation of HMAC-DRBG, allowing our proofs of cryptographic security properties to transfer to this implementation. Thus, this will create the first fully verified real-world DRBG.