Rating:
from z3 import *
table1 = [0x70, 0x30, 0x53, 0xA1, 0xD3, 0x70, 0x3F, 0x64, 0xB3, 0x16,
0xE4, 0x04, 0x5F, 0x3A, 0xEE, 0x42, 0xB1, 0xA1, 0x37, 0x15,
0x6E, 0x88, 0x2A, 0xAB]
table2 = [0x20, 0xAC, 0x7A, 0x25, 0xD7, 0x9C, 0xC2, 0x1D, 0x58, 0xD0,
0x13, 0x25, 0x96, 0x6A, 0xDC, 0x7E, 0x2E, 0xB4, 0xB4, 0x10,
0xCB, 0x1D, 0xC2, 0x66, 0x3B]
s = Solver()
Serial = [BitVec('serial%s' % i, 8) for i in range(len(table1))] # serial
byte_3b = BitVec('byte3b', 8)
stack = []
s = Solver()
Y = 0
s.add(byte_3b == 0) # set initial state for byte_3b
# state = byte_3b # this is the sum of states for the byte 3b when we go on
def is_alphanum(x):
return Or(
And(x >= 0x30, x <= 0x39),
And(x >= 0x41, x <= 0x5a),
x == 0x20)
# And(x >= 0x61, x <= 0x7a)
def display_model(m):
block = {}
password = ""
for x in m:
if 'serial' in str(x):
block[int(str(x)[6:])] = int(str(m[x]))
for v in block.itervalues():
password += chr(v)
print password
while Y < 24:
cond = is_alphanum(Serial[Y])
s.add(cond)
A = Serial[Y]
A = RotateLeft(A, 3)
byte_3b = RotateRight(byte_3b, 2)
A += byte_3b
A ^= table1[Y]
byte_3b = A
A = RotateLeft(A, 4)
A ^= table2[Y]
s.add(A == 0)
Y += 1
if s.check() == sat:
m = s.model()
display_model(m)
else:
print 'no solution found!!'
