Paper 2019/1155

Machine-Checked Proofs for Cryptographic Standards

José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, and Pierre-Yves Strub


We present a high-assurance and high-speed implementation of the SHA-3 hash function. Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. Our implementation is the first to achieve simultaneously the four desirable properties (efficiency, correctness, provable security, and side-channel protection) for a non-trivial cryptographic primitive. Concretely, our mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA-3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks. The proofs include new EasyCrypt libraries of independent interest for programmable random oracles and modular indifferentiability proofs.

Available format(s)
Publication info
Published elsewhere. ACM CCS 2019
high-assurance cryptographyEasyCryptJasminSHA-3indifferentiability
Contact author(s)
cecile baritel @ gmail com
fdupress @ gmail com
2019-10-07: received
Short URL
Creative Commons Attribution


      author = {José Bacelar Almeida and Cécile Baritel-Ruet and Manuel Barbosa and Gilles Barthe and François Dupressoir and Benjamin Grégoire and Vincent Laporte and Tiago Oliveira and Alley Stoughton and Pierre-Yves Strub},
      title = {Machine-Checked Proofs for Cryptographic Standards},
      howpublished = {Cryptology ePrint Archive, Paper 2019/1155},
      year = {2019},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.