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.
|title||Differential cryptanalysis with SAT solvers|
|advisors||Florian Mendel, Maria Eichlseder|
- Black/white version (except for first 2 pages, print version)
- Presentation slides
- Presentation slides (long version)
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.
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.
The implementation generating CNF files for given algorithm implementations.
- algotocnf on github
- statistics retrieved for our testcases
Testcases for our MD4 and SHA-256 attacks as well as CNF files for cnf-analysis.