Inverting a function f at a given point y in its range involves finding any x in the domain such that f(x) = y. This is a general problem. We wish to find a heuristic for inverting those functions which satisfy certain statistical properties similar to those of random functions. As an example, we choose popular secure hash functions which are expected to be hard to invert and any successful strategy to do so will be quite useful. This provides an excellent challenge for sat solvers. We first find the limits of inverting via direct encoding of these functions as SAT: for md4 this is one round and twelve steps and for md5 it is one round and ten steps. Then, we show that by adding customized constraints obtained by modifying an earlier attack by Dobbertin, we can invert md4 up to 2 rounds and 7 steps in < 8 hours.
展开▼
