OT Crazy SAT encoding of md4 preimage

[Georgi Guninski <guninski () guninski com>]

Warning:  If you can break this probably you
can break md5 and sha1, so take care

Some people broke large SAT formulas [1] related
to a problem of Erdos with plingeling.

The md4 preimage encoding in SAT is much smaller.

The CNFs are https://j.ludost.net/md4crazy/

17b is 17 bytes preimage of zero hash.

32b is 32 bytes preimage of zero hash.

easy is 16 bytes something trivial. 
One solution is easy with the right solver, 
second solution differing in the first 128 vars 
is hard (if it exists).

Suggested solvers are plingeling and cryptominisat
(latest stable, for cryptominisat run
--restrict=256. plingeling is the parallel version of lingeling).

plingeling-ats:  http://fmv.jku.at/lingeling/
cryptominisat:   https://gforge.inria.fr/projects/cryptominisat/

Good luck ;)

[1] http://cgi.csc.liv.ac.uk/~konev/SAT14/

_______________________________________________
Sent through the Full Disclosure mailing list
http://nmap.org/mailman/listinfo/fulldisclosure
Web Archives & RSS: http://seclists.org/fulldisclosure/