英文:
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 encoding and hashing constraints to Z3?
英文:
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?
答案1
得分: 1
Z3（或任何约束求解器）不能对任何值得一提的哈希算法进行逆向执行（讽刺意味！）
这类问题经常出现，我们想找出哈希碰撞，或者从明文-密文对中找到密钥等。没有真正“官方认可”的算法（如SHA-2/3、MD5、RC4、AES等）可以通过这种方式破解。实际上，我知道这种方法成功的唯一情况是因为算法存在缺陷，参见：https://galois.com/blog/2011/06/zuc-in-cryptol/
另外，当您在Stack Overflow上发布问题时，最好发布其他人可以运行的代码。您发布的代码片段无法独立运行，这会使理解和调试变得困难。请参考：https://stackoverflow.com/help/how-to-ask，尤其是https://stackoverflow.com/help/minimal-reproducible-example。
英文:
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/
As a side note, when you post to stack-overflow, it's always best to post code that people can run. The segments you posted don't stand on their own, which makes understanding/debugging hard. See: https://stackoverflow.com/help/how-to-ask and especially https://stackoverflow.com/help/minimal-reproducible-example
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论