Abstract
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
reduced-difficulty 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.