Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/11229
Title: Machine-Checked Proofs for Cryptographic Standards Indifferentiability of SPONGE and Secure High-Assurance Implementations of SHA-3
Authors: José Bacelar Almeida
Strub,PY
Stoughton,A
Tiago Filipe Oliveira
Laporte,V
Gregoire,B
Dupressoir,F
Barthe,G
Manuel Barbosa
Baritel Ruet,C
Issue Date: 2019
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.
URI: http://repositorio.inesctec.pt/handle/123456789/11229
http://dx.doi.org/10.1145/3319535.3363211
metadata.dc.type: conferenceObject
Publication
Appears in Collections:HASLab - Articles in International Conferences

Files in This Item:
File Description SizeFormat 
P-00R-F7P.pdf1.58 MBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.