publication . Conference object . Contribution for newspaper or weekly magazine . 2019

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

Cavallaro, Lorenzo; Kinder, Johannes; Wang, XiaoFeng; Katz, Jonathan; Almeida, José Bacelar; Baritel-Ruet, Cécile; Barbosa, Manuel; Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; ...
Open Access English
  • Published: 11 Nov 2019
  • Publisher: HAL CCSD
Abstract
International audience; 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, ...
Subjects
free text keywords: SHA-3, indifferentiability, high-assurance cryptography, EasyCrypt, Jasmin, [INFO]Computer Science [cs], [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Hash function, Theoretical computer science, Correctness, Random oracle, Cryptographic primitive, Provable security, Timing attack, Proof assistant, Computer science
Funded by
ANR| scrypt
Project
scrypt
Secure Compilation of Cryptographic primitives
  • Funder: French National Research Agency (ANR) (ANR)
  • Project Code: ANR-18-CE25-0014
,
NSF| SaTC: CORE: Medium: Towards Mechanized Proofs of Composable Security Properties
Project
  • Funder: National Science Foundation (NSF)
  • Project Code: 1801564
  • Funding stream: Directorate for Computer & Information Science & Engineering | Division of Computer and Network Systems
,
ANR| TECAP
Project
TECAP
Protocol Analysis - Combining Existing Tools
  • Funder: French National Research Agency (ANR) (ANR)
  • Project Code: ANR-17-CE39-0004
,
EC| FutureTPM
Project
FutureTPM
Future Proofing the Connected World: A Quantum-Resistant Trusted Platform Module
  • Funder: European Commission (EC)
  • Project Code: 779391
  • Funding stream: H2020 | RIA
18 references, page 1 of 2

[1] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. In ACM CCS 2017: 24th Conference on Computer and Communications Security, Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM Press, 1807-1823. https://doi.org/10.1145/3133956.3134078 [OpenAIRE]

[2] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and François Dupressoir. 2013. Certified computer-aided cryptography: eficient provably secure machine code from high-level implementations. In ACM CCS 2013: 20th Conference on Computer and Communications Security, Ahmad-Reza Sadeghi, Virgil D. Gligor, and Moti Yung (Eds.). ACM Press, 1217-1230. https://doi.org/10.1145/2508859. 2516652

[3] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and François Dupressoir. 2016. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. In Fast Software Encryption - FSE 2016 (Lecture Notes in Computer Science), Thomas Peyrin (Ed.), Vol. 9783. Springer, Heidelberg, 163-184. https://doi.org/10.1007/978-3-662-52993-5_9

[4] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. 2016. Verifying Constant-Time Implementations. In USENIX Security 2016: 25th USENIX Security Symposium, Thorsten Holz and Stefan Savage (Eds.). USENIX Association, 53-70.

[23] Morris J. Dworkin. 2015. SHA-3 Standard: Permutation-Based Hash and Extendable-Output Functions. http://dx.doi.org/10.6028/NIST.FIPS.202

[24] Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. In IEEE Security & Privacy. To appear. Retrieved from http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf.

[25] Xavier Leroy. 2009. A Formally Verified Compiler Back-end. J. Autom. Reasoning 43, 4 (2009), 363-446. https://doi.org/10.1007/s10817-009-9155-4

[26] Ueli M. Maurer, Renato Renner, and Clemens Holenstein. 2004. Indiferentiability, Impossibility Results on Reductions, and Applications to the Random Oracle Methodology. In TCC 2004: 1st Theory of Cryptography Conference (Lecture Notes in Computer Science), Moni Naor (Ed.), Vol. 2951. Springer, Heidelberg, 21-39. https://doi.org/10.1007/978-3-540-24638-1_2 [OpenAIRE]

[27] Adam Petcher and Greg Morrisett. 2015. The Foundational Cryptography Framework. In Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. 53-72. https://doi.org/10.1007/978-3-662-46666-7_4 [OpenAIRE]

[28] Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph Wintersteiger, and Santiago Zanella-Beguelin. 2019. EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. Cryptology ePrint Archive, Report 2019/757. https://eprint.iacr.org/2019/757.

[29] Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. 2017. Verified low-level programming embedded in F*. PACMPL 1, ICFP (2017), 17:1- 17:29. https://doi.org/10.1145/3110261

[30] Thomas Ristenpart, Hovav Shacham, and Thomas Shrimpton. 2011. Careful with Composition: Limitations of the Indiferentiability Framework. In Advances in Cryptology - EUROCRYPT 2011 (Lecture Notes in Computer Science), Kenneth G. Paterson (Ed.), Vol. 6632. Springer, Heidelberg, 487-506. https://doi.org/10.1007/ 978-3-642-20465-4_27 [OpenAIRE]

[31] Phillip Rogaway and Thomas Shrimpton. 2004. Cryptographic Hash-Function Basics: Definitions, Implications, and Separations for Preimage Resistance, Second-Preimage Resistance, and Collision Resistance. In Fast Software Encryption - FSE 2004 (Lecture Notes in Computer Science), Bimal K. Roy and Willi Meier (Eds.), Vol. 3017. Springer, Heidelberg, 371-388. https://doi.org/10.1007/ 978-3-540-25937-4_24 [OpenAIRE]

[32] Victor Shoup. 2004. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332. http://eprint.iacr.org/2004/ 332.

[33] Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine DelignatLavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016. Dependent Types and Multi-Monadic Efects in F*. In 43rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256- 270. https://www.fstar-lang.org/papers/mumon/

18 references, page 1 of 2
Abstract
International audience; 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, ...
Subjects
free text keywords: SHA-3, indifferentiability, high-assurance cryptography, EasyCrypt, Jasmin, [INFO]Computer Science [cs], [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Hash function, Theoretical computer science, Correctness, Random oracle, Cryptographic primitive, Provable security, Timing attack, Proof assistant, Computer science
Funded by
ANR| scrypt
Project
scrypt
Secure Compilation of Cryptographic primitives
  • Funder: French National Research Agency (ANR) (ANR)
  • Project Code: ANR-18-CE25-0014
,
NSF| SaTC: CORE: Medium: Towards Mechanized Proofs of Composable Security Properties
Project
  • Funder: National Science Foundation (NSF)
  • Project Code: 1801564
  • Funding stream: Directorate for Computer & Information Science & Engineering | Division of Computer and Network Systems
,
ANR| TECAP
Project
TECAP
Protocol Analysis - Combining Existing Tools
  • Funder: French National Research Agency (ANR) (ANR)
  • Project Code: ANR-17-CE39-0004
,
EC| FutureTPM
Project
FutureTPM
Future Proofing the Connected World: A Quantum-Resistant Trusted Platform Module
  • Funder: European Commission (EC)
  • Project Code: 779391
  • Funding stream: H2020 | RIA
18 references, page 1 of 2

[1] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. In ACM CCS 2017: 24th Conference on Computer and Communications Security, Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM Press, 1807-1823. https://doi.org/10.1145/3133956.3134078 [OpenAIRE]

[2] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and François Dupressoir. 2013. Certified computer-aided cryptography: eficient provably secure machine code from high-level implementations. In ACM CCS 2013: 20th Conference on Computer and Communications Security, Ahmad-Reza Sadeghi, Virgil D. Gligor, and Moti Yung (Eds.). ACM Press, 1217-1230. https://doi.org/10.1145/2508859. 2516652

[3] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and François Dupressoir. 2016. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. In Fast Software Encryption - FSE 2016 (Lecture Notes in Computer Science), Thomas Peyrin (Ed.), Vol. 9783. Springer, Heidelberg, 163-184. https://doi.org/10.1007/978-3-662-52993-5_9

[4] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. 2016. Verifying Constant-Time Implementations. In USENIX Security 2016: 25th USENIX Security Symposium, Thorsten Holz and Stefan Savage (Eds.). USENIX Association, 53-70.

[23] Morris J. Dworkin. 2015. SHA-3 Standard: Permutation-Based Hash and Extendable-Output Functions. http://dx.doi.org/10.6028/NIST.FIPS.202

[24] Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. In IEEE Security & Privacy. To appear. Retrieved from http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf.

[25] Xavier Leroy. 2009. A Formally Verified Compiler Back-end. J. Autom. Reasoning 43, 4 (2009), 363-446. https://doi.org/10.1007/s10817-009-9155-4

[26] Ueli M. Maurer, Renato Renner, and Clemens Holenstein. 2004. Indiferentiability, Impossibility Results on Reductions, and Applications to the Random Oracle Methodology. In TCC 2004: 1st Theory of Cryptography Conference (Lecture Notes in Computer Science), Moni Naor (Ed.), Vol. 2951. Springer, Heidelberg, 21-39. https://doi.org/10.1007/978-3-540-24638-1_2 [OpenAIRE]

[27] Adam Petcher and Greg Morrisett. 2015. The Foundational Cryptography Framework. In Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. 53-72. https://doi.org/10.1007/978-3-662-46666-7_4 [OpenAIRE]

[28] Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph Wintersteiger, and Santiago Zanella-Beguelin. 2019. EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. Cryptology ePrint Archive, Report 2019/757. https://eprint.iacr.org/2019/757.

[29] Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. 2017. Verified low-level programming embedded in F*. PACMPL 1, ICFP (2017), 17:1- 17:29. https://doi.org/10.1145/3110261

[30] Thomas Ristenpart, Hovav Shacham, and Thomas Shrimpton. 2011. Careful with Composition: Limitations of the Indiferentiability Framework. In Advances in Cryptology - EUROCRYPT 2011 (Lecture Notes in Computer Science), Kenneth G. Paterson (Ed.), Vol. 6632. Springer, Heidelberg, 487-506. https://doi.org/10.1007/ 978-3-642-20465-4_27 [OpenAIRE]

[31] Phillip Rogaway and Thomas Shrimpton. 2004. Cryptographic Hash-Function Basics: Definitions, Implications, and Separations for Preimage Resistance, Second-Preimage Resistance, and Collision Resistance. In Fast Software Encryption - FSE 2004 (Lecture Notes in Computer Science), Bimal K. Roy and Willi Meier (Eds.), Vol. 3017. Springer, Heidelberg, 371-388. https://doi.org/10.1007/ 978-3-540-25937-4_24 [OpenAIRE]

[32] Victor Shoup. 2004. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332. http://eprint.iacr.org/2004/ 332.

[33] Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine DelignatLavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016. Dependent Types and Multi-Monadic Efects in F*. In 43rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256- 270. https://www.fstar-lang.org/papers/mumon/

18 references, page 1 of 2
Any information missing or wrong?Report an Issue