Z3首次运用

虽然模仿痕迹较重，但是感觉抓住了精髓
from z3 import *
Datacmp=[0x66,0x4e,0xa9,0xfd,0x3c,0x55,
0x90,0x24,0x57,0xf6,0x5d,0xb1,
0x1,0x20,0x81,0xfd,0x36,0xa9,
0x1f,0xa1,0xe,0xd,0x80,0x8f,
0xce,0x77,0xe8,0x23,0x9e,0x27,
0x60,0x2f,0xa5,0xcf,0x1b,0xbd,
0x32,0xdb,0xff,0x28,0xa4,0x5d]
flag=[BitVec('flag[%2d]' % i,8)for i in range (64)]
out=[0]64
f=Solver()
x=0
y=0
index=0
for i in range (7):
for j in range(6):
index=6i+j
x=flag[index]
y=flag[index]
x=~x
x=x&((2+j)i)
y=(y&(~((2+j)i)))|x
index=7j+i
out[index]=y
for i in range (42):
if(i%2!=1):
out[i]=(out[i]+out[i-1])%256
else:
out[i]=(out[i]0x6b)%256
for i in range(42):
f.add(Datacmp[i] == out[i])
while(f.check() == sat):
condition = []
m = f.model()
p=""
for i in range(42):
p+=chr(int("%s" % (m[flag[i]])))
condition.append(flag[i]!=int("%s" % (m[flag[i]])))
print(p)
f.add(Or(condition))