Princeton University Library Catalog

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

Author/​Artist:
Ye, Katherine [Browse]
Format:
Senior thesis
Language:
English
Advisor(s):
Appel, Andrew [Browse]
Contributor(s):
Green, Matthew [Browse]
Department:
Princeton University. Department of Computer Science [Browse]
Class year:
2016
Description:
73 pages
Summary note:
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.