Skip navigation
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 
Ye_Katherine_thesis.pdf489.62 kBAdobe PDF    Request a copy


Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.