text: In the present paper we describe the technology for translating algorithmic descriptions of discrete functions to SAT. The proposed technology is aimed at applications in algebraic cryptanalysis. We describe how cryptanalysis instances are reduced to SAT in such a way that it should be perceived as natural by the cryptographic community. Therefore, in the theoretical part of the paper we justify the main principles of general reduction to SAT for discrete functions from a class containing the majority of functions employed in cryptography. Based on these principles we describe the Transalg software system, developed with SAT-based cryptanalysis specifics in mind. We show the results of applications of Transalg to construction of a number of attacks on various cryptographic functions. Some of the corresponding attacks are state of the art. We also compare the functional capabilities of the proposed system with that of other software systems that can be used to reduce cryptanalysis instances to SAT, and also with the CBMC system widely employed in symbolic verification. In the paper we also present vast experimental data, obtained using the SAT-solvers that took first places at the SAT-competitions in the recent several years.
  @cite_99: In 2010, Tao Xie and Dengguo Feng [XF10] constructed the rst single-block collision for MD5 consisting of two 64-byte messages that have the same MD5 hash. Details of their attack, developed using what they call an evolutionary approach, has not been disclosed security reasons". Instead they have posted a challenge to the cryptology community to nd a new dierent single-block collision attack for MD5. This paper answers that challenge by presenting a single-block collision attack based on other message dierences together with an example colliding message pair. The attack is based on a new collision nding algorithm that exploits the low number of bitconditions in the rst round. It uses a new way to choose message blocks that satisfy bitconditions up to step 22 and additionally uses three known tunnels to correct bitconditions up to step 25. The attack has an average runtime complexity equivalent to 2 49:8 calls to MD5’s compression function.
  @cite_78: Hash functions are important cryptographic primitives which map arbitrarily long messages to fixed-length message digests in such a way that: (1) it is easy to compute the message digest given a message, while (2) inverting the hashing process (e.g. finding a message that maps to a specific message digest) is hard. One attack against a hash function is an algorithm that nevertheless manages to invert the hashing process. Hash functions are used in e.g. authentication, digital signatures, and key exchange. A popular hash function used in many practical application scenarios is the Secure Hash Algorithm (SHA-1). In this thesis we investigate the current state of the art in carrying out preimage attacks against SHA-1 using SAT solvers, and we attempt to find out if there is any room for improvement in either the encoding or the solving processes. We run a series of experiments using SAT solvers on encodings of reduceddifficulty versions of SHA-1. Each experiment tests one aspect of the encoding or solving process, such as e.g. determining whether there exists an optimal restart interval or determining which branching heuristic leads to the best average solving time. An important part of our work is to use statistically sound methods, i.e. hypothesis tests which take sample size and variation into account. Our most important result is a new encoding of 32-bit modular addition which significantly reduces the time it takes the SAT solver to find a solution compared to previously known encodings. Other results include the fact that reducing the absolute size of the search space by fixing bits of the message up to a certain point actually results in an instance that is harder for the SAT solver to solve. We have also identified some slight improvements to the parameters used by the heuristics of the solver MiniSat; for example, contrary to assertions made in the literature, we find that using longer restart intervals improves the running time of the solver.
  @cite_54: In this paper, we present a divide-and-conquer SAT solver, MapleAmpharos, that uses a novel propagation-rate (PR) based splitting heuristic. The key idea is that we rank variables based on the ratio of how many propagations they cause during the run of the worker conflict-driven clause-learning solvers to the number of times they are branched on, with the variable that causes the most propagations ranked first. The intuition here is that, in the context of divide-and-conquer solvers, it is most profitable to split on variables that maximize the propagation rate. Our implementation MapleAmpharos uses the AMPHAROS solver as its base. We performed extensive evaluation of MapleAmpharos against other competitive parallel solvers such as Treengeling, Plingeling, Parallel CryptoMiniSat5, and Glucose-Syrup. We show that on the SAT 2016 competition Application benchmark and a set of cryptographic instances, our solver MapleAmpharos is competitive with respect to these top parallel solvers. What is surprising that we obtain this result primarily by modifying the splitting heuristic.
  @cite_32: Inverting a function f at a given point y in its range involves finding any x in the domain such that f(x) = y. This is a general problem. We wish to find a heuristic for inverting those functions which satisfy certain statistical properties similar to those of random functions. As an example, we choose popular secure hash functions which are expected to be hard to invert and any successful strategy to do so will be quite useful. This provides an excellent challenge for SAT solvers. We first find the limits of inverting via direct encoding of these functions as SAT: for MD4 this is one round and twelve steps and for MD5 it is one round and ten steps. Then, we show that by adding customized constraints obtained by modifying an earlier attack by Dobbertin, we can invert MD4 up to 2 rounds and 7 steps in < 8 hours.
  @cite_95: In this article, we present a small, complete, and efficient SAT-solver in the style of conflict-driven learning, as exemplified by Chaff. We aim to give sufficient details about implementation to enable the reader to construct his or her own solver in a very short time.This will allow users of SAT-solvers to make domain specific extensions or adaptions of current state-of-the-art SAT-techniques, to meet the needs of a particular application area. The presented solver is designed with this in mind, and includes among other things a mechanism for adding arbitrary boolean constraints. It also supports solving a series of related SAT-problems efficiently by an incremental SAT-interface.
  @cite_15: In this paper we construct preimage attack on the truncated variant of the MD4 hash function. Specifically, we study the MD4-39 function defined by the first 39 steps of the MD4 algorithm. We suggest a new attack on MD4-39, which develops the ideas proposed by H. Dobbertin in 1998. Namely, the special relaxation constraints are introduced in order to simplify the equations corresponding to the problem of finding a preimage for an arbitrary MD4-39 hash value. The equations supplemented with the relaxation constraints are then reduced to the Boolean Satisfiability Problem (SAT) and solved using the state-of-the-art SAT solvers. We show that the effectiveness of a set of relaxation constraints can be evaluated using the black-box function of a special kind. Thus, we suggest automatic method of relaxation constraints generation by applying the black-box optimization to this function. The proposed method made it possible to find new relaxation constraints that contribute to a SAT-based preimage attack on MD4-39 which significantly outperforms the competition.
  @cite_58: This paper proposes several approaches to improve the collision attack on MD4 proposed First, we propose a new local collision that is the best for the MD4 collision attack. Selection of a good message difference is the most important step in achieving effective collision attacks. This is the first paper to introduce an improvement to the message difference approach of , where we propose a new local collision. Second, we propose a new algorithm for constructing differential paths. While similar algorithms have been proposed, they do not support the new local collision technique. Finally, we complete a collision attack, and show that the complexity is smaller than the previous best work.
  @cite_25: 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.
  @cite_82: 
summary: As we already noted, @cite_25 was the first paper to demonstrate the applicability of SAT-based cryptanalysis to relevant cryptographic algorithms. In that paper using the solver @cite_95 it was possible to quite effectively find single-block collisions for MD4. Using new propositional encoding methods (in particular, the system) and state-of-the-art SAT solvers it is possible to find preimages for MD4 and MD5 several hundred times faster than it was done in @cite_25 . Nevertheless, on the current stage SAT-based cryptanalysis is less effective than specialized methods (see, for example @cite_58 @cite_99 @cite_82 ) on problems of finding collisions of cryptographic hash functions. However, as far as we know, it is the SAT-based approach that yields best known preimage attacks on truncated variants of hash functions @cite_32 @cite_78 @cite_54 . In application to MD4-39 for a long time the SAT-based preimage attack from @cite_32 was considered to be the best. In @cite_15 we significantly improved the results from @cite_32 . It was possible for the large part thanks to functional capabilities of the system.