solve_with_z3.py

from z3 import *

import binascii, struct

def decrypt(data0, data1):
    # inverted key schedule for decryption
    key0 = 0x0a728e203850a80e 
    key1 = 0x1b8e2679ccaef6b4

    for round in xrange(31, -1, -1):
        key0 ^= key1
        key0 = ((key0 << 61) | (key0 >> 3)) & 0xffffffffffffffff

        key1 ^= round
        key1 = (key1 - key0) & 0xffffffffffffffff
        key1 = ((key1 << 8) | (key1 >> 56)) & 0xffffffffffffffff
        
        data1 ^= data0
        data1 = ((data1 << 61) | (data1 >> 3)) & 0xffffffffffffffff
        
        data0 ^= key0
        data0 = (data0 - data1) & 0xffffffffffffffff
        data0 = ((data0 << 8) | (data0 >> 56)) & 0xffffffffffffffff

    return data0, data1
    
mask = binascii.a2b_hex("DF90BC7057EF965AEECF0955CE80200D4FE10E0746A4C62FF0EC55532B785764")

mixer = struct.unpack("<QQQQQQQQQQQQQQQQ", binascii.a2b_hex("8013000000000000FA25000000000000AA0C000000000000E200000000000000E404000000000000DA56000000000000611A0000000000003F1200000000000009270000000000000301000000000000070E000000000000C000000000000000352000000000000031150000000000002000000000000000C70D000000000000"))
target = struct.unpack("<QQQQQQQQQQQQQQQQ", binascii.a2b_hex("6AC26F1400000000046B7610000000006CCEE52A00000000E4FCF52D000000009A013424000000009DE9671F000000007FAA4840000000004CC7264C000000004E96B2160000000002589013000000005F9BCF33000000000F98D52C0000000064C1FC1D00000000A39DA914000000006216102C00000000DBDEA92B00000000"))

s = Solver()

mat = []
for i in xrange(16):
    t = BitVec("bv%02d" % i, 64)
    s.add(t >= 0)
    s.add(t <= 0xffff)
    mat.append(t)
    
for col in xrange(4):
    for row in xrange(4):
        s.add( \
            mat[ 0+col] * mixer[0+row*4] + \
            mat[ 4+col] * mixer[1+row*4] + \
            mat[ 8+col] * mixer[2+row*4] + \
            mat[12+col] * mixer[3+row*4] == target[col+row*4])
            
s.check()
m = s.model()

result = [int(str(m[mat[i]])) for i in xrange(16)]

data0 = 0
data1 = 0
for i in xrange(4):
    data0 = (data0 << 16) | result[i]
    data1 = (data1 << 16) | result[4+i]
    
plain0, plain1 = decrypt(data0, data1)

data0 = 0
data1 = 0
for i in xrange(4):
    data0 = (data0 << 16) | result[8+i]
    data1 = (data1 << 16) | result[12+i]
    
plain2, plain3 = decrypt(data0, data1)

masked = struct.pack(">QQQQ", plain0, plain1, plain2, plain3)

s = ""
for i in xrange(0, 32, 2):
    res = struct.unpack("<H", mask[i:i+2])[0] ^ struct.unpack(">H", masked[i:i+2])[0]
    s += chr(res)
    
print repr(s)