Paper Info
Title
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3
Abstract
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.
Year
DOI
Venue
2019
10.1145/3319535.3363211
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security
Keywords
Field
DocType
EasyCrypt, Jasmin, SHA-3, high-assurance cryptography, indifferentiability
Computer security,Cryptography,Computer science,SHA-3,Implementation,Mathematical proof,High assurance
Conference
ISBN
Citations 
PageRank 
978-1-4503-6747-9
0
0.34
References 
Authors
0
10
Name
Order
Citations
PageRank
José Bacelar Almeida11028.34
Cécile Baritel-Ruet200.34
Manuel Barbosa333724.91
Gilles Barthe42337152.36
François Dupressoir51749.68
Benjamin Grégoire681748.93
Vincent Laporte7364.95
Tiago R. Oliveira83610.45
Alley Stoughton9153.31
Pierre-Yves Strub1054029.87