| Meno: | Ladislav
|
|---|
| Priezvisko: | Pápay
|
|---|
| Názov: | Use of SAT Solvers in Cryptanalysis
|
|---|
| Vedúci: | doc. RNDr. Martin Stanek, PhD.
|
|---|
| Rok: | 2016
|
|---|
| Blok: | INF
|
|---|
| Kµúčové slová: | SAT, cryptography, hash functions, heuristics
|
|---|
| Abstrakt: | SAT solvers are a universal tool for finding solutions to boolean satisfiability problems.
In the past they have also been used for cryptographic problems, such as finding
preimages for hash functions or obtaining the key for stream ciphers. However these
solutions are not easily reusable or modifiable and require significant effort to produce
the programs that create the SAT instances.
To avoid these issues we create a modeling library that allows simple creation of
SAT instances. While we focus specifically on various problems related to cryptographic
hash functions, the library is generic enough that it can be used for other purposes as
well.
Using this library we create models for several cryptographic hash functions. Various
SAT solvers, optimizations and heuristics are evaluated on these models to compare
their performance. These include the use of the Espresso logic minimizer to reduce the
instance size, forcing custom variable branching order with help of modified SAT solvers
and others.
|
|---|