Skip to main content

Verified correctness and security of OpenSSL HMAC

Author(s): Beringer, L; Petcher, A; Ye, K; Appel, Andrew W.

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.
Publication Date: 2015
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.