You are looking at a specific version 20060727:062437 of this paper. See the latest version.

Paper 2006/254

Applications of SAT Solvers to Cryptanalysis of Hash Functions

Ilya Mironov and Lintao Zhang

Abstract

Several standard cryptographic hash functions were broken in 2005. Some essential building blocks of these attacks lend themselves well to automation by encoding them as CNF formulas, which are within reach of modern SAT solvers. In this paper we demonstrate effectiveness of this approach. In particular, we are able to generate full collisions for MD4 and MD5 given only the differential path and applying a (minimally modified) off-the-shelf SAT solver. To the best of our knowledge, this is the first example of a SAT-solver-aided cryptanalysis of a non-trivial cryptographic primitive. We expect SAT solvers to find new applications as a validation and testing tool of practicing cryptanalysts.

Note: This is the full version of the paper presented at SAT 06.

Metadata
Available format(s)
PDF PS
Category
Secret-key cryptography
Publication info
Published elsewhere. Theory and Applications of Satisfiability Testing (SAT 06), pages 102--115, 2006
Keywords
hash functionscryptanalysisSAT solver
Contact author(s)
mironov @ microsoft com
History
2006-07-27: received
Short URL
https://ia.cr/2006/254
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.