z3 solver example

easy-crack-me-z3.py

from z3 import *
s = Solver()
s.set(unsat_core=True)
def is_valid(x):
	return Or(
			(x==ord('0')),
			(x==ord('1')),
			(x==ord('2')),
			(x==ord('3')),
			(x==ord('4')),
			(x==ord('5')),
			(x==ord('6')),
			(x==ord('7')),
			(x==ord('8')),
			(x==ord('9')),
			(x==ord('a')),
			(x==ord('b')),
			(x==ord('c')),
			(x==ord('d')),
			(x==ord('e')),
			(x==ord('f')),
	)
vec = ""
length = 39
for i in range(length):
	vec += F"pw[{i}] "
m = BitVecs(vec,8)
for i in range(6,length-1):
	s.add(is_valid(m[i]))

s.add(m[0] ==ord('T'))
s.add(m[1] ==ord('W'))
s.add(m[2] ==ord('C'))
s.add(m[3] ==ord('T'))
s.add(m[4] ==ord('F'))
s.add(m[5] ==ord('{'))
s.add(m[38] ==ord('}'))

v21 = [0]*8
v22 = [0]*8
unk_400f00 = [3,2,2,0,3,2,1,3,3,1,1,3,1,2,2,3]
alpha = ['0','1','2','3','4','5','6','7','8','9','a','b','c','d','e','f']
unk_400f40 = [0x15E,0xDA,0x12F,0x131,0x100,0x131,0xfb,0x102]
unk_400f60 = [0x52,0x0c,0x1,0x0f,0x05c,0x5,0x53,0x58]
unk_400f80 = [0x1,0x57,7,0x0d,0x0d,0x53,0x51,0x51]
unk_400fa0 = [0x129,0x103,0x12b,0x131,0x135,0x10b,0xff,0xff]
unk_400fc0 = [0x80,0x80,0x0FF,0x80,0x0FF,0x0FF,0x0FF,0x0FF,0x80,0x0FF,0x0FF,0x80,0x80,0x0FF,0x0FF,0x80,0x0FF,0x0FF,0x80,0x0FF,0x80,0x80,0x0FF,0x0FF,0x0FF,0x0FF,0x80,0x0FF,0x0FF,0x0FF,0x80,0x0FF]
for k in range(8):
	v10 = 0
	v11 = 0
	for l in range(4):
		i = 4*k+6+l
		if(i<39) and (i>=0):
			v5 = m[i]
			v10+=v5
			v11^=v5
	v21[k] = v10
	v22[k] = v11
	s.add(v21[k]==unk_400f40[k])
	s.add(v22[k]==unk_400f60[k])

v23 = [0]*8
v24 = [0]*8
for M in range(8):
	v14 = 0
	v15 = 0
	for N in range(4):
		i = 8*N+6+M
		if(i<39) and (i>=0):
			v6 = m[i]
			v14+=v6
			v15^=v6
	v23[M] = v14
	v24[M] = v15
	s.add(v23[M]==unk_400fa0[M])
	s.add(v24[M]==unk_400f80[M])
for i in range(32):
	v7 = m[i+6]
	v33i = unk_400fc0[i]
	if(v33i==0):
		s.add(And(
		Or(v7<=47,v7>57),
		Or(v7<=96,v7>102)
		))
	elif(v33i==128):
		s.add(And(
		Or(v7<=47,v7>57),
		Not(Or(v7<=96,v7>102))
		))
	elif(v33i==255):
		s.add(Not(Or(v7<=47,v7>57)))
v18 = 0
for j in range(16):
	v18+=m[2*(j+3)]
s.add(v18==1160)
s.add(m[37] == 53)
s.add(m[7] == 102)
s.add(m[11] == 56)
s.add(m[12] == 55)
s.add(m[23] == 50)
s.add(m[31] == 52)
while s.check() == z3.sat:
	model = s.model()
	nope = []
	out = ''
	for i in m:
		if str(i):
			out += chr(model[i].as_long()&0xff)
		nope.append(i!=model[i])
	s.add(Or(nope[:-1]))
	ok = True
	for i in range(len(alpha)):
		if(out.count(alpha[i])!=unk_400f00[i]):
			ok = False
			break
	if not ok:
		continue
	print(out)
	exit(0)