sat_solve.py

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))