from z3 import * | |
import os | |
import pdb | |
solver = Solver() | |
X = [ BitVec("x%s" % i, 8) for i in range(16) ] | |
# The last one is a null byte. No choice in the matter | |
solver.add(X[15] == 0) | |
# PERFORM THE SHUFFLE | |
# BEFORE: 0123456789ABCDE* | |
# AFTER: 26715B9E3*48ACD0 | |
SHUFFLED = [None] * 16 | |
SHUFFLED[0] = X[2] | |
SHUFFLED[1] = X[6] | |
SHUFFLED[2] = X[7] | |
SHUFFLED[3] = X[1] | |
SHUFFLED[4] = X[5] | |
SHUFFLED[5] = X[11] | |
SHUFFLED[6] = X[9] | |
SHUFFLED[7] = X[14] | |
SHUFFLED[8] = X[3] | |
SHUFFLED[9] = X[15] | |
SHUFFLED[10] = X[4] | |
SHUFFLED[11] = X[8] | |
SHUFFLED[12] = X[10] | |
SHUFFLED[13] = X[12] | |
SHUFFLED[14] = X[13] | |
SHUFFLED[15] = X[0] | |
def dword_add(vars, consts): | |
ret = [] | |
carry = BitVecVal(0, 8) | |
for i in range(4): | |
v = (vars[i] + consts[i] + carry) & 0xFF | |
carry = If(BVAddNoOverflow(vars[i],consts[i] + carry, False), BitVecVal(0, 8), BitVecVal(1, 8)) | |
ret.append(v) | |
return ret | |
ADDED = [] | |
ADDED += dword_add(SHUFFLED[0:4], [0xEF, 0xBE, 0xAD, 0xDE]) | |
ADDED += dword_add(SHUFFLED[4:8], [0xAD, 0xDE, 0xE1, 0xFE]) | |
ADDED += dword_add(SHUFFLED[8:12], [0x37, 0x13, 0x37, 0x13]) | |
ADDED += dword_add(SHUFFLED[12:16], [0x66, 0x74, 0x63, 0x67]) | |
XORED = [None] * 16 | |
XORED[0] = ADDED[0] ^ 0x76 | |
XORED[1] = ADDED[1] ^ 0x58 | |
XORED[2] = ADDED[2] ^ 0xB4 | |
XORED[3] = ADDED[3] ^ 0x49 | |
XORED[4] = ADDED[4] ^ 0x8D | |
XORED[5] = ADDED[5] ^ 0x1A | |
XORED[6] = ADDED[6] ^ 0x5F | |
XORED[7] = ADDED[7] ^ 0x38 | |
XORED[8] = ADDED[8] ^ 0xD4 | |
XORED[9] = ADDED[9] ^ 0x23 | |
XORED[10] = ADDED[10] ^ 0xF8 | |
XORED[11] = ADDED[11] ^ 0x34 | |
XORED[12] = ADDED[12] ^ 0xEB | |
XORED[13] = ADDED[13] ^ 0x86 | |
XORED[14] = ADDED[14] ^ 0xF9 | |
XORED[15] = ADDED[15] ^ 0xAA | |
[solver.add(XORED[i] == X[i]) for i in range(15)] | |
solver.add(X[0] == 67) # C | |
solver.add(X[1] == 84) # T | |
solver.add(X[2] == 70) # F | |
solver.add(X[3] == 123) # { | |
solver.check() | |
answer = [chr(solver.model()[X[i]].as_long()) for i in range(15)] | |
print(''.join(answer)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment