z3 solver script for MixMix Rev Challenge from DefenitCTF 2020

mixmix_crack.py

from z3 import *
import string


def algo(myinput):
	# stolen arr (seed[0xDEFEA7], rand arr[0-255], swapped vals)
	rand_num_0_255 ="29, 24, 74, 0E8, 18, 0D6, 91, 43, 8B, 2D, 3D, 62, 75, 32, 88, 0EA, 0C2, 4F, 83, 0E9, 67, 2B, 0AC, 0A9, 6F, 8F, 0C7, 13, 0A3, 0AD, 5F, 66, 0E5, 59, 15, 5A, 2F, 11, 4E, 61, 55, 16, 0CC, 0B, 80, 42, 5, 2E, 0D, 0, 5D, 82, 2A, 0B9, 3B, 8E, 3F, 41, 0A1, 8A, 0D5, 89, 49, 69, 12, 0FB, 0DD, 22, 0C0, 3E, 3C, 4C, 56, 44, 0C6, 8D, 40, 0AA, 0B1, 14, 9B, 0BE, 0F4, 0BA, 78, 1, 0D8, 94, 0EC, 50, 0EE, 0ED, 0AE, 1F, 71, 76, 6B, 47, 0BC, 0D0, 33, 10, 0B4, 0DA, 57, 6E, 93, 7, 8C, 37, 6C, 98, 0E, 0BF, 2C, 0C4, 25, 0F3, 7C, 17, 7E, 0DC, 7A, 0D7, 6D, 0C1, 0AB, 0C, 2, 77, 0D3, 68, 5C, 0F0, 0E6, 79, 0D9, 46, 58, 9, 1E, 0CE, 6, 35, 5E, 0CF, 85, 0B2, 0CA, 0F9, 0C3, 70, 45, 0FC, 0F, 26, 0AF, 19, 7F, 4D, 0BD, 5B, 0A2, 52, 1D, 99, 0BB, 36, 84, 72, 0EF, 0B0, 38, 0A5, 0B3, 0B8, 9F, 0FE, 21, 97, 20, 0C5, 90, 0A8, 31, 0E2, 0A7, 0D4, 0D2, 0DE, 0B5, 0E0, 4B, 92, 87, 0E4, 0F5, 0DB, 6A, 65, 9C, 34, 95, 0F8, 0D1, 0A0, 3A, 28, 7D, 81, 63, 53, 54, 3, 0C8, 0A4, 23, 1C, 4A, 27, 39, 0CB, 0F2, 8, 48, 0E3, 86, 0B7, 73, 0FD, 0B6, 4, 0DF, 0CD, 1A, 7B, 30, 96, 64, 0EB, 0F6, 0A, 1B, 0FA, 0F7, 9E, 0E7, 51, 0F1, 0E1, 0FF, 9D, 9A, 0C9, 60, 0A6".replace(' ','').split(',')
	rand_num_0_255 = map(lambda x: int(x,16) , rand_num_0_255)

	lsb_inp_arr = [0]*256
	shuffled_bits_from_inp = [0]*256

	for i in range(len(myinput)):
		v4 = myinput[i]
		for j in range(8):
			lsb_inp_arr[j+8*i] = v4 & 1
			v4 >>= 1

	for i in range(256):
		shuffled_bits_from_inp[i] = lsb_inp_arr[rand_num_0_255[i]]

	#stole while debugging as it doesn't depend on input
	shuffled_from_randbits = [2,0,0,0,2,0,0,0,2,0,0,0,5,0,0,0,0,0,0,0,1,0,0,0,4,0,0,0,7,0,0,0,4,0,0,0,2,0,0,0,1,0,0,0,6,0,0,0,4,0,0,0,5,0,0,0,1,0,0,0,3,0,0,0,5,0,0,0,2,0,0,0,5,0,0,0,5,0,0,0,0,0,0,0,6,0,0,0,6,0,0,0,7,0,0,0,6,0,0,0,2,0,0,0,4,0,0,0,6,0,0,0,6,0,0,0,5,0,0,0,4,0,0,0,3,0,0,0,0,0,0,0,5,0,0,0,1,0,0,0,2,0,0,0,2,0,0,0,1,0,0,0,0,0,0,0,2,0,0,0,2,0,0,0,3,0,0,0,1,0,0,0,5,0,0,0,2,0,0,0,0,0,0,0,1,0,0,0,7,0,0,0,7,0,0,0,4,0,0,0,7,0,0,0,6,0,0,0,3,0,0,0,1,0,0,0,7,0,0,0,7,0,0,0,7,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,7,0,0,0,5,0,0,0,1,0,0,0,0,0,0,0,3,0,0,0,6,0,0,0,3,0,0,0,2,0,0,0,2,0,0,0,6,0,0,0,3,0,0,0,4,0,0,0,2,0,0,0,7,0,0,0,3,0,0,0,5,0,0,0,2,0,0,0,4,0,0,0,3,0,0,0,7,0,0,0,6,0,0,0,1,0,0,0,6,0,0,0,4,0,0,0,5,0,0,0,1,0,0,0,6,0,0,0,0,0,0,0,5,0,0,0,3,0,0,0,6,0,0,0,6,0,0,0,5,0,0,0,0,0,0,0,6,0,0,0,3,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,7,0,0,0,5,0,0,0,6,0,0,0,4,0,0,0,1,0,0,0,5,0,0,0,7,0,0,0,0,0,0,0,4,0,0,0,5,0,0,0,4,0,0,0,4,0,0,0,0,0,0,0,0,0,0,0,3,0,0,0,3,0,0,0,3,0,0,0,7,0,0,0,1,0,0,0,1,0,0,0,4,0,0,0,7,0,0,0,3,0,0,0,3,0,0,0,0,0,0,0,7,0,0,0,0,0,0,0,1,0,0,0,1,0,0,0]

	shuffled_bits_from_inp_2nd = [0]*256
	
	for i in range(4):
		for j in range(8):
			for k in range(8):
				shuffled_bits_from_inp_2nd[8 * (8 * i + j) + k] = shuffled_bits_from_inp[8 * (8 * i + shuffled_from_randbits[8*(k+(j<<3))]) + shuffled_from_randbits[(8*(k+(j<<3)))+4]]


	inpenc_list = []

	for i in range(4):
		for j in range(8):
			v5 = 0
			for k in range(8):
				v5 += shuffled_bits_from_inp_2nd[8 * (8 * i + j) + 7 - k] << k
			inpenc_list.append(v5)

	#stole arr made using "Defenit"
	deflist = [0x8D,0xAA,0x64,0xCD,0x66,0x5A,0xD4,0x1F,0x8C,0x54,0x24,0x3A,0x56,0x3F,0x2F,0x9F,0x15,0x8B,0x09,0xB0,0xFF,0x53,0xCE,0x14,0x49,0x8A,0xD2,0x20,0x5B,0x25,0xC7,0x33,0x1C,0x17,0xE1,0x48,0xD1,0x5C,0x89,0x7C,0xD9,0x3D,0x23,0x29,0x43,0xAF,0x47,0x4C,0x3E,0xFC,0x22,0x75,0x99,0xEB,0xDB,0x86,0x6B,0x81,0x40,0xAB,0x83,0xA5,0x8F,0x00,0xF6,0xB2,0x0C,0xD6,0xEF,0xF8,0x82,0x45,0xB8,0x65,0x52,0x19,0x9D,0x4F,0xF2,0x18,0x95,0x78,0x03,0x80,0x96,0xAC,0x6E,0x42,0x9E,0x60,0x7D,0xC1,0x32,0x69,0x28,0xDA,0xE4,0x93,0x02,0x39,0x0A,0x9A,0xB9,0xBC,0x1A,0x1D,0x38,0xAD,0xC6,0x6D,0x58,0x5D,0xED,0xDC,0x4E,0x73,0x13,0x44,0xC9,0x07,0xBF,0x87,0xE2,0xD0,0xA3,0x0D,0x16,0x62,0xFE,0x6F,0x70,0x84,0x0E,0x88,0xE8,0x34,0x0B,0xE7,0x4D,0xC2,0x5F,0xE9,0xBD,0x37,0xE6,0x3B,0x90,0xA2,0x74,0x55,0xFB,0x08,0xEE,0x72,0x2A,0xB7,0xA9,0xF7,0x2D,0x7B,0xA7,0x2B,0xB6,0xEC,0x06,0x01,0xC4,0xA6,0xB5,0xD7,0xF3,0x91,0x8E,0xD3,0xF9,0x10,0x77,0xBE,0xBB,0xD8,0x92,0xF4,0x63,0xB1,0x7E,0x35,0xA8,0xCF,0xDD,0xBA,0x46,0x98,0x67,0x61,0x04,0x2E,0xCB,0x0F,0x31,0xB4,0x05,0x4A,0x7F,0x76,0xC5,0x7A,0x30,0xA4,0x9B,0x6A,0x51,0x12,0xC8,0xDE,0x68,0x2C,0x1E,0x5E,0xA1,0x79,0xEA,0xAE,0xFA,0xA0,0xE0,0x1B,0x26,0x97,0x27,0xF5,0xCA,0x9C,0x36,0xC0,0xC3,0x3C,0xD5,0x6C,0xF1,0x57,0xDF,0xF0,0xCC,0x11,0x94,0x50,0xFD,0x85,0x21,0xE5,0x59,0xB3,0x41,0xE3,0x71,0x4B]
	v14 = 0
	v6 = 0
	final_def_arr = []

	for i in range(1,33):
	    v6 = (((v14 + deflist[i]))&0xff)
	    v14 = ((v6 + v14 + (deflist[i]))&0xff) - v6
	    deflist[v14],deflist[i] = deflist[i],deflist[v14]
	    v7 = (((deflist[v14] + deflist[i])))&0xff
	    final = ((v7 + deflist[v14] + deflist[i])&0xff)-v7
	    final_def_arr.append(deflist[final]) 

	
	res_arr = []
	for x,y in zip(final_def_arr,inpenc_list):
		res_arr.append(x^y)

	return res_arr


#print algo("hahathisismyinput")
#encrypted = [159, 174, 210, 25, 138, 207, 134, 121, 142, 178, 203, 47, 82, 7, 22, 59, 49, 168, 123, 234, 104, 161, 29, 178, 100, 55, 3, 42, 154, 191, 190, 21]
s = Solver()
inp = []
target = [41, 113, 78, 203, 142, 203, 181, 185, 51, 179, 165, 73, 168, 34, 183, 91, 185, 215, 115, 13, 104, 1, 53, 186, 167, 177, 230, 250, 16, 30, 24, 168]

# print(len(target))
alp = string.ascii_lowercase + string.ascii_uppercase + string.digits + '_}{' + '\x00'

for i in range(32):
	b = BitVec("%d" % i, 16)
	inp.append(b)
	s.add(Or([inp[i] == ord(c) for c in alp]))


flag_fmt_hint = "Defenit{"

for h in range(len(flag_fmt_hint)):
	s.add(inp[h] == ord(flag_fmt_hint[h]))

#Defenit{m1x_r4nd_c0lumn_r0w_rc4}

res = algo(inp)

for i in range(len(target)):
	s.add((res[i]) == (target[i]))


#print(s)

print s.check()

while s.check() == sat:
	solution = s.model()
	block = []
	flag = ""
	for i in range(len(inp)):
		c = inp[i]
		try: 
			flag += (chr(int(str(solution[c])))) 
		except :
			pass
		block.append(c != solution[c])
	s.add(Or(block))
	print flag