TUCTF2017_future_solver.py

# A solution to the CUCTF 2017 Future task using Z3Py
# inspired by Hackeriet's solution in https://blog.hackeriet.no/solution-to-tuctf-2017-future/
from z3 import *

# This is the flag format
# flag = "TUCTF{..................}"

auth = [0x8b, 0xce, 0xb0, 0x89, 0x7b, 0xb0, 0xb0, 0xee, 0xbf, 0x92, 0x65, 0x9d, 0x9a, 0x99, 0x99, 0x94, 0xad, 0xe4, 0x00]

# Declare the variables for Z3
a, b, c, d, e, f, g, h, i, j, k, l, m = Ints('a b c d e f g h i j k l m')
n, o, p, q, r, s, t, u, v, w, x, y, z = Ints('n o p q r s t u v w x y z')

mat = [[a, b, c, d, e], [f, g, h, i, j], [k, l, m, n, o], [p, q, r, s, t], [u, v, w, x, y]]

# Create a mapping dictionary based on genMatrix()
mapper = {}
for i in range(25):
	m = (i*2)%25
	f = (i*7)%25
	mapper[f] = mat[m/5][m%5]

# Create the equations based on genAuthString()
equations = [mat[0][0] + mat[4][4] == int(auth[0]),
	mat[2][1] + mat[0][2] == int(auth[1]),
	mat[4][2] + mat[4][1] == int(auth[2]),
	mat[1][3] + mat[3][1] == int(auth[3]),
	mat[3][4] + mat[1][2] == int(auth[4]),
	mat[1][0] + mat[2][3] == int(auth[5]),
	mat[2][4] + mat[2][0] == int(auth[6]),
	mat[3][3] + mat[3][2] + mat[0][3] == int(auth[7]),
	mat[0][4] + mat[4][0] + mat[0][1] == int(auth[8]),
	mat[3][3] + mat[2][0] == int(auth[9]),
	mat[4][0] + mat[1][2] == int(auth[10]),
	mat[0][4] + mat[4][1] == int(auth[11]),
	mat[0][3] + mat[0][2] == int(auth[12]),
	mat[3][0] + mat[2][0] == int(auth[13]),
	mat[1][4] + mat[1][2] == int(auth[14]),
	mat[4][3] + mat[2][3] == int(auth[15]),
	mat[2][2] + mat[0][2] == int(auth[16]),
	mat[1][1] + mat[4][1] == int(auth[17]),
	mat[0][0] == ord('T'),
	mat[2][1] == ord('U'),
	mat[4][2] == ord('C'),
	mat[1][3] == ord('T'),
	mat[3][4] == ord('F'),
	mat[1][0] == ord('{'),
	mat[2][4] == ord('}')]

# Create a solver and solve
s = Solver()
s.add(equations)
s.check()
m = s.model()

# Map the solved values to the flag 
solution = [m[mapper[ix]].as_long() for ix in range(25)]
print(''.join(chr(int(i)) for i in solution))