Verified Security of Merkle-Damgaard

Abstract : Cryptographic hash functions provide a basic data authentication mechanism and are used pervasively as building blocks to realize many cryptographic functionalities, including block ciphers, message authentication codes, key exchange protocols, and encryption and digital signature schemes. Since weaknesses in hash functions may imply vulnerabilities in the constructions that build upon them, ensuring their security is essential. Unfortunately, many widely used hash functions, including SHA-1 and MD5, are subject to practical attacks. The search for a secure replacement is one of the most active topics in the field of cryptography. In this paper we report on the first machine-checked and independently-verifiable proofs of collision-resistance and indifferentiability of Merkle-Damg{å}rd, a construction that underlies many existing hash functions. Our proofs are built and verified using an extension of the EasyCrypt framework, which relies on state-of-the-art verification tools such as automated theorem provers, SMT solvers, and interactive proof assistants.
Type de document :
Communication dans un congrès
25th IEEE Computer Security Foundations Symposium, CSF 2012, Jun 2012, Cambridge, MA, United States. IEEE, pp.354-368, 2012, Computer Security Foundations Symposium (CSF), 2012 IEEE 25th. 〈10.1109/CSF.2012.14〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00765883
Contributeur : Benjamin Gregoire <>
Soumis le : lundi 17 décembre 2012 - 10:16:57
Dernière modification le : mardi 30 janvier 2018 - 16:38:02
Document(s) archivé(s) le : dimanche 18 décembre 2016 - 03:05:23

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, Cesar Kunz, et al.. Verified Security of Merkle-Damgaard. 25th IEEE Computer Security Foundations Symposium, CSF 2012, Jun 2012, Cambridge, MA, United States. IEEE, pp.354-368, 2012, Computer Security Foundations Symposium (CSF), 2012 IEEE 25th. 〈10.1109/CSF.2012.14〉. 〈hal-00765883〉

Partager

Métriques

Consultations de la notice

288

Téléchargements de fichiers

317