-
Notifications
You must be signed in to change notification settings - Fork 1
/
intro.tex
32 lines (28 loc) · 1.9 KB
/
intro.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
Hash algorithms are ubiquitous in our world of digital communication.
Using hash algorithms we can verify data integrity of messages with high
probability without transmitting the actual message for example. Fundamentally
hash algorithms take arbitrary input data and return a hash value of fixed
size specific for this input. In cryptology the security of cryptographic
systems depends on three properties of hash algorithms. One of them is called
collision resistance meaning that given a hash value it is computationally
infeasible to find two different inputs leading to the defined hash value.
SAT solvers are sophisticated tools to solve difficult mathematical problems
in the most efficient way. They take a boolean equation as input and tell
whether or not the logical system is consistent or not. This way it can tell
whether a particular state of the system is desirable or not; once it is
represented with boolean algebra.
In this bachelor's thesis we combine both ideas. We will use SAT solvers to
represent states in the hash algorithm evaluation. Given an intermediate
state of the evaluation, we consider additional assumptions which might
lead to the representation of a hash collision. We can use our implementation
to verify whether this assumption is a satisfiable state within the hash algorithm
specification. This way we are searching for collisions within the hash
algorithm starting with an intermediate state.
Our implementation is an extension of an existing framework for differential
cryptanalysis. We therefore do not represent the state of a hash algorithm
evaluation directly, but rather the difference between two instances evaluating
a hash algorithm. Hopefully in the end we can find two input values resulting
in the same hash value.
Additionally we introduce three encodings to represent the differential state
in boolean algebra to build a bridge between SAT solving and hash algorithm
cryptanalysis.