TY - GEN
T1 - Machine-checked proofs for cryptographic standards indifferentiability of sponge and secure high-assurance implementations of SHA-3
AU - Almeida, José Bacelar
AU - Barthe, Gilles
AU - Laporte, Vincent
AU - Baritel-Ruet, Cécile
AU - Dupressoir, François
AU - Oliveira, Tiago
AU - Strub, Pierre Yves
AU - Barbosa, Manuel
AU - Grégoire, Benjamin
AU - Stoughton, Alley
N1 - Publisher Copyright:
© 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.
PY - 2019/11/6
Y1 - 2019/11/6
N2 - 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.
AB - 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.
KW - EasyCrypt
KW - High-assurance cryptography
KW - Indifferentiability
KW - Jasmin
KW - SHA-3
U2 - 10.1145/3319535.3363211
DO - 10.1145/3319535.3363211
M3 - Conference contribution
AN - SCOPUS:85075931229
T3 - Proceedings of the ACM Conference on Computer and Communications Security
SP - 1607
EP - 1622
BT - CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security
PB - Association for Computing Machinery
T2 - 26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019
Y2 - 11 November 2019 through 15 November 2019
ER -