Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3

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

Publikováno v: CCS 2019-26th ACM Conference on Computer and Communications Security
CCS 2019-26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.1607-1622, ⟨10.1145/3319535.3363211⟩
CCS
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security
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 (ACM), pp. 1607-1622, ACM CCS 2019, London, United Kingdom, 11/11/19 . https://doi.org/10.1145/3319535.3363211

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 resistanc

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::81ad6142ce1106a8c1d25f32a2c29be8
https://hal.archives-ouvertes.fr/hal-02404581/document