Using SAT Solvers to Detect Contradictions in Di erential Characteristics
Lukáš Prokop · 2014
The NP-completeness of SAT has been proven in 1971 by Stephen Cook and under the assumption of P 6= NP , the problem is infeasible for large problem sizes. However, recent advances in the field of SAT solver design make large SAT problems solvable on an industrial level if enough computational resources are provided. At the same time, hash algorithms’ collision resistance depends on the computational complexity of the algorithm which has successfully been reduced by Wang et al. Combining those techniques we might be able break the security of modern hash algorithms. In this bachelor’s thesis we present an implementation for performing (partial) SAT-based attacks on hash algorithms by evaluating the satisfiability of differential characteristics. We evaluate three possible CNF encodings for this problem.