Z3
use z3 to solve problem¶
安装: pip install z3-solver
教程: https://ericpony.github.io/z3py-tutorial/guide-examples.htm
上面连接失效了可以看下git仓库，我已经离线了。
原加密算法¶
i=0
#x=???
while(i<64):
if x>=0:
x=x*2
else:
x=(x*2)^0xB0004B7679FA26B3
使用z3进行求解¶
from z3 import *
import binascii
#copy from ida
encode = [0x96, 0x62, 0x53, 0x43, 0x6D, 0xF2, 0x8F, 0xBC, 0x16, 0xEE,
0x30, 0x05, 0x78, 0x00, 0x01, 0x52, 0xEC, 0x08, 0x5F, 0x93,
0xEA, 0xB5, 0xC0, 0x4D, 0x50, 0xF4, 0x53, 0xD8, 0xAF, 0x90,
0x2B, 0x34, 0x81, 0x36, 0x2C, 0xAA, 0xBC, 0x0E, 0x25, 0x8B,
0xE4, 0x8A, 0xC6, 0xA2, 0x81, 0x9F, 0x75, 0x55, 0xB3, 0x26,
0xFA, 0x79, 0x76, 0x4B, 0x00, 0xB0]
n = [BitVec("n%d" % i, 64) for i in range(6)]
solver = Solver()
for j in range(6):
for i in range(64):
n[j] = If(n[j] >= 0, n[j] * 2, (n[j] * 2) ^ 0xB0004B7679FA26B3)
b = 0
while(b < 64):
# solver.add(((n[0] << b) >> (b+64-b-8)) >= 0x20) the last qword high bits is 0;
solver.add(((n[0] << b) >> (b+64-b-8)) <= 0x7e)
b = b+8
solver.add(n[0] == 0xbc8ff26d43536296)
solver.add(n[1] == 0x520100780530ee16)
solver.add(n[2] == 0x4dc0b5ea935f08ec)
solver.add(n[3] == 0x342b90afd853f450)
solver.add(n[4] == 0x8b250ebcaa2c3681)
solver.add(n[5] == 0x55759f81a2c68ae4)
if solver.check() == sat:
print(solver.model())
# n5 = 32056
# n0 = 7378644943136451686
# n1 = 7148951143638579506
# n4 = 7363777037631763767
# n2 = 3257850080642543666
# n3 = 3835203404393046370
# print(binascii.unhexlify(hex(n0)[2:])[::-1], end='')
# print(binascii.unhexlify(hex(n1)[2:])[::-1], end='')
# print(binascii.unhexlify(hex(n2)[2:])[::-1], end='')
# print(binascii.unhexlify(hex(n3)[2:])[::-1], end='')
# print(binascii.unhexlify(hex(n4)[2:])[::-1], end='')
# print(binascii.unhexlify(hex(n5)[2:])[::-1], end='')
s = [0xBC8FF26D43536296, 0x520100780530EE16, 0x4DC0B5EA935F08EC, 0x342B90AFD853F450,
0x8B250EBCAA2C3681, 0x55759F81A2C68AE4]
r = ''
s1 = []
for i in range(len(s)):
t = s[i]
for j in range(64):
if t & 1:
t ^= 0xB0004B7679FA26B3
t >>= 1
t |= 0x8000000000000000
else:
t >>= 1
print(hex(t))
while t > 0:
r += chr(t & 0xff)
t >>= 8
print(r)
本页面的全部内容在 CC BY-NC-SA 4.0 协议之条款下提供，附加条款亦可能应用。