[SOLVED] Z3 Constraint solver for hashing operations

Z3 Constraint solver for hashing operations

I'm attempting to solve a python lambda expression using Z3.

    flippy = lambda x: bytes.fromhex((m := x.encode().hex())[1::2] + m[::2])
    check = lambda x, y: False if not all(
        f(flippy(x)).hexdigest().startswith(g) for f, g in
        zip([md5, sha1, sha256, sha384, sha256], y.split("-"))) else True

My attempt at creating a solver looks something like this;

for i, algorithm in enumerate(hash_algorithms):
    solver.add(algorithm(bytes.fromhex((m := x.encode().hex())[1::2] + m[::2])).hexdigest().startswith(y[i:i+5]))
    i += 5

However this gives me this error;

Traceback (most recent call last):
  File "I:\test.py", line 33, in <module>
    solver.add(algorithm(bytes.fromhex((m := name.encode().hex())[1::2] + m[::2])).hexdigest().startswith(secret[i:i+5]))
AttributeError: 'SeqRef' object has no attribute 'encode'

I'm very much a beginner to Z3, but how can I add a encode and hashing constraints to Z3?

Solution

Z3 (or any constraint solver for that matter) cannot reverse-execute any hash-algorithm worthy of its salt (pun intended!)

This sort of question comes up often, where we'd like to find if there are hash-collisions, or find a key out of a plaintext-ciphertext pair etc. No real "sanctioned" algorithm (i.e., SHA-2/3, MD5, RC4, AES etc.) can be broken this way. In fact, the only time I know this was successful was because the algorithm had a deficiency, see: https://galois.com/blog/2011/06/zuc-in-cryptol/