我想用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
函数中,我不知道如何表达if中的exit()
,我想要的总是False。但我只是返回错误。你知道吗
你知道怎么解决这个问题吗?你知道吗
您的代码有两个问题:
正如您所观察到的,用
False
替换exit
是不对的 {cd3}函数中。(这里的python版本很奇怪 在某些情况下,它会返回一个布尔值,而只是简单的死 在其他方面。其他的都在旁边 你返回的是一个整数,在这个整数中,你返回的是一个 布尔型。在z3中,您总是希望返回相同的类型;整数。 所以选择一些会导致案例产生False
最终。后来你在检查是否均匀,有什么奇怪的吗 数字就行了。说1
;因此修改它以生成1
,而不是False
当调用exit
时。在验证时,如果结果是偶数,Python代码将返回
False
;因此需要正确地断言这一点。现在你在做solver.add(f_z3(k)%2==0)
,相反,你应该要求模不是偶数,比如:solver.add(f_z3(k)%2!=0)
。通过这两个修改,您将获得以下代码:
运行时,将生成:
表示有效键
"1111111111111111"
。你知道吗对于第二点我没有注意到,我更专注于第一点。 返回1并不能解决我的问题,我只是用一个小例子简化了实际问题。我想要一个通用的解决方案。你知道吗
我发现这种模式现在起作用了
所以我的第一个函数是
我仍然在寻找一种更好的方法来解决这种模式,它告诉If条件总是错误的。你知道吗
相关问题 更多 >
编程相关推荐