Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment