Názov:Use of SAT Solvers in Cryptanalysis
Vedúci:doc. RNDr. Martin Stanek, PhD.
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.

Súbory diplomovej práce: