0

我想用z3在python中生成一个keygen。这是验证功能：

def f(a):
    a = ord(a)
    if a <= 47 or a > 57:
        if a <= 64 or a > 98:
            exit()
        else:
            return a - 55
    else:
        return a - 48


def validate(key):
    if len(key) != 16:
        return False

    for k in key:
        if f(k)%2== 0:
            return False
    return True

我试图为此编写一个求解器

from z3 import *
solver = Solver()

def f_z3(a):
    return If(
        Or(a<=47, a>57),
        If(
            Or(a<=64, a>98),
            False, #  exit()???
            a -55
        ),
        a -48
    )

key = IntVector("key", 16)
for k in key:
    solver.add(f_z3(k)%2==0)

solver.check()
print(solver.model())

这是输出

[key__1 = 48,
 key__10 = 48,
 key__9 = 48,
 key__15 = 48,
 key__6 = 48,
 key__8 = 48,
 key__4 = 48,
 key__0 = 48,
 key__14 = 48,
 key__11 = 48,
 key__7 = 48,
 key__5 = 48,
 key__2 = 48,
 key__12 = 48,
 key__13 = 48,
 key__3 = 48]

它返回键“0000000000000000”，但 validate("0000000000000000") 返回 False。

我知道问题出在f_z3函数上，我不知道怎么表达exit()里面的 if，我想要的东西总是 False。但相反，我只是返回 False。

知道如何解决这个问题吗？

4

2 回答 2

2

您的代码有两个问题：

  1. 正如您所观察到的，在函数中替换exitwithFalse是不正确的f_z3。（python 版本在这里很奇怪，它在某些情况下会返回一个布尔值，而在其他情况下只是简单地死掉。但这不是重点。）在所有其他分支中，您返回一个整数，而在那个分支中，您正在返回一个布尔值。在 z3 中，您总是希望返回相同的类型；一个整数。所以选择一些最终会导致该案例产生的东西False 。由于稍后您要检查均匀性，因此任何奇数都可以。说1；所以修改它以产生1而不是 调用False何时。exit

  2. 在您进行验证时，False如果结果是偶数，则 Python 代码会返回；所以你需要正确地断言。目前您正在做solver.add(f_z3(k)%2==0)，相反，您应该要求模数不均匀，如下所示：solver.add(f_z3(k)%2!=0).

通过这两个修改，您将拥有以下代码：

from z3 import *
solver = Solver()

def f_z3(a):
    return If(
        Or(a<=47, a>57),
        If(
            Or(a<=64, a>98),
            1,
            a -55
        ),
        a -48
    )

key = IntVector("key", 16)
for k in key:
    solver.add(f_z3(k)%2!=0)

solver.check()
print(solver.model())

运行时，这会产生：

[key__1 = 49,
 key__10 = 49,
 key__9 = 49,
 key__15 = 49,
 key__6 = 49,
 key__8 = 49,
 key__4 = 49,
 key__0 = 49,
 key__14 = 49,
 key__11 = 49,
 key__7 = 49,
 key__12 = 49,
 key__5 = 49,
 key__2 = 49,
 key__13 = 49,
 key__3 = 49]

这表明有效的密钥"1111111111111111"。

于 2018-10-06T22:44:48.127 回答
0

对于我没有注意到的第二点，我更专注于第一点。返回 1 并不能解决我的问题，我只是用一个更小的例子简化了真正的问题。我想要这种模式的通用解决方案。

def f(x):
   if condition(x):
       exit()
   else:
       return g(x) # return something in relation with x

我发现这种模式现在有效

def f_z3(x):
    global solver
    solver.add(Not(condition(x))
    return g(x)

所以我的第一个功能将是

def f_z3(a):
    global solver
    # sins we have two nested condition we have to add an And
    solver.add(
        Not(
            And(
                Or(a<=47, a>57),
                Or(a<=64, a>98)
            )
        )
    )
    return If(
        Or(a<=47, a>57),
        a-55,
        a - 48
    )

我仍在寻找一种更好的方法来解决这种模式，它告诉 If 条件始终为 False。

于 2018-10-07T10:22:07.673 回答