MegoSAT homepage
About
Consider hash algorithms MD4 (48 rounds) and SHA256 (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 fullround hash collisions in MD4 and roundreduced (up to 24 rounds) SHA256. 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 
Alternative downloads:
 Black/white version (except for first 2 pages, print version)
 Presentation slides
 Presentation slides (long version)
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.
 cnfanalysis

I analyzed CNF files for SAT features. I released python and Go implementations.
 cnfanalysisgo on github
 cnfanalysispy on github
 cnfanalysistests2 on github
 Technical report “An average SAT problem” (TBD)
 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.
 algotocnf on github
 statistics retrieved for our testcases
 testcases

Testcases for our MD4 and SHA256 attacks as well as CNF files for cnfanalysis.
 STP CVC code for Testcase A
 ...
 Testcase A (one solution)
 Testcase B (one solution)
 Testcase C (one solution)
 Testcase 18 (one solution)
 Testcase 21 (one solution)
 Testcase 23 (one solution)
 Testcase 24 (one solution)
 download scripts for CNF files on github
 Miscellaneous

 “Introducing MegoSAT: Search for directions” (last update 2015.06.15, 900 kB)
 A goequivalent IPASIR interface [compare with SAT Race 2015] (last update 2015.06.20, 4 kB)
 A CLItool to analyse DIMACS files (last update 2015.08.07, 45 kB)