Solver for "A happy family (RE)" challenge from ångstromCTF 2020

a_happy_family.py

#a_happy_family solver

from z3 import *

basechars = "angstromctf20"
def toascii(v):
	res = ''
	for i in range(8):
		res += chr(v & 0xFF)
		v >>= 8

	return res[::-1]

def tobase(v, i):
	for _ in range(17-i):
		v /= 13

	return basechars[v % 13]

def tohex(val, nbits):
	return hex((val + (1 << nbits)) % (1 << nbits))

def to(val, nbits):
	return (val + (1 << nbits)) % (1 << nbits)


def add_constraints(s):
	s.add(And(n1 >=0,n1 <= 0xFFFFFFFFFFFFFFFF))
	s.add(And(n2 >=0,n2 <= 0xFFFFFFFFFFFFFFFF))
	s.add(And(n3 >=0,n3 <= 0xFFFFFFFFFFFFFFFF))
	s.add(And(n4 >=0,n4 <= 0xFFFFFFFFFFFFFFFF))
	s.add(n1 != 0x34ed16e30ff921f5)
	s.add(n1 != 0x315fd864fae49ddc)
	s.add(n1 != 0x34ecacf08588e980)
	s.add(n1 != 0x34ed16e30ff6f420)
	s.add(n1 != 0x315fd864fae27007)
	s.add(n2 != 0x9397a0cc9e512090)
	s.add(n2 != 0x9397a0c045ee082f)
	s.add(n2 != 0x9397a0c045ee082f)
	s.add(n3 != 0x8b888bcdbebc2f6a)
	s.add(n4 != 0x8b888bcdbebc2f6a)
	s.add(n4 != 0x7605350af74bd050)
	s.add(n4 != 0x7605350ae4987b57)
	s.add(n4 != 0x7605350af74ba567)
	return s

def tobase_z3(v, i):
	for _ in range(17-i):
		v /= 13
	#"angstromctf20"
	return simplify(If(v % 13 == 0, ord("a"), 
						If(v % 13 == 1, ord("n"),
							If(v % 13 == 2, ord("g"),
								If(v % 13 == 3, ord("s"),
									If(v % 13 == 4, ord("t"),
										If(v % 13 == 5, ord("r"),
											If(v % 13 == 6, ord("o"),
												If(v % 13 == 7, ord("m"),
													If(v % 13 == 8, ord("c"),
														If(v % 13 == 9, ord("t"),
															If(v % 13 == 10, ord("f"),
																If(v % 13 == 11, ord("2"),
																	If(v % 13 == 12, ord("0"),0))))))))))))))

n1,n2,n3,n4 = Ints('n1 n2 n3 n4')

s = Solver()


n1_sol = "artomtf2srn00tgm2f"
n2_sol = "ng0fa0mat0tmmmra0c"
n3_sol = "ngnrmcornttnsmgcgr"
n4_sol = "a0fn2rfa00tcgctaot"

n = len(n1_sol)


for i in range(n):
	s.add(simplify(tobase_z3(n1, i)) == ord(n1_sol[i]))
	s.add(simplify(tobase_z3(n2, i)) == ord(n2_sol[i]))
	s.add(simplify(tobase_z3(n3, i)) == ord(n3_sol[i]))
	s.add(simplify(tobase_z3(n4, i)) == ord(n4_sol[i]))


s = add_constraints(s)

print(s.check())

r = s.model()

v1 = r.eval(n1).as_long()
v2 = ~r.eval(n2).as_long()
v3 = -(r.eval(n3).as_long() - 0x1337)
v4 = (r.eval(n4).as_long()  + 0x4242) ^ 0x1234567890abcdef

print('1st: '+tohex(v1,64)+':'+toascii(v1))
print('2nd: '+tohex(v2,64)+':'+hex(r.eval(n2).as_long())+':'+toascii(to(v2,64)))
print('3rd: '+tohex(v3,64)+':'+hex(r.eval(n3).as_long())+':'+toascii(to(v3,64)))
print('4th: '+tohex(v4,64)+':'+hex(r.eval(n4).as_long())+':'+toascii(to(v4,64)))

s1 = toascii(to(v1,64))[::-1]
s2 = toascii(to(v2,64))[::-1]
s3 = toascii(to(v3,64))[::-1]
s4 = toascii(to(v4,64))[::-1]

#s = s1+s2+s3+s4

r = [None]*32
for i in range(8):
	r[i*2] = s1[i]
	r[i*2+1] = s3[i]
	r[16+i*2] = s2[i]
	r[16+i*2 +1] = s4[i]

print(''.join(r))

print('done')