International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Applications of SAT Solvers to Cryptanalysis of Hash Functions

Authors:
Ilya Mironov
Lintao Zhang
Download:
URL: http://eprint.iacr.org/2006/254
Search ePrint
Search Google
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.
BibTeX
@misc{eprint-2006-21747,
  title={Applications of SAT Solvers to Cryptanalysis of Hash Functions},
  booktitle={IACR Eprint archive},
  keywords={secret-key cryptography / hash functions, cryptanalysis, SAT solver},
  url={http://eprint.iacr.org/2006/254},
  note={Theory and Applications of Satisfiability Testing (SAT 06), pages 102--115, 2006 mironov@microsoft.com 13353 received 23 Jul 2006, last revised 24 Jul 2006},
  author={Ilya Mironov and Lintao Zhang},
  year=2006
}