Verifiable Security of Merkle-Damgård

Cryptographic hash functions provide a basic data authentication mechanism and are used pervasively as build ing blocks to realize many cryptographic functionalities, including block ciphers, message authentication codes, key exchange protocols, and encryption and digital signature schemes. S ince weaknesses in hash functions may imply vulnerabilities in t he constructions that build upon them, ensuring their security is essential. Unfortunately, many widely used hash functio ns, including SHA-1 and MD5, are subject to practical attacks. The search for a secure replacement is one of the most active topi cs in the field of cryptography. In this paper we report on the first machine-checked and independently-verifiable proofsof 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.