This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2012 IEEE 25th Computer Security Foundations Symposium (CSF 2012)
Cambridge, MA USA
June 25-June 27
ISBN: 978-0-7695-4718-3
M. Backes, Saarland Univ., Saarbrucken, Germany
G. Barthe, IMDEA Software Inst., Madrid, Spain
M. Berg, Saarland Univ., Saarbrucken, Germany
B. Gregoire, INRIA Sophia Antipolis-Mediterranee, Sophia-Antipolis, France
C. Kunz, Univ. Politec. de Madrid, Madrid, Spain
M. Skoruppa, Saarland Univ., Saarbrucken, Germany
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 in differentiability of Merkle-Damgaard, a construction that underlies many existing hash functions. Our proofs are built and verified using an extension of the Easy Crypt framework, which relies on state-of-the-art verification tools such as automated theorem provers, SMT solvers, and interactive proof assistants.
Index Terms:
Cryptography,Resistance,Games,Probabilistic logic,Semantics,Electronic mail,Easy Crypt,Cryptographic hash functions,collision-resistance,indifferentiability,Merkle-Damgaard,SHA-3
Citation:
M. Backes, G. Barthe, M. Berg, B. Gregoire, C. Kunz, M. Skoruppa, S. Z. Beguelin, "Verified Security of Merkle-Damgård," csf, pp.354-368, 2012 IEEE 25th Computer Security Foundations Symposium (CSF 2012), 2012
Usage of this product signifies your acceptance of the Terms of Use.