To refer to this page use:
|Abstract:||We have proved, with machine-checked proofs in Coq, that an OpenSSL implementation of HMAC with SHA- 256 correctly implements its FIPS functional specification and that its functional specification guarantees the expected cryptographic properties. This is the first machine-checked cryptographic proof that combines a source-program implementation proof, a compiler-correctness proof, and a cryptographic-security proof, with no gaps at the specification interfaces. The verification was done using three systems within the Coq proof assistant: the Foundational Cryptography Framework, to verify crypto properties of functional specs; the Verified Software Toolchain, to verify C programs w.r.t. functional specs; and CompCert, for verified compilation of C to assembly language.|
|Citation:||Beringer, L, Petcher, A, Ye, K, Appel, A. "Verified correctness and security of OpenSSL HMAC" Proceedings of the 24th USENIX Conference on Security Symposium, 207 - 221|
|Pages:||207 - 221|
|Type of Material:||Conference Article|
|Journal/Proceeding Title:||Proceedings of the 24th USENIX Conference on Security Symposium, August 12-14, 2015, Washington, D.C.|
|Version:||This is the author’s final manuscript. All rights reserved to author(s).|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.