Using Automatic Generation of Relaxation
Constraints to Improve the Preimage Attack on
39-step MD4
Irina Gribanova, Alexander Semenov

arXiv:1802.06940v1 [cs.AI] 20 Feb 2018

Matrosov Institute for System Dynamics and Control Theory SB RAS, Irkutsk, Russia
Email: the42dimension@gmail.com, biclop.rambler@yandex.ru
Abstract—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.
Keywords—cryptographic hash functions; MD4; preimage attack; SAT; black-box optimization.

I. I NTRODUCTION
Cryptographic hash functions have a wide range of applications: starting from various data security [1] and cryptocurrency protocols [2] to theoretical methods for cryptographic
resistance justification of different cryptosystems [3], [4]. The
Merkle-Damgard construction [5], [6] is considered to be one
of the most successful paradigms for constructing cryptographically resistant hash functions. The MD4 hash function
[7] is one of the first examples of hash functions based on
the Merkle-Damgard construction. The widely known works
[8], [9] demonstrated the possibility of constructing collisions
for hash functions MD4 and MD5. Thus, these functions
have been compromised with respect to the collision attack.
However, today even MD4 remains resistant to the so called
preimage attack, which consists in the following: for a known
hash value to find a corresponding input message. In this
context, the implementation of preimage attacks on truncated
variants of MD4 hash function is of interest. The truncated
variant of the MD4 hash function is a variant of the original
algorithm, which contains fewer steps (non-truncated variant
consists of 48 steps). Hereinafter by MD4-k we denote a
truncated variant of MD4 with k steps, k < 48.
The first successful attack on truncated variant of MD4
with a relatively large number of steps was described by H.

Dobbertin in [10]. In this work it was showed that two-round
version of MD4, i.e. MD4-32, is not one-way. The main idea of
Dobbertin’s attack is to use additional constraints on chaining
variables at the certain steps of the MD4 algorithm to derive
additional information, which leads to fast resolution of the
corresponding cryptanalysis equations.
To the best of our knowledge, the attack described in [11]
is currently the best known attack on truncated variants of
MD4. This attack is a SAT-variant of Dobbertin’s attack which
used the constraints of Dobbertin’s type, in the sense that they
were applied to the same chaining variables as in [10]. The
resulting system of cryptanalysis equations was reduced to the
Boolean Satisfiability Problem (SAT) and then solved using
the MINISAT [12] SAT solver. For MD4-32 the SAT variant
of the Dobbertin’s attack turned out to be very effective. The
main novelty of [11] is to use Dobbertin’s constraints and
state-of-the-art SAT solvers to find preimages for MD4-k,
k = {36, 37, 39}, within a reasonable time. However, it should
be noted that the corresponding computational experiment for
MD4-39 took a lot of time (about 8 hours on one processor
core). In addition, in [11] only the hash values of special
kinds were considered. It is surprising that until 2017 there
was, apparently, no progress in the practical implementation
of the preimage attacks, which would be more effective than
the attack from [11].
In [13] we presented a parallel SAT-variant of Dobbertin’s
attack on MD4-k, k ≤ 39. One of the main results of [13]
is the automatic search procedure of Dobbertin’s constraints.
For MD4-39 it was achieved a relatively fast solving of the
preimage finding problem for the hash value 1128 (hereinafter
an denotes a word which consists of n a symbols).
In the present paper we improve the results from [13] in
the following directions. First, we consider the problem of
finding relaxation constraints of Dobbertin’s type as a problem
of black-box optimization over Boolean hypercube. To solve
this problem we develop metaheuristic algorithm related to
the class of Tabu Search algorithms. Using this algorithm
we construct new relaxation constraints of Dobbertin’s type
for the MD4-39 preimage finding problem. These constraints,
which are different from the ones presented in [10] and [11],
make it possible to find the MD4-39 preimages for 65-75%
of randomly generated 128-bit vectors within one minute of
the MINISAT 2.2 SAT solver runtime on a single processor core

Intel i7-3770K (3.5 GHz). Whereas using constraints from [10]
and [11] MINISAT 2.2 is not capable to solve these tasks in
several hours.
II. P RELIMINARIES
As it was mentioned above, the MD4 hash function is a
cryptographic hash function based on the Merkle-Damgard
construction. This hash function can be used to calculate hash
values for messages of an arbitrary length. The input message
is split into 512-bit blocks. The resulting hash value is written
in a special 128-bit register called hash register. The hash
register is divided into four parts of 32-bit length. According to
the Merkle-Damgard construction, the fixed Initial Value (IV)
is written to the hash register before hashing the first block
of input message. Further, the contents of the hash register is
iteratively modified. Thus, before hashing the 512-bit block
with number t + 1, the hash register contains the result of
hashing of message blocks with numbers from 1 to t. The
process of hashing of one 512-bit block is divided into 3
rounds with 16 steps each (thus, 48 steps in total). The contents
of the hash register is mixed with the input message using the
round functions. In total, MD4 uses three round functions,
detailed descriptions of which can be found in a variety of
sources (i.e. [8]). On each step with number k = 1, . . . , 48
a variable called chaining variable is associated with one of
four parts of the hash register.
Hereinafter, we consider the problem of finding preimage
(preimage attack) for the function of the kind:
fMD4−k : {0, 1}512 → {0, 1}128,

(1)

assuming that at the initial moment of time the hash register
contains IV, corresponding to the specification of MD4. In fact,
we consider the problem of finding 512-bit MD4-k preimage
for known 128-bit hash value. Herein the main object of
further interest is the function fMD4−39 .
Let us briefly recall the idea of the Dobbertin’s attack [10].
Based on the analysis of the round functions properties, H.
Dobbertin proposed to fix with constant K the values of certain
chaining variables corresponding to the steps of the algorithm
with numbers:
13, 14, 15, 17, 18, 19, 21, 22, 23, 25, 26, 27.

(2)

The substitution of corresponding values into the cryptanalysis equations makes it possible to derive a significant part
of the values of variables, which encode the unknown 512-bit
input message. This, in turn, leads to a further simplification
of the problem. As a result, in 1998 H. Dobbertin managed to
find preimages for the MD4-32 hash function on a personal
computer. We will refer to Dobbertin’s constraints to denote
the additional constraints of the form vi = K, where vi
is chaining variable at i-th step and i goes through the set
of numbers from (2). In general case, similar constraints on
various steps of the MD4 algorithm different from (2) can
be used. For all such constraints we use the term relaxation
constraints.

The next step is to use a powerful combinatorial algorithm
for solving the cryptanalysis equations with additional relaxation constraints. As it was mentioned above, this idea was
proposed in [11] where Dobbertin’s constraints were used with
constant K = 0 and the corresponding cryptanalysis equations
were solved using the MINISAT [12] SAT solver.
Let us recall, that SAT (short for ”Satisfiability”) is a
problem of satisfiability of an arbitrary Boolean formula,
which consists in the following: for an arbitrary formula F
over the set of Boolean variables X to decide if there exists
such an assignment of variables from X that makes this
formula true. It is usually considered in the variant where F
is presented in conjunctive normal form (CNF).
The approach in which modern SAT solvers are used
to solve cryptanalysis problems is called SAT-based cryptanalysis. To reduce the preimage finding problem (inversion
problem) of an arbitrary total discrete function of the kind
f : {0, 1}n → {0, 1}m to SAT one can use various automatic
translation systems, like C RYPTOL [14] or URSA [15]. In
our work we use software system T RANSALG [16] specially
designed to produce SAT encodings for the inversion problems
of cryptographic functions. T RANSALG performs a symbolic
execution [17] of a program, which specifies the considered
function f . The result of such execution is a CNF C(f )
called template CNF. By C(f, y) we denote the result of the
substitution of a known image y of function f , y ∈ Rangef ,
into CNF C(f ). It can be shown that C(f, y) is satisfiable.
Asumming that satisfying assignment for C(f, y) is found
using SAT solver, a preimage x ∈ {0, 1}n such that f (x) = y
can be extracted from this assignment. Using the methods of
SAT-based cryptanalysis to find preimages of cryptographic
hash functions is called a SAT-based preimage attack on this
function.
As it was mentioned above, in [13] the parallel version of
SAT-based preimage attack on MD4-k (k ≤ 39) from [11] was
proposed. However, in the role of relaxation constraints the
same Dobbertin’s constraints were used. In the next section we
consider the generation of relaxation constrains as a problem
of block-box optimization over Boolean hypercube. We also
present computational results obtained using new relaxation
constraints.
III. T HE

GENERATION OF RELAXATION CONSTRAINS AS A
PROBLEM OF BLACK - BOX OPTIMIZATION

Let us consider the preimage finding problem for the
function of the kind (1) with fixed k and reduce this problem
to SAT. Let C(fMD4−k ) be template CNF for this problem
and X be a set of all Boolean variables in C(fMD4−k ). By
C(fMD4−k , χ) we denote a CNF obtained by substitution of
a hash value χ ∈ {0, 1}128 into C(fMD4−k ).
Below we briefly describe the idea of switching variables
introduced in [13]. Suppose that there is some set of relaxation
constraints ℜ = {R1 , . . . , RQ }, where an arbitrary constraint
Rj , j ∈ {1, . . . , Q} is usually a conjunction of some literals,
i.e. a formula of the kind:
l1 (xj1 ) ∧ . . . ∧ ltj (xjtj ), {xj1 , . . . , xjtj } ⊆ X

(3)

(note that literal l(x) is a formula of the kind x or ¬x, where
x is a Boolean variable).
Consider a new set of Boolean variables S = {s1 , . . . , sQ },
S ∩ X = ∅. We call such variables switching variables. Let
us associate with an arbitrary Rj , j ∈ {1, . . . , Q} of the kind
(3) the following CNF:
CRj = (¬sj ∨ l1 (xj1 )) ∧ . . . ∧ (¬sj ∨ ltj (xjtj )).
It should be noted that the literals l1 (xj1 ), . . . , ltj (xjtj ) can
be derived from CNF sj ∧ CRj using the Unit Propagation
(UP) rule [18]. Then, this new information will be further
propagated according to UP. On the other hand, it’s obvious
that ¬sj ∧ CRj ≡ ¬sj . In this case the constraint Rj does not
give any additional information. We say that the constraint Rj
is active if sj = 1 and inactive if sj = 0.
Let S be the set of switching variables. The set of all
possible values of variables from S is {0, 1}Q. Thus, each
nonzero Boolean vector λ ∈ {0, 1}Q specifies some set of
active relaxation constraints from set ℜ. Our first goal is to
learn how to distinguish more effective sets of relaxation constraints from less effective ones (in the sence of increasing the
efficiency of the corresponding SAT-based preimage attack).
To solve this problem we use the approach similar to that
applied in [19], [20] for searching SAT partitionings [21] of
SAT-instances arising in cryptanalysis problems. In particular,
we introduce a measure of efficiency for an arbitrary set of
relaxation constraints from ℜ and consider the problem of
finding sets of relaxation constrains with good efficiency as a
problem of maximization of a specially defined function over
Boolean hypercube {0, 1}Q .
The problem of choosing the adequate measure of efficiency
for relaxation constraints is quite non-trivial. At this stage,
after a large number of experiments, the measure was defined
as follows. Consider an arbitrary vector λ ∈ {0, 1}Q, where
{λh1 , . . . , λhd } is a set of components equal to 1. Taking into
account the above, these components define a set of active
relaxation constraints from ℜ = {R1 , . . . , RQ }, namely, the
constraints with numbers h1 , . . . , hd . Consider the following
CNF:
C̃(λ) = C(fMD4−k , χ) ∧ (∧j∈{h1 ,...,hd } CRj ).

(4)

Everywhere below, we will use notation C̃(λ) →UP l(x)
to denote that literal l(x) is derived from CNF (4) using
UP. By X in ⊂ X we denote a set of Boolean variables in
C(fMD4−k , χ), which encode an unknown 512-bit input of
fMD4−k function.
For an arbitrary λ ∈ {0, 1}Q we consider the function:
µ(λ) = #{l(x)|C̃(λ) →UP l(x) : x ∈ X in }.

(5)

In other words µ(λ) is the number of literals from X in , which
were derived by UP from CNF (4) as a result of activation of
relaxation constraints corresponding to vector λ.
We will consider the maximization problem of (5) over
Boolean hypercube {0, 1}Q. It’s obvious that function (5)
is a function of black-box type and its analitical properties

are unknown. Thereby it is justified to use metaheuristic
algorithms for the maximization problem of (5). At this stage,
we implemented a special variant of Tabu Search algorithm
[22]. In the computational experiments, discussed further, we
considered the Hamming neighborhoods of the radius 1 in
{0, 1}Q. The pseudocode of the algorithm is presented below.
Algorithm 1 Tabu Search Algorithm (A1)
1: hλcenter , µbest i ← hλstart , µ(λstart )i
2: initializeLists(L1 , L2 )
3: repeat
4:
bestValueUpdated ← false
5:
repeat
6:
λ ← getNewPoint(N (λcenter ))
7:
markPointInTabuLists(λ, L1, L2 )
8:
if isCorrectPoint(λ) then
9:
compute µ(λ)
10:
if µ(λ) > µbest then
11:
hλbest , µbest i ← hλ, µ(λ)i
12:
bestValueUpdated ← true
13:
end if
14:
end if
15:
until N (λcenter ) is checked
16:
if bestValueUpdated then
17:
λcenter ← λbest
18:
else
19:
λcenter ← getNewCenter(L2)
20:
end if
21: until timeExceeded() or L2 = ∅
22: return hλbest , µbest i
Let us give more detailed description of the A1 algorithm.
The input of A1 algorithm is CNF C(fMD4−39 , χ) encoding
the MD4-39 preimage finding problem for a known hash value
and starting point λstart with a corresponding set of relaxation
constraints of the kind (3). As a starting point, either a random
point or some known point can be chosen. The contents of the
L1 and L2 lists are initialized using function initializeLists.
At the initial moment the L1 list is empty, L2 contains point
λstart , λcenter is equal to λstart and µbest is the value of the
objective function µ(λstart ).
In the main loop of the algorithm the neighborhood of the
point λcenter , denoted by N (λcenter ), is considered. Function
getNewPoint chooses any unchecked point from N (λcenter ) as
a current point λ. Function markPointInTabuLists adds point
λ to L2 and then marks λ as checked in all neighborhoods
of points from L2 which contain λ. This allows to avoid reprocessing of the same points. If the neighborhood of some
point contains only checked points, then this point is moved
to L1 .
For current point λ and corresponding CNF C̃(λ) of the
kind (4) function isCorrectPoint runs a SAT solver for a short
period of time. If, as the result, CNF C̃(λ) is proven to be
unsatisfiable, then the algorithm moves to the next point from
the neighborhood N (λcenter ). Otherwise, the value µ(λ) is
computed and compared with the value µbest .

In case if we did not improve µbest value in the neighborhood of λcenter , new point λcenter must be selected from L2 .
Function getNewCenter chooses a point from L2 with a value
of the objective function which is closest to the known µbest .
The algorithm is completed if a certain time limit is exceeded or the entire search space is processed (in this case L2
is empty). The output of the algorithm is the point λbest and
the corresponding value of the objective function µ(λbest ).
IV. C OMPUTATIONAL EXPERIMENTS
In this section we describe computational results for MD439 preimage attack using the method of relaxation constraints
generation described above. At the current stage, the A1
algorithm is implemented as a single-threaded application. To
calculate the value of the function (5) the Unit Propagation
procedure, implemented in all modern CDCL solvers, is used.
Everywhere below, the constraints of the kind (3), consisting
only of literals with negation, were used as relaxation constraints. Thus, we used constraints of Dobbertin’s type with
constant K = 0.
Let us note here that the structure of the MD4-39 hash
function makes it impossible to impose constraints on the first
four and the last (preceding the calculation of the final hash
value) four steps of the MD4-39 algorithm. According to this,
the sets of new relaxation constraints were selected (using the
values of the corresponding switching variables) from the set
ℜ of power Q = 31. Thus, the problem of maximization of the
function (5) over Boolean hypercube {0, 1}31 was considered.
In the early experiments it was found that some sets of
relaxation constraints produce CNFs, for which the UNSAT
can be proven quite quickly (within a few seconds). In
practical implementation of the algorithm for each set of
values of switching variables that specifies a set of relaxation
constraints, not only the value of function (5) was calculated,
but also short time limit was given to solve the corresponding
SAT instance. This step allows to screen out some points
without the computation of the objective function.
In the A1 algorithm the following actions are performed:
selection of starting search point; screening out the points for
which unsatisfiability is proven quickly; accumulation of all
record points; exit from local maxima.
The A1 algorithm was run on one core of Intel i7-3770K
(3.5 GHz) processor under Linux OS (Ubuntu 16.04). In
all computational experiments the MD4-39 preimage finding
problem for χ = 0128 was considered. For the points, obtained
using the A1 algorithm, with the value of the objective
function close to the maximal possible value (i.e. 512), we
established that corresponding sets of relaxation constraints
define unsatisfiable CNFs. The satisfiability problems of such
CNFs were considered as a separate problems, which in some
cases required a significant amount of time. Thus, it was
necessary to select points from {0, 1}31 for which there was
a good chance for the corresponding CNF of the kind (4) to
be satisfiable. To find such points the following heuristic was
used: first, to select only those points where the value of the
function µ(λ) was improved (i.e., record points); second, to

select the points with the value of the function µ(λ) from
the interval [256, 320]. The total number of record points
from the number of all points processed in several hours was
approximately 2%. The total number of perspective points
identified by the heuristic described above was 0.5%. For each
point from the perspective set of points the MINISAT 2.2 SAT
solver was applied to the corresponding CNFs with a small
time limit (60 seconds).
As a result of the above actions, two new sets of relaxation
constraints were obtained. These sets are specified by the following vectors of values of switching variables from {0, 1}31:
ρ1 : 0000000001101110111011101000000
ρ2 : 0000000000101110111011101100000
The application of these sets allows one to find preimages
of the MD4-39 hash function for known hash values 0128
and 1128 within a minute of MINISAT 2.2 runtime (whereas
using constraints from [11] the solution of the preimage
finding problem for 1128 requires about 2 hours, and the
preimage finding problem for 0128 cannot be solved in 8
hours). Corresponding results are presented in Table I, where
ρDe denotes the set of relaxation constraints described in [11]
and ρDobbertin denotes the variant of Dobbertin’s constraints
from [10] with constant K = 0. Below these relaxation
constraints are specified by the vectors of values of switching
variables from {0, 1}31 (in the similar notation to that of ρ1
and ρ2 ):
ρDobbertin : 0000000011101110111011100000000
ρDe :
0000000001101110111011100000000
What is particularly interesting is that the application of
new sets of relaxation constraints ρ1 and ρ2 also allows one
to find preimages of MD4-39 for randomly generated 128-bit
hash values persistently. To obtain this result, we considered
a test set consisting of 500 randomly generated vectors from
{0, 1}128. Each vector from this set was taken as a hash value
of the MD4-39 hash function. After that the preimage finding
problem for this value was solved using constraints ρ1 and
ρ2 . For the prevailing part of the tasks (65-75%) the solutions
were successfully found using the MINISAT 2.2 SAT solver.
The average time of finding one preimage was less than 1
minute. The rest ones (25-35% of the tasks) corresponded to
128-bit vectors for which there were no MD4-39 preimages
under constraints ρ1 and ρ2 . These results are presented in
Table II. Note that even in a few hours we did not manage to
solve the preimage finding problem for any vector from the
test set using constraints from [10] or [11].
V. C ONCLUSION
In the present paper a new SAT-based preimage attack on
the 39-step variant of the MD4 cryptographic hash function
is suggested. This attack makes it possible to solve the MD439 preimage finding problem for a very significant percentage of randomly generated 128-bit vectors, spending on one
such vector less than a minute of MINISAT 2.2 runtime. The
proposed attack is much more effective than the best known

TABLE I
F INDING THE MD4-39 PREIMAGES FOR HASH VALUES 0128
Relaxation
constraints

µ(λ)

ρ1
ρ2
ρDobbertin
ρDe

288
288
288
256

AND 1128

Solving time (s)
χ = 0128

χ = 1128

20
60
20
> 8 hours

10
UNSAT
> 8 hours
7000

TABLE II
F INDING THE MD4-39 PREIMAGES FOR 500 RANDOMLY GENERATED
128- BIT HASH VALUES
Relaxation
constraints

Avg.
solving
time (s)

Max.
solving
time (s)

ρ1
ρ2

12
46

80
250

Solved instances (in % of total
number of instances)
with preimages
with no preim(SAT)
ages (UNSAT)
65
35
75
25

attack on the considered truncated variant of the MD4 hash
function presented about 10 years ago in [11].
We intend to develop the approach described in this paper
in the direction of studying the preimage finding problem of
MD4-k, where k ≥ 40. The preliminary results show that
the corresponding problem for MD4-40 demands significantly
more computational resources in comparison with MD4-39:
the relaxation constrains constructed using the method described in this paper do not make it possible to solve the MD440 preimage finding problem on a single processor core. At the
same time, this effect is not observed between the preimage
attacks on MD4-38 and MD4-39. In the nearest future we plan
to apply the parallel SAT solvers to the inversion problems of
MD4-k, k ≥ 40 with relaxation constraints constructed using
the method presented in this paper.
VI. R ELATED W ORK
The first mention of the approach to the construction of
hash functions, which is widely known today as the MerkleDamgard construction, can be found in [23]. In [5] and
[6] R. Merkle and I. Damgard independently described a
number of important properties of hash functions based on
this construction. One of the first practical implementations
of Merkle-Damgard construction was the MD4 hash function
[7] developed by R.Rivest. In [8] the MD4 hash function
was completely compromised with respect to the collision
attack. The collision search problem for the functions from
MD family in the form of SAT was first proposed in [24].
However, real practical results in this direction were obtained
later in [25]. The use of propositional encodings presented in
[16] made it possible to find collisions for MD4 hash function
(with the help of modern SAT solvers) about 1000 times faster
than it was done in [25].
In a number of works the resistance of MD4 hash function to
the preimage attack was studied. Today it is generally accepted
that MD4 is not resistant to the preimage attack, although
the best known preimage attack on the full-round version of

MD4 is theoretical [26]. The first practical preimage attack on
truncated variant of MD4 was implemented by H.Dobbertin:
the algorithm presented in [10] allows one to find preimages
of MD4-32 on a personal computer. As far as we know,
in the last 10 years the best practical attack on truncated
variants of MD4 was attack described in [11]. In this attack
the MINISAT [12] SAT solver was used to find preimages of
MD4-39 weakened by the additional constraints. In the present
paper we significantly improve the results presented in [11].
ACKNOWLEDGMENT
The research was funded by Russian Science Foundation
(project No. 16-11-10046).
R EFERENCES
[1] B. Schneier, Applied Cryptography - Protocols, Algorithms, and Source
Code in C, 2nd Edition. Wiley, 1996.
[2] S. Nakamoto, “Bitcoin: A peer-to-peer electronic cash system.”
[Online]. Available: http://bitcoin.org/bitcoin.pdf
[3] D. Pointcheval and J. Stern, “Security arguments for digital signatures
and blind signatures,” Journal of Cryptology, vol. 13, no. 3, pp. 361–396,
2000.
[4] N. Koblitz and A. J. Menezes, “The random oracle model: A twenty-year
retrospective,” Des. Codes Cryptography, vol. 77, no. 2-3, pp. 587–610,
2015.
[5] R. C. Merkle, “A certified digital signature,” in Advances in Cryptology
- CRYPTO ’89, Proceedings, ser. Lecture Notes in Computer Science,
G. Brassard, Ed., vol. 435. Springer, 1989, pp. 218–238.
[6] I. Damgård, “A design principle for hash functions,” in Advances in
Cryptology - CRYPTO ’89, Proceedings, ser. Lecture Notes in Computer
Science, G. Brassard, Ed., vol. 435. Springer, 1989, pp. 416–427.
[7] R. L. Rivest, “The MD4 message digest algorithm,” in Advances in
Cryptology - CRYPTO ’90, Proceedings, ser. Lecture Notes in Computer
Science, A. Menezes and S. A. Vanstone, Eds., vol. 537. Springer, 1990,
pp. 303–311.
[8] X. Wang, X. Lai, D. Feng, H. Chen, and X. Yu, “Cryptanalysis of
the hash functions MD4 and RIPEMD,” in Advances in Cryptology
- EUROCRYPT 2005, Proceedings, ser. Lecture Notes in Computer
Science, R. Cramer, Ed., vol. 3494. Springer, 2005, pp. 1–18.
[9] X. Wang and H. Yu, “How to break MD5 and other hash functions,” in
Advances in Cryptology - EUROCRYPT 2005, Proceedings, ser. Lecture
Notes in Computer Science, R. Cramer, Ed., vol. 3494. Springer, 2005,
pp. 19–35.
[10] H. Dobbertin, “The first two rounds of MD4 are not one-way,” in
Fast Software Encryption, ser. Lecture Notes in Computer Science,
S. Vaudenay, Ed. Springer Berlin Heidelberg, 1998, vol. 1372, pp.
284–292.
[11] D. De, A. Kumarasubramanian, and R. Venkatesan, “Inversion attacks
on secure hash functions using SAT solvers,” in Theory and Applications
of Satisfiability Testing - SAT 2007, Proceedings, ser. Lecture Notes in
Computer Science, J. Marques-Silva and K. A. Sakallah, Eds., vol. 4501.
Springer, 2007, pp. 377–382.
[12] N. Eén and N. Sörensson, “An extensible SAT-solver,” in SAT, ser.
Lecture Notes in Computer Science, E. Giunchiglia and A. Tacchella,
Eds., vol. 2919. Springer, 2003, pp. 502–518.
[13] I. Gribanova, O. Zaikin, I. Otpuschennikov, and A. Semenov, “Using
parallel SAT solving algorithms to study the inversion of MD4 hash
function,” in Parallel Computing Technologies, PCT 2017, Kazan,
Russia, April 3-7, 2017, Proceedings, 2017, pp. 100–109.
[14] L. Erkök and J. Matthews, “Pragmatic equivalence and safety checking
in Cryptol,” in Proceedings of the 3rd ACM Workshop Programming
Languages meets Program Verification, PLPV 2009, Savannah, GA,
USA, 2009, pp. 73–82.
[15] P. Janicic, “URSA: a system for uniform reduction to SAT,” Logical
Methods in Computer Science, vol. 8, no. 3, pp. 1–39, 2012.

[16] I. Otpuschennikov, A. Semenov, I. Gribanova, O. Zaikin, and
S. Kochemazov, “Encoding cryptographic functions to SAT using
Transalg system,” in ECAI 2016, Proceedings, ser. Frontiers in Artificial
Intelligence and Applications, G. A. Kaminka, M. Fox, P. Bouquet,
E. Hüllermeier, V. Dignum, F. Dignum, and F. van Harmelen, Eds.,
vol. 285. IOS Press, 2016, pp. 1594–1595.
[17] J. C. King, “Symbolic execution and program testing,” Commun. ACM,
vol. 19, no. 7, pp. 385–394, 1976.
[18] W. F. Dowling and J. H. Gallier, “Linear-time algorithms for testing
the satisfiability of propositional horn formulae,” The Journal of Logic
Programming, vol. 1, no. 3, pp. 267–284, oct 1984.
[19] A. Semenov and O. Zaikin, “Using Monte Carlo method for searching
partitionings of hard variants of Boolean satisfiability problem,” in Parallel Computing Technologies, ser. Lecture Notes in Computer Science,
V. Malyshkin, Ed., vol. 9251. Springer International Publishing, 2015,
pp. 222–230.
[20] A. Semenov and O. Zaikin, “Algorithm for finding partitionings of hard
variants of Boolean satisfiability problem with application to inversion
of some cryptographic functions,” SpringerPlus, vol. 5, no. 1, pp. 1–16,
2016.
[21] A. E. J. Hyvärinen, “Grid based propositional satisfiability solving,”
Ph.D. dissertation, Aalto University, Helsinki, Finland, 2011.
[22] F. Glover and M. Laguna, TABU search. Kluwer, 1999.
[23] R. C. Merkle, “Secrecy, authentication, and public key systems,” Ph.D.
dissertation, Stanford University, Stanford, USA, 1979.
[24] D. Jovanovic and P. Janicic, “Logical analysis of hash functions,” in
Frontiers of Combining Systems, 5th International Workshop, FroCoS
2005, Proceedings, ser. Lecture Notes in Computer Science, B. Gramlich, Ed., vol. 3717. Springer, 2005, pp. 200–215.
[25] I. Mironov and L. Zhang, “Applications of SAT solvers to cryptanalysis
of hash functions,” in SAT, ser. Lecture Notes in Computer Science,
A. Biere and C. P. Gomes, Eds., vol. 4121. Springer, 2006, pp. 102–
115.
[26] G. Leurent, “MD4 is not one-way,” in Fast Software Encryption, ser.
Lecture Notes in Computer Science, K. Nyberg, Ed., vol. 5086. Berlin,
Heidelberg: Springer Berlin Heidelberg, 2008, pp. 412–428.

