Solution to DCTF 2015 Crypto 300

crypto300.py

import z3

ciphertext = "320b1c5900180a034c74441819004557415b0e0d1a316918011845524147384f5700264f48091e4500110e41030d1203460b1d0752150411541b455741520544111d0000131e0159110f0c16451b0f1c4a74120a170d460e13001e120a1106431e0c1c0a0a1017135a4e381b16530f330006411953664334593654114e114c09532f271c490630110e0b0b"
c = map(ord, ciphertext.decode("hex"))
space = [z3.Int("space%d" % x) for x in range(len(c) + 1)]
p = z3.Array("plain", z3.IntSort(), z3.BitVecSort(8))
s = z3.Solver()
s.add(space[0] == 0xA)
for i in range(len(c)):
    s.add(z3.Or(
        z3.And(space[i + 1] == space[i] + 1, p[i] % 2 == 0),
        z3.And(space[i + 1] == space[i] - 1, p[i] % 2 == 1)))
    s.add(z3.Or(
        z3.And(c[i] == p[i] ^ p[i + space[i]], i + space[i] < len(c) - 1),
        z3.And(c[i] == p[i] ^ p[space[i]], i + space[i] >= len(c) - 1)))
    s.add(z3.Or(
        p[i] == ord(' '),
        p[i] == ord('.'),
        p[i] == ord('_'),
        z3.And(p[i] >= ord('0'), p[i] <= ord('9')),
        z3.And(p[i] >= ord('A'), p[i] <= ord('Z')),
        z3.And(p[i] >= ord('a'), p[i] <= ord('z'))))
s.check()
m = s.model()
func = m[p]
plain = [func.else_value().as_long()] * len(c)
for key,val in func.as_list()[:-1]:
    plain[key.as_long()] = val.as_long()
print "".join(map(chr, plain))