Commit 91b9ca96 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

add a 3 verification with VST: CCS2017

parent 5f33c4dc
......@@ -71,7 +71,7 @@ to synthesize certified elliptic-curve crypto software~\cite{Philipoom2018Correc
This software suite is now being used in BoringSSL~\cite{fiat-crypto}.
The verification approach has been used to prove the correctness of OpenSSL's
implementations of HMAC~\cite{Beringer2015VerifiedCA} and SHA-256~\cite{2015-Appel}.
implementations of HMAC~\cite{Beringer2015VerifiedCA}, mbedTLS HMAC-DRBG~\cite{2017-Ye} and SHA-256~\cite{2015-Appel}.
In terms of languages and tooling, this work is closest to what we present here,
but our work considers an asymmetric primitive and provides computer-verified
proofs up to the mathematical definition of the group theory behind elliptic curves.
......@@ -57,6 +57,30 @@
_publisher = {ACM},
author = {Katherine Q. Ye and
Matthew Green and
Naphat Sanguansin and
Lennart Beringer and
Adam Petcher and
Andrew W. Appel},
title = {Verified Correctness and Security of MbedTLS HMAC-DRBG},
booktitle = {Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security},
year = {2017},
series = {CCS ’17},
pages = {2007–2020},
address = {New York, NY, USA},
publisher = {ACM},
note = {\url{}},
_doi = {10.1145/3133956.3133974},
_isbn = {9781450349468},
_keywords = {formal verification, pseudo-random generator, hmac-drbg, functional specification},
_location = {Dallas, Texas, USA},
_numpages = {14},
author = {Daniel J. Bernstein and
Bernard van Gastel and
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment