Show simple item record

dc.contributor.authorAlmeida, José Bacelaren_US
dc.contributor.authorBaritel-Ruet, Cécileen_US
dc.contributor.authorBarbosa, Manuelen_US
dc.contributor.authorBarthe, Gillesen_US
dc.contributor.authorDupressoir, Françoisen_US
dc.contributor.authorGrégoire, Benjaminen_US
dc.contributor.authorLaporte, Vincenten_US
dc.contributor.authorOliveira, Tiagoen_US
dc.contributor.authorStoughton, Alleyen_US
dc.contributor.authorStrub, Pierre-Yvesen_US
dc.date.accessioned2020-05-07T19:01:01Z
dc.date.available2020-05-07T19:01:01Z
dc.date.issued2019-11-06
dc.identifier.citationJosé Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub. 2019. "Machine-checked proofs for cryptographic standards." Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. CCS '19: 2019 ACM SIGSAC Conference on Computer and Communications Security. https://doi.org/10.1145/3319535.3363211
dc.identifier.urihttps://hdl.handle.net/2144/40690
dc.description.abstractWe 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.en_US
dc.description.urihttps://dl.acm.org/doi/10.1145/3319535.3363211
dc.language.isoen_US
dc.publisherACM, Inc.en_US
dc.relation.ispartofProceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security
dc.rightsThis work was determined by OpenBU staff to be the final author draft submitted using a template provided by the Association for Computing Machinery. It appears in OpenBU under the auspices of Boston University's Open Access Policy. Please write to open-help@bu.edu with any questions.en_US
dc.subjectHigh-assurance cryptographyen_US
dc.subjectEasyCrypten_US
dc.subjectJasminen_US
dc.subjectSHA-3en_US
dc.subjectIndifferentiabilityen_US
dc.titleMachine-checked proofs for cryptographic standardsen_US
dc.typeConference materialsen_US
dc.description.versionAccepted manuscripten_US
dc.identifier.doi10.1145/3319535.3363211
pubs.elements-sourcecrossrefen_US
pubs.notesEmbargo: No embargoen_US
pubs.organisational-groupBoston Universityen_US
pubs.organisational-groupBoston University, College of Arts & Sciencesen_US
pubs.organisational-groupBoston University, College of Arts & Sciences, Department of Computer Scienceen_US
pubs.publication-statusPublisheden_US
dc.date.online2019-11-06
dc.identifier.mycv533026


This item appears in the following Collection(s)

Show simple item record