Machine-Checked Proofs for Cryptographic Standards
Tools
Tools
Tools
Almeida, José Bacelar, Baritel-Ruet, Cécile, Barbosa, Manuel, Barthe, Gilles, Dupressoir, François, Grégoire, Benjamin, Laporte, Vincent Laporte, Oliveira, Tiago, Stoughton, Alley and Strub, Pierre-Yves (2019) Machine-Checked Proofs for Cryptographic Standards In: 26th ACM Conference on Computer and Communications Security (CCS 2019), 11-15 Nov 2019, London, UK.
|
Text
Machine-Checked Proofs for Cryptographic Standards.pdf - Accepted version Manuscript Download (986kB) | Preview |
Official URL: https://doi.org/10.1145/3319535.3363211
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.
| Item Type: | Conference or Workshop Item (Conference Paper) | |||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Divisions : | Faculty of Engineering and Physical Sciences > Computer Science | |||||||||||||||||||||||||||||||||
| Authors : |
|
|||||||||||||||||||||||||||||||||
| Date : | 2019 | |||||||||||||||||||||||||||||||||
| Funders : | European Union's Horizon 2020 | |||||||||||||||||||||||||||||||||
| DOI : | 10.1145/3319535.3363211 | |||||||||||||||||||||||||||||||||
| Grant Title : | FutureTPM | |||||||||||||||||||||||||||||||||
| Copyright Disclaimer : | © 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM. | |||||||||||||||||||||||||||||||||
| Uncontrolled Keywords : | High-assurance cryptography; EasyCrypt; Jasmin; SHA-3; Indifferentiability | |||||||||||||||||||||||||||||||||
| Related URLs : | ||||||||||||||||||||||||||||||||||
| Additional Information : | Session 7D: Formal Analysis III | |||||||||||||||||||||||||||||||||
| Depositing User : | Clive Harris | |||||||||||||||||||||||||||||||||
| Date Deposited : | 09 Oct 2019 10:59 | |||||||||||||||||||||||||||||||||
| Last Modified : | 12 Dec 2019 15:21 | |||||||||||||||||||||||||||||||||
| URI: | http://epubs.surrey.ac.uk/id/eprint/852900 |
Actions (login required)
 |
View Item |
Downloads
Downloads per month over past year