CSAW CTF 2013 – crackme (at katagaitai勉強会#6 - 関東|easy)

result.txt

$ python solve.py
[s_1 = 49,
 s_2 = 97,
 s_0 = 98,
 s_3 = 87,
 s_5 = 120,
 s_4 = 60]
registration code: b1aW<x

$ nc 45.32.49.214 54321
Enter registration code: b1aW<x
Thank you, valued customer!
Your key is: day 145: they still do not realize this software sucks

solve.py

from z3 import *

s_list = [BitVec("s_%d" % i, 32) for i in xrange(6)]

solver = Solver()

for s in s_list:
    solver.add(0x20 <= s, s <= 0x7e)

h = 1337

for s in s_list:
    h += (h << 5) + s

solver.add(h == 0xEF2E3558)

if solver.check() == sat:
    m = solver.model()
    print m

    reg_code = ''
    for s in s_list:
        reg_code += chr(m[s].as_long())

    print "registration code: %s" % reg_code
else:
    print "Unable to find answer."