tuctf-future-z3.py

#!/usr/bin/env python

from z3 import *
import string

solver = z3.Solver()
for x in range(0,5):
  for y in range(0,5):
    varname = "mat_%i_%i" % (x,y)
    globals()[varname] = BitVec(varname,32)
    solver.add(globals()[varname] >= 0x20)
    solver.add(globals()[varname] <= 0xF0)

def check(x):
  for i in range(0,25):
    m = (i * 2) % 25
    f = (i * 7) % 25
    vname = "mat_%i_%i" % (m / 5, m % 5)
    if f == x:
      return vname

print check(4)
print check(5)

# import sys
# sys.exit(0)

# mat_0_0
# mat_2_1
# mat_4_2
# mat_1_3

solver.add(mat_0_0 == BitVecVal(ord('T'),32))
solver.add(mat_2_1 == BitVecVal(ord('U'),32))
solver.add(mat_4_2 == BitVecVal(ord('C'),32))
solver.add(mat_1_3 == BitVecVal(ord('T'),32))
solver.add(mat_3_4 == BitVecVal(ord('F'),32))
solver.add(mat_1_0 == BitVecVal(ord('{'),32))

solver.add(mat_0_0 + mat_4_4 == BitVecVal(0x8b,32))
solver.add(mat_2_1 + mat_0_2 == BitVecVal(0xce,32))
solver.add(mat_4_2 + mat_4_1 == BitVecVal(0xb0,32))
solver.add(mat_1_3 + mat_3_1 == BitVecVal(0x89,32))
solver.add(mat_3_4 + mat_1_2 == BitVecVal(0x7b,32))
solver.add(mat_1_0 + mat_2_3 == BitVecVal(0xb0,32))
solver.add(mat_2_4 + mat_2_0 == BitVecVal(0xb0,32))
solver.add(mat_3_3 + mat_3_2 + mat_0_3 == BitVecVal(0xee,32))
solver.add(mat_0_4 + mat_4_0 + mat_0_1 == BitVecVal(0xbf,32))
solver.add(mat_3_3 + mat_2_0 == BitVecVal(0x92,32))
solver.add(mat_4_0 + mat_1_2 == BitVecVal(0x65,32))
solver.add(mat_0_4 + mat_4_1 == BitVecVal(0x9d,32))
solver.add(mat_0_3 + mat_0_2 == BitVecVal(0x9a,32))
solver.add(mat_3_0 + mat_2_0 == BitVecVal(0x99,32))
solver.add(mat_1_4 + mat_1_2 == BitVecVal(0x99,32))
solver.add(mat_4_3 + mat_2_3 == BitVecVal(0x94,32))
solver.add(mat_2_2 + mat_0_2 == BitVecVal(0xad,32))
solver.add(mat_1_1 + mat_4_1 == BitVecVal(0xe4,32))

print solver.check()
n = solver.model()
print n

soln_array = {}
for d in n.decls():
  print "%s = %s" % (d.name(),n[d])
  soln_array[d.name()] = n[d]

out = ""
for i in range(0,25):
  vn = check(i)
  out += chr(int(str(soln_array[vn])))

print out