Princeton University Library Catalog
- Ye, Katherine [Browse]
- Senior thesis
- Appel, Andrew [Browse]
- Green, Matthew [Browse]
- Princeton University. Department of Computer Science [Browse]
- Class year:
- 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.