This paper investigates the power of SAT solvers in cryptanalysis. The contributions are two-fold and are relevant to both theory and practice. First, we introduce an efficient, generic and automated method for generating SAT instances encoding a wide range of cryptographic computations. This method can be used to automate the first step of algebraic attacks, i.e. the generation of a system of algebraic equations. Second, we illustrate the limits of SAT solvers when attacking cryptographic algorithms, with the aim of finding weak keys in block ciphers and preimages in hash functions. SAT solvers allowed us to find, or prove the absence of, weak-key classes under both differential and linear attacks of full-round block ciphers based on the International Data Encryption Algorithm (IDEA), namely, WIDEA-n for
, and MESH-64(8). In summary: (i) we have found several classes of weak keys for WIDEA-n and (ii) proved that a particular class of weak keys does not exist in MESH-64(8). SAT solvers provided answers to two complementary open problems (presented in Fast Software Encryption 2009): the existence and non-existence of such weak keys. Although these problems were supposed to be difficult to answer, SAT solvers provided an efficient solution. We also report on experimental results about the performance of a modern SAT solver as the encoded cryptanalytic tasks become increasingly hard. The tasks correspond to preimage attacks on reduced MD4 algorithm.
