Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and secure high-assurance implementations of SHA-3

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

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

25 Citations (Scopus)
212 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationCCS'19
Subtitle of host publicationProceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security
PublisherAssociation for Computing Machinery (ACM)
Pages1607-1622
Number of pages15
ISBN (Print)978-1-4503-6747-9
DOIs
Publication statusPublished - 15 Nov 2019
EventACM CCS 2019: 26th ACM Conference on Computer and Communications Security - London, United Kingdom
Duration: 11 Nov 201915 Nov 2019
Conference number: 26
https://www.sigsac.org/ccs/CCS2019/

Conference

ConferenceACM CCS 2019
Abbreviated titleACM CCS 2019
Country/TerritoryUnited Kingdom
CityLondon
Period11/11/1915/11/19
Internet address

Bibliographical note

Provisional publication date added based on conference dates.

Fingerprint

Dive into the research topics of 'Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and secure high-assurance implementations of SHA-3'. Together they form a unique fingerprint.

Cite this