Applications of SAT Solvers in Cryptanalysis: Finding Weak Keys and Preimages

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 di↵erential and linear attacks  of full-round block ciphers based on the International Data Encryption Algorithm (IDEA),  namely, WIDEA-n for n 2 {4, 8}, and MESH-64(8). In summary: (i) we have found sev eral 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 per formance of a modern SAT solver as the encoded cryptanalytic tasks become increasingly  hard. The tasks correspond to preimage attacks on reduced MD4 algorithm.