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

doi:10.1145/3319535.3363211

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 proceeding › Conference Contribution (Conference Proceeding)

31 Citations (Scopus)

256 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 language	English
Title of host publication	CCS'19
Subtitle of host publication	Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security
Publisher	Association for Computing Machinery
Pages	1607-1622
Number of pages	15
ISBN (Print)	978-1-4503-6747-9
DOIs	https://doi.org/10.1145/3319535.3363211
Publication status	Published - 15 Nov 2019
Event	ACM CCS 2019: 26th ACM Conference on Computer and Communications Security - London, United Kingdom Duration: 11 Nov 2019 → 15 Nov 2019 Conference number: 26 https://www.sigsac.org/ccs/CCS2019/

Conference

Conference	ACM CCS 2019
Abbreviated title	ACM CCS 2019
Country/Territory	United Kingdom
City	London
Period	11/11/19 → 15/11/19
Internet address	https://www.sigsac.org/ccs/CCS2019/

Bibliographical note

Provisional publication date added based on conference dates.

Access to Document

10.1145/3319535.3363211

Full-text PDF (author’s accepted manuscript)
This is the author accepted manuscript (AAM). The final published version (version of record) is available online via ACM at https://dl.acm.org/doi/10.1145/3319535.3363211. Please refer to any applicable terms of use of the publisher.
Accepted author manuscript, 963 KB

Handle.net

Persistent link

Cite this

Bacelar Almeida, J., Barbosa, M., Baritel-Ruet, C., Barthe, G., Dupressoir, F., Grégoire, B., Laporte, V., Oliveira, T., Strub, P.-Y., & Stoughton, A. (2019). Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and secure high-assurance implementations of SHA-3. In CCS'19: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (pp. 1607-1622). Association for Computing Machinery. https://doi.org/10.1145/3319535.3363211

@inproceedings{c4da71902b8d4efe98a551660be7f6d1,

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.",

author = "\{Bacelar Almeida\}, Jos{\'e} and Manuel Barbosa and C{\'e}cile Baritel-Ruet and Gilles Barthe and Fran{\c c}ois Dupressoir and Benjamin Gr{\'e}goire and Vincent Laporte and Tiago Oliveira and Pierre-Yves Strub and Alley Stoughton",

note = "Provisional publication date added based on conference dates. ; ACM CCS 2019 : 26th ACM Conference on Computer and Communications Security, ACM CCS 2019 ; Conference date: 11-11-2019 Through 15-11-2019",

year = "2019",

month = nov,

day = "15",

doi = "10.1145/3319535.3363211",

language = "English",

isbn = "978-1-4503-6747-9",

pages = "1607--1622",

booktitle = "CCS'19",

publisher = "Association for Computing Machinery",

address = "United States",

url = "https://www.sigsac.org/ccs/CCS2019/",

}

Bacelar Almeida, J, Barbosa, M, Baritel-Ruet, C, Barthe, G, Dupressoir, F, Grégoire, B, Laporte, V, Oliveira, T, Strub, P-Y & Stoughton, A 2019, Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and secure high-assurance implementations of SHA-3. in CCS'19: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, pp. 1607-1622, ACM CCS 2019, London, United Kingdom, 11/11/19. https://doi.org/10.1145/3319535.3363211

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and secure high-assurance implementations of SHA-3. / Bacelar Almeida, José; Barbosa, Manuel; Baritel-Ruet, Cécile et al.
CCS'19: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, 2019. p. 1607-1622.

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

TY - GEN

T1 - Machine-Checked Proofs for Cryptographic Standards

T2 - ACM CCS 2019

AU - Bacelar Almeida, José

AU - Barbosa, Manuel

AU - Baritel-Ruet, Cécile

AU - Barthe, Gilles

AU - Dupressoir, François

AU - Grégoire, Benjamin

AU - Laporte, Vincent

AU - Oliveira, Tiago

AU - Strub, Pierre-Yves

AU - Stoughton, Alley

N1 - Conference code: 26

PY - 2019/11/15

Y1 - 2019/11/15

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.

U2 - 10.1145/3319535.3363211

DO - 10.1145/3319535.3363211

M3 - Conference Contribution (Conference Proceeding)

SN - 978-1-4503-6747-9

SP - 1607

EP - 1622

BT - CCS'19

PB - Association for Computing Machinery

Y2 - 11 November 2019 through 15 November 2019

ER -

Bacelar Almeida J, Barbosa M, Baritel-Ruet C, Barthe G, Dupressoir F, Grégoire B et al. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and secure high-assurance implementations of SHA-3. In CCS'19: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery. 2019. p. 1607-1622 doi: 10.1145/3319535.3363211

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

Abstract

Conference

Bibliographical note

Access to Document

Handle.net

Fingerprint

Cite this