HUST 2017 - Mystic Crypt

from z3 import *
 
 
I_LOVE = [0x49, 0x5F, 0x4C, 0x30, 0x56, 0x33, 0x5F, 0x53, 0x65, 0x43, 0x75, 0x52, 0x31, 0x74, 0x79, 0x5F]
I_LOVE += [0x56, 0x65, 0x52, 0x79, 0x5F, 0x6D, 0x75, 0x43, 0x48, 0x5F, 0x41, 0x6E, 0x64, 0x59, 0x30, 0x75]
I_LOVE += [0x83, 0x5B, 0xD1, 0x73, 0xD5, 0x68, 0x8E, 0x20, 0xB0, 0x2B, 0xFB, 0x72, 0x81, 0x5F, 0x82, 0x2D]
I_LOVE += [0x5A, 0xAA, 0x41, 0xA1, 0x05, 0xC7, 0x34, 0xE2, 0x4D, 0x98, 0x75, 0x8C, 0x29, 0xC1, 0x45, 0xF9]
I_LOVE += [0xF9, 0x35, 0x48, 0xD6, 0x2C, 0x5D, 0xC6, 0xF6, 0x9C, 0x76, 0x3D, 0x84, 0x1D, 0x29, 0xBF, 0xA9]
I_LOVE += [0xFE, 0x0F, 0x49, 0x72, 0xFB, 0xC8, 0x7D, 0x90, 0xB6, 0x50, 0x08, 0x1C, 0x9F, 0x91, 0x4D, 0xE5]
I_LOVE += [0x7C, 0xD6, 0x91, 0x0D, 0x50, 0x8B, 0x57, 0xFB, 0xCC, 0xFD, 0x6A, 0x7F, 0xD1, 0xD4, 0xD5, 0xD6]
I_LOVE += [0xC0, 0x47, 0x4A, 0x84, 0x3B, 0x8F, 0x37, 0x14, 0x8D, 0xDF, 0x3F, 0x08, 0x12, 0x4E, 0x72, 0xED]
I_LOVE += [0x5B, 0x96, 0xC4, 0xC4, 0x0B, 0x1D, 0x93, 0x3F, 0xC7, 0xE0, 0xF9, 0x40, 0x16, 0x34, 0x2C, 0x96]
I_LOVE += [0x87, 0x5F, 0x3B, 0x14, 0xBC, 0xD0, 0x0C, 0x00, 0x31, 0x0F, 0x33, 0x08, 0x23, 0x41, 0x41, 0xE5]
I_LOVE += [0xC8, 0x15, 0x1D, 0xE2, 0xC3, 0x08, 0x8E, 0xDD, 0x04, 0xE8, 0x77, 0x9D, 0x12, 0xDC, 0x5B, 0x0B]
I_LOVE += [0x4E, 0xD9, 0x02, 0x3F, 0xF2, 0x09, 0x0E, 0x3F, 0xC3, 0x06, 0x3D, 0x37, 0xE0, 0x47, 0x7C, 0xD2]
I_LOVE += [0x48, 0x05, 0xA8, 0x03, 0x8B, 0x0D, 0x26, 0xDE, 0x8F, 0xE5, 0x51, 0x43, 0x9D, 0x39, 0x0A, 0x48]
I_LOVE += [0x10, 0xCB, 0x65, 0x6D, 0xE2, 0xC2, 0x6B, 0x52, 0x21, 0xC4, 0x56, 0x65, 0xC1, 0x83, 0x2A, 0xB7]
I_LOVE += [0xE4, 0xE0, 0x01, 0x7B, 0x6F, 0xED, 0x27, 0xA5, 0xE0, 0x08, 0x76, 0xE6, 0x7D, 0x31, 0x7C, 0xAE]
I_LOVE += [0x49, 0x5F, 0x4C, 0x30, 0x56, 0x33, 0x5F, 0x53, 0x65, 0x43, 0x75, 0x52, 0x31, 0x74, 0x79, 0x5F]
I_LOVE += [0x56, 0x65, 0x52, 0x79, 0x5F, 0x6D, 0x75, 0x43, 0x48, 0x5F, 0x41, 0x6E, 0x64, 0x59, 0x30, 0x75]
I_LOVE += [0x04, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]
I_LOVE += [0xAE, 0xD7, 0x7B, 0xAA, 0xAE, 0xD7, 0x7B, 0xAA, 0xAE, 0xD7, 0x7B, 0xAA, 0xAE, 0xD7, 0x7B, 0xAA]
I_LOVE += [0xAE, 0xD7, 0x7B, 0xAA, 0xAE, 0xD7, 0x7B, 0xAA, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]
 
 
INDEX = "\x63\x7C\x77\x7B\xF2\x6B\x6F\xC5\x30\x01\x67\x2B\xFE\xD7\xAB\x76\xCA\x82\xC9\x7D\xFA\x59\x47\xF0"
INDEX += "\xAD\xD4\xA2\xAF\x9C\xA4\x72\xC0\xB7\xFD\x93\x26\x36\x3F\xF7\xCC\x34\xA5\xE5\xF1\x71\xD8\x31\x15"
INDEX += "\x04\xC7\x23\xC3\x18\x96\x05\x9A\x07\x12\x80\xE2\xEB\x27\xB2\x75\x09\x83\x2C\x1A\x1B\x6E\x5A\xA0"
INDEX += "\x52\x3B\xD6\xB3\x29\xE3\x2F\x84\x53\xD1\x00\xED\x20\xFC\xB1\x5B\x6A\xCB\xBE\x39\x4A\x4C\x58\xCF"
INDEX += "\xD0\xEF\xAA\xFB\x43\x4D\x33\x85\x45\xF9\x02\x7F\x50\x3C\x9F\xA8\x51\xA3\x40\x8F\x92\x9D\x38\xF5"
INDEX += "\xBC\xB6\xDA\x21\x10\xFF\xF3\xD2\xCD\x0C\x13\xEC\x5F\x97\x44\x17\xC4\xA7\x7E\x3D\x64\x5D\x19\x73"
INDEX += "\x60\x81\x4F\xDC\x22\x2A\x90\x88\x46\xEE\xB8\x14\xDE\x5E\x0B\xDB\xE0\x32\x3A\x0A\x49\x06\x24\x5C"
INDEX += "\xC2\xD3\xAC\x62\x91\x95\xE4\x79\xE7\xC8\x37\x6D\x8D\xD5\x4E\xA9\x6C\x56\xF4\xEA\x65\x7A\xAE\x08"
INDEX += "\xBA\x78\x25\x2E\x1C\xA6\xB4\xC6\xE8\xDD\x74\x1F\x4B\xBD\x8B\x8A\x70\x3E\xB5\x66\x48\x03\xF6\x0E"
INDEX += "\x61\x35\x57\xB9\x86\xC1\x1D\x9E\xE1\xF8\x98\x11\x69\xD9\x8E\x94\x9B\x1E\x87\xE9\xCE\x55\x28\xDF"
INDEX += "\x8C\xA1\x89\x0D\xBF\xE6\x42\x68\x41\x99\x2D\x0F\xB0\x54\xBB\x16"
 
 
def sub_401040(recovery, num):
    for i in range(4):
        for j in range(4):
            recovery[(4*j)+i] ^= I_LOVE[(16*num) + 4 * i + j]
 
    return recovery
 
 
def sub_401A50(recovery):
    recovery_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
 
    for x in range(16):
        recovery_tmp[x] = recovery[x]
 
    recovery[5] = recovery_tmp[4]
    recovery[6] = recovery_tmp[5]
    recovery[7] = recovery_tmp[6]
    recovery[4] = recovery_tmp[7]
 
    recovery[10] = recovery_tmp[8]
    recovery[8] = recovery_tmp[10]
 
    recovery[11] = recovery_tmp[9]
    recovery[9] = recovery_tmp[11]
 
    recovery[15] = recovery_tmp[12]
    recovery[14] = recovery_tmp[15]
    recovery[13] = recovery_tmp[14]
    recovery[12] = recovery_tmp[13]
 
    return recovery
 
 
def sub_401C90(recovery):
    for i in range(4):
        for j in range(4):
            recovery[(4*i)+j] = INDEX.find(chr(recovery[(4*i)+j])) 
 
    return recovery
 
 
def sub_4017F0(recovery):
    input_ = [BitVec("input_%d" % x, 32) for x in range(16)]
 
    s = Solver()
    for x in range(16): s.add(input_[x] <= 0xff)
 
    for i in range(4):
        v1 = input_[i]
        v2 = (input_[i + 12] ^ input_[i + 8] ^ input_[i + 4] ^ input_[i]) & 0xff
        v3 = (input_[i + 4] ^ input_[i]) & 0xff
        input_[i] ^= v2 ^ 27 * ((v3 >> 7) & 1) ^ 2 * v3 & 0xff
        v4 = input_[i + 8] ^ input_[i + 4] & 0xff
        input_[i + 4] ^= v2 ^ 27 * ((v4 >> 7) & 1) ^ 2 * v4 & 0xff
        v5 = input_[i + 12] ^ input_[i + 8] & 0xff
        input_[i + 8] ^= v2 ^ 27 * ((v5 >> 7) & 1) ^ 2 * v5 & 0xff
        input_[i + 12] ^= v2 ^ 27 * (((v1 ^ input_[i + 12]) >> 7) & 1) ^ 2 * (v1 ^ input_[i + 12]) & 0xff
 
    for i in range(16):
        s.add(input_[i] == recovery[i])    
 
    if s.check() == sat:
        model = s.model()
        for x in model:
            index_ = str(x).find("_") + 1
            rec_idx = int(str(x)[index_:])
            recovery[rec_idx] = int(str(model[x]))
 
    return recovery
 
 
def decrypt(fd, decrypt_):
 
    while True:
        try:
            recovery = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
 
            stream = fd.read(0x20)[:0x10]
 
            for l in range(4):
                for m in range(4):
                    recovery[(4*m)+l] = ord(stream[(4*l)+m])
 
            recovery = sub_401040(recovery, 0xe)
            recovery = sub_401A50(recovery)
            recovery = sub_401C90(recovery)
 
            for k in range(0x1, 0xe):
                recovery = sub_401040(recovery, 0xe-k)
                recovery = sub_4017F0(recovery)
                rerecoverycovery = sub_401A50(recovery)
                recovery = sub_401C90(recovery)
 
            recovery = sub_401040(recovery, 0)
 
            result = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
            for i in range(4):
                for j in range(4):
                    result[ (4*i) + j] = recovery[(4*j) + i]
 
            png = ""
            for x in range(16):
                png += chr(result[x])
            decrypt_.write(png)
 
        except:
            print "[+] Done."
            break
 
 
if __name__ == "__main__":
    print "[+] Hust 2017 rev 150pt"
    print "[+] making \"recovery.png\""
    
    fd = open("Find Me.hust", "rb")
    decrypt_ = open("recovery.png", "wb")    
    decrypt(fd, decrypt_)