In this research, we consider the problems of searching for collisions in cryptographic hash functions from the MD family as variants of the Boolean Satisfiability problem (SAT). To construct the SAT encodings for MD4 and MD5 algorithms, we employ the Transalg system designed to automatically transform algorithmic descriptions of discrete functions to Boolean equations. For hash functions under consideration, the SAT encodings are much more compact than known analogues, because the several additional constraints based on the known differential attacks on these functions are used in these encodings. The solving time for the SAT instances, encoding the search for single block collisions for MD4, is on average less than 1 sec on an usual PC. To solve the SAT instances, encoding the search for two-block collisions for MD5, we employed parallel SAT solvers working on the computing cluster. As a result, we found a class of two-block collisions for MD5 with the first 10 zero bytes. We constructed several dozens of collisions of the proposed kind. Also, we considered the inversion problem for the MD4 hash function (the search for the preimage for a given hash value). To solve this problem, we developed a technique relying on the so called variables. Each switch variable is responsible for an additional constraint on several Boolean variables included in the SAT encoding. If a switch variable takes the value of Truth then the corresponding constraint becomes enabled and should be taken into account by the SAT solving algorithm. Otherwise this constraint remains inactive. The use of switch variables made it possible to find new additional constraints (similar to Dobbertin's constraints) and to improve the effectiveness of solving the inversion problem for 39-step MD4 by a hundredfold.

The authors share their experience in organizing volunteer computing projects for solving problems that imply massive coarse-grained parallelism. Details and features of this process are illustrated using real functioning projects OPTIMA@home and SAT@home as examples. Both projects are based on the BOINC platform. The former is used to solve global optimization problems and the latter – to solve combinatorial problems reduced to Boolean satisfiability problems (SAT).

The article i s devoted to converting combinatorial problems into the problems of solving Boolean equations. Some theoretical results are presented as the basis of technology for propositional encoding of algorithms calculating discrete functions. Software system Transalg implementing the technology is described. Examples of using the Transalg for translating cryptoanalysis algorithms to SAT-problem are presented. The technics for translating 0-1-ILP optimization algorithms into SAT are considered too.

A technology for translating different combinatorial problems to the tasks of finding solutions of logical (Boolean) equations is presented. Theoretical possibility of translations of that sort was shown by S. Cook in 1971. The report is expected to describe in detail Transalg the new translator of algorithms to the propositional logic. Unlike previous developments this translator allows obtaining propositional encodings for algorithms computing arbitrary everywhere defined Register Machine-computable discrete functions. Actually a program computing this function should be written in a special high level (C-like) language. Translator was used for obtaining propositional encodings of some encryption algorithms, algorithms describing functioning the gene networks of a certain class and for translating the problems from 0-1 ILP to SAT.