Hacker News Reader

Comment by pbsd | Hacker News Reader

While SAT, and their cousin SMT, solvers are useful in the analysis of symmetric cryptographic primitives, they quickly become useless once the complexity of the problem hits a certain threshold. They are best employed to analyze contained parts of the primitive.

It can be wise to use a SAT solver to find a preimage of, e.g., SHA-256 reduced to 10 rounds. But it will be hopeless on the full function, unless it is severely broken.

View on HN

I think you misread the article. They are not claiming to break SHA, they are claiming they can get better than bruteforce performance on mining bitcoins.

I understand that. The author himself does not claim this approach is faster than bruteforce. Indeed, consider the converse: for mining using a SAT solver to be faster than bruteforce implies that the SAT solver is able to exploit some structure in the hash function which plain bruteforce has no access to. The point of a good hash function is to have no such structure.

If you additionally consider how SAT solving algorithms work, they are less amenable to modern CPUs than plain bruteforce, which can take full advantage of SIMD and instruction parallelism. If you look at password hash breakers, you will see them using extra tricks, like early abort, to speed things up even further.

>The point of a good hash function is to have no such structure.

Our hash functions are not perfect with respect to this.

That is equivalent to breaking SHA, if you consider a partial preimage attack a weakness, which I'd say many cryptographers do.

Reply on news.ycombinator.com