Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp013484zk346
 Title: THE NOTORIOUS PRG:FORMAL VERIFICATION OF THE HMAC-DRBG PSEUDORANDOM NUMBER GENERATOR Authors: Ye, Katherine Advisors: Appel, Andrew Contributors: Green, Matthew Department: Computer Science Class Year: 2016 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. Extent: 73 pages URI: http://arks.princeton.edu/ark:/88435/dsp013484zk346 Type of Material: Princeton University Senior Theses Language: en_US Appears in Collections: Computer Science, 1988-2016

Files in This Item:
File SizeFormat