Thanks for explaining! I just can't understand how such 'solvers' can help with crypto, when strong crypto-algos are not reversible and hence there is no point to approach them backwards?
If any algorithm can be weakened by such 'problem solvers', it wouldn't be considered strong? For instance, can SHA256 be reversed (i.e. collision found) faster with such a solver? I guess not..
I realize that with crypto, solvers can optimize the flow of the algorithm, make it more efficient and omit repeating some code parts, but a good bruteforcer written in assembly can be as optimized..?
SAT solvers can solve logical problems much faster than brute force. They take advantage of heuristics, and they use certain mathematical techniques to rule out parts of the search space and narrow it down significantly.
In general most crypto can't be broken by solvers. The solvers might be faster than brute force, but still take exponential amounts of time to solve it. However if the crypto was designed badly, there can be weaknesses in it that the solvers can find and exploit.
It's basically like those logic puzzles that are sometimes asked to kids. I don't have a specific example handy, but they go like "Fred won't sit next to Bill. Bill wants to sit next to Mary. Mary wants to sit in the same table as Ned..." And then they ask you to find a seating arrangement that satisfies all these constraints.
You can try every possibility, and there are exponentially many as you add more people. But if you are clever, you can realize certain constraints rule out large portions of the search space. Like you know the answer must have Mary in the same table as Ned, so you don't even try any possibilities where that's not true. There are many other clever tricks SAT solvers use to shrink the search space.
Crypto algorithms are deterministic, and therefore reversible. Solvers would work with any crypto, it's just that with normal crypto your computer would degrade to dust before they had time to finish. This was breakable because the Salsa algorithm was processing 16 bits instead of 32, which makes the set of possible earlier states astronomically smaller.
A "properly" implemented 16 bit Salsa20 would have 64/128 bits of key, which would still take a very long time to break. The reason _this_ implementation was broken (assuming the referenced snippet [1] is accurate) is the rotl function and the rotation values. The shifts are being calculated for 32 bits but are being used with 16 bit values. Instead of all 16 bits being rotated and used, half the shifts result in 0 while the others affect only a handful of high bits, which means there is very little diffusion going on.
I think the misunderstanding is just definitional, if you're searching on a constrained-space it wouldn't be called brute-force, though by all means you are still enumerating possible solutions.
> Brute force search should not be confused with backtracking, where large sets of solutions can be discarded without being explicitly enumerated *
If any algorithm can be weakened by such 'problem solvers', it wouldn't be considered strong? For instance, can SHA256 be reversed (i.e. collision found) faster with such a solver? I guess not..
I realize that with crypto, solvers can optimize the flow of the algorithm, make it more efficient and omit repeating some code parts, but a good bruteforcer written in assembly can be as optimized..?