MegoSAT.
Differential cryptanalysis
with SAT solvers.

MegoSAT homepage

About

Consider hash algorithms MD4 (48 rounds) and SHA-256 (64 rounds). We took two instances of one algorithm which were give slightly different inputs. At the same time we claim that the output difference between both instances is none. This technically constitutes a hash collision (two different inputs yield the same output in a hash function). It was the SAT solver's task to determine all intermediate values (and sometimes even parts of the input message).

And our attack setting was successful! We found full-round hash collisions in MD4 and round-reduced (up to 24 rounds) SHA-256. However, we tweaked the SAT encoding to actually be able to solve up to 24 rounds. My thesis discusses those tweaks.

As a side project, I also analyzed a huge amount of CNF files for SAT features.

The thesis

title Differential cryptanalysis with SAT solvers
advisors Florian Mendel, Maria Eichlseder
author Lukas Prokop
published August 2016
PDF file (600 kB)

Alternative downloads:

Subprojects

My master thesis features many subprojects, which are published on their own at various places on the WWW.

Benford's law

I verified Benford's law for DIMACS CNF files. Because I can.

cnf-analysis

I analyzed CNF files for SAT features. I released python and Go implementations.

Pure python hash algorithms

I adjusted pure python hash algorithm implementations to the newest py3k release.

algotocnf

The implementation generating CNF files for given algorithm implementations.

testcases

Testcases for our MD4 and SHA-256 attacks as well as CNF files for cnf-analysis.

Miscellaneous