Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement