Hack.lu CTF 2016 - Cthulhu's treasure

solve.py

import struct
from z3 import *

p = lambda x: struct.pack('<I', x)

s = Solver()

name = [BitVec('name_%d' % i, 8) for i in range(10)]
for i, c in enumerate(list('cthulhu\0\0\0')):
    s.add(name[i] == ord(c))
passphrase = [BitVec('passphrase_%d' % i, 32) for i in range(5)]
x = [BitVec('x_%d' % i, 64) for i in range(118)]

s.add(passphrase[4] & 0xff000000 == 0)

s.add(x[0] == 0xdeadb00b)
n = 1
for i in range(10):
    for j in range(15-i):
        c = ZeroExt(56, name[i])
        s.add(x[n] == ((x[n-1] ^ c) * 0xdeadbeef) ^ ((x[n-1] ^ c) * 0xdeadbeef << 0x7))
        n += 1

for i in range(5):
    for j in range(4-i):
        a = ZeroExt(32, passphrase[i])
        b = ZeroExt(32, passphrase[4-j-i])
        s.add(x[n] == (((x[n-1] ^ a) << 0x2 ^ b) * 0xcafebabe) ^ (((x[n-1] ^ a) << 0x2 ^ b) * 0xcafebabe << 0x6))
        n += 1

s.add(x[n-1] == 0xeeedc4e74f7b2012)

assert s.check() == sat
m = s.model()
print ''.join([p(m[a].as_long()) for a in passphrase]).encode('hex')