Z3 哈希运算的约束求解器

Question

我正在尝试使用 Z3 解决 python lambda 表达式。

    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

我创建求解器的尝试看起来像这样；

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

但是这给了我这个错误；

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'

我是 Z3 的初学者，但我如何向 Z3 添加编码和哈希约束？

Answer 1

Z3 是一个强大的 SMT 求解器，但它并不是为直接处理编码和加密散列而设计的。但是，您可以创建一个模型来表示更高抽象级别的问题，然后使用 Z3 找到解决方案。

对于这个问题，您可以将输入 x 表示为一个字符序列，并将所需的输出 y 表示为一个十六进制字符序列。然后，您可以为 flippy 函数执行的转换创建约束，并为匹配哈希前缀创建约束。

这里有一个可能的方法来模拟你的问题：

from z3 import *

# Create Z3 variables
x = [String(f"x_{i}") for i in range(10)]  # Adjust the length as needed
y = [String(f"y_{i}") for i in range(20)]  # Length based on 4 hash prefixes

# Create a Z3 solver
solver = Solver()

# Add constraints for the flippy function
for i in range(len(x) // 2):
    solver.add(Or(And(0x30 <= Ord(x[i * 2]), Ord(x[i * 2]) <= 0x39),
                  And(0x61 <= Ord(x[i * 2]), Ord(x[i * 2]) <= 0x66)))
    solver.add(Or(And(0x30 <= Ord(x[i * 2 + 1]), Ord(x[i * 2 + 1]) <= 0x39),
                  And(0x61 <= Ord(x[i * 2 + 1]), Ord(x[i * 2 + 1]) <= 0x66)))
    solver.add(Concat(x[i * 2 + 1], x[i * 2]) == y[4 * i:4 * (i + 1)])

# Add constraints for matching the hash prefixes
hash_prefixes = [y[i:i + 4] for i in range(0, len(y), 4)]
desired_prefixes = ["md5_prefix", "sha1_prefix", "sha256_prefix", "sha384_prefix"]  # Replace these with actual values
for i in range(len(hash_prefixes)):
    solver.add(hash_prefixes[i] == desired_prefixes[i])

# Check for a solution
if solver.check() == sat:
    model = solver.model()
    x_solution = "".join([model[x[i]].as_string() for i in range(len(x))])
    y_solution = "".join([model[y[i]].as_string() for i in range(len(y))])
    print("x:", x_solution)
    print("y:", y_solution)
else:
    print("No solution found")

请记住，这种方法实际上并不计算加密哈希。它仅代表更高抽象级别的问题。如果您要解决的问题与现实世界的密码挑战有关，您可能需要使用不同的方法，例如蛮力或其他专门方法。