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
Přispěvatelé: Instituto de Engenharia de Sistemas e Computadores (INESC), Universidade do Porto, Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Institute IMDEA Software [Madrid], Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy), University of Surrey (UNIS), University of Bristol [Bristol], Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Computer Science Department [Boston] (Boston University), Boston University [Boston] (BU), Département d'informatique de l'École polytechnique (X-DEP-INFO), École polytechnique (X), ANR-18-CE25-0014,scrypt,Compilation sécurisée de primitives cryptographiques(2018), ANR-17-CE39-0004,TECAP,Analyse de protocoles - unir les outils existants(2017), Universidade do Porto = University of Porto, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Universidade do Minho
Jazyk: angličtina
Rok vydání: 2019
Předmět:
Zdroj: 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
Popis: 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.
This work received support from the National Institute of Standards and Technologies under agreement number 60NANB15D248.This work was partially supported by Office of Naval Research under projects N00014-12-1-0914, N00014-15-1-2750 and N00014-19-1-2292.This work was partially funded by national funds via the Portuguese Foundation for Science and Technology (FCT) in the context of project PTDC/CCI-INF/31698/2017. Manuel Barbosa was supported by grant SFRH/BSAB/143018/2018 awarded by the FCT.This work was supported in part by the National Science Foundation under grant number 1801564.This work was supported in part by the FutureTPM project of the Horizon 2020 Framework Programme of the European Union, under GA number 779391.This work was supported by the ANR Scrypt project, grant number ANR-18-CE25-0014.This work was supported by the ANR TECAP project, grant number ANR-17-CE39-0004-01.
Databáze: OpenAIRE
Externí odkaz: