DownUnderCTF 2021 - Flag Checker solve script

solve.py

from z3 import *

def ch_transform(c):
	return ((c >> 7) * 0x1b ^ c * 2) & 0xff

def reverse_shuffle(inp):

	mappings = {0: 29, 1: 34, 2: 13, 3: 18, 4: 15, 5: 20, 6: 35, 7: 28, 8: 19, 9: 12, 10: 21, 11: 14, 12: 3, 13: 8, 14: 25, 15: 30, 16: 1, 17: 6, 18: 9, 19: 2, 20: 31, 21: 24, 22: 7, 23: 0, 24: 5, 25: 10, 26: 17, 27: 22, 28: 27, 29: 32, 30: 11, 31: 4, 32: 23, 33: 16, 34: 33, 35: 26}
	mappings = {v:k for k,v in mappings.items()}

	out = [None] * len(inp)
	for orig, new in mappings.items():
		out[new] = inp[orig]

	return out

def reverse_num_combine(inp, nums):

	# The known output values
	n_out = [inp[nums[i]] for i in range(6)]

	# The unknown input values that produce the output
	n = [BitVec(f"n{i}", 32) for i in range(6)]

	s = Solver()
	s.add(inp[nums[0]] == ch_transform(n[4]) ^ ch_transform(n[0]) ^ n[0] ^ n[2] ^ ch_transform(n[2]))
	s.add(inp[nums[1]] == ch_transform(n[5]) ^ ch_transform(n[1]) ^ n[1] ^ n[3] ^ ch_transform(n[3]))
	s.add(inp[nums[2]] == ch_transform(n[0]) ^ n[4])
	s.add(inp[nums[3]] == ch_transform(n[1]) ^ n[5])
	s.add(inp[nums[4]] == ch_transform(n[2]) ^ ch_transform(n[0]) ^ n[0])
	s.add(inp[nums[5]] == ch_transform(n[3]) ^ ch_transform(n[1]) ^ n[1])

	if s.check() == sat:

		m = s.model()
		final_nums = [int(str(m[e])) for e in n]

		for i in range(6):
			inp[nums[i]] = final_nums[i]
		return inp

def reverse_combine(inp):

	nums = [
		[0,1,2,6,12,18],
		[3,4,5,11,17,23],
		[7,8,9,13,14,15],
		[10,16,22,28,29,35],
		[19,20,24,25,26,30],
		[21,27,31,32,33,34]
	]

	for n in nums[::-1]:
		inp = reverse_num_combine(inp, n)
	return inp

if __name__ == '__main__':
	
	target = bytes.fromhex("0f4f733c41c6a4afb441d665c899aab36c99613c4edd704615663c1b7f16a66f2313126e")

	for _ in range(16):
		target = reverse_shuffle(target)
		target = reverse_combine(target)

	
	print("".join(map(chr, target)))
	# DUCTF{rev3rs1bl3___and___1nv3rtibl3}