svattt2017_SerialMe.py

from pwn import *
r = remote('54.175.77.52', 2345)

from z3 import *

def gen(s):
	p1 = 0
	for i in xrange(len(s)):
		p1 = 2 * p1 + ord(s[i])
	p2 = 0x1337
	print hex(p1)
	s = Solver()
	pvar = list(BitVecs(' '.join([('p%d' % i) for i in xrange(15)]), 16))
	# add ASCII lowercase bounds
	for p in pvar: s.add(p >= 32, p <= 127)
	# add separator
	s.add(pvar[7] == 45)
	# add constraints
	s.add((((pvar[6] + 5 * pvar[1]  + 11 * pvar[2] + 31 * pvar[4]  + 43 * pvar[5] + 3 * (pvar[0] + 9 * pvar[3])) ^ p1) +
		  ((pvar[14]  + 5 * pvar[9] + 11 * pvar[10] + 31 * pvar[12] + 43 * pvar[13] + 3 * (pvar[8] + 9 * pvar[11])) ^ p2)) == 0x5a5a)
	print "[*] Solving key constraints..."
	if s.check() == sat:
		print "[*] Model found!"
		m = s.model()
		pss = []
		for u in pvar: pss.append(chr(m[u].as_long()))
		print('[*] pass = %s' % (''.join(pss)))
		return ''.join(pss)
	else:
		print '[*] Not found'
		raise ArgumentError('key not found')

while True:
	try:
		print r.recvuntil('Name: ', timeout=5)
		s = r.recvline()
		s = s[:-2]
		print s.encode('hex')
		r.sendline(gen(s))
	except Exception as e:
		r.interactive()
		r.close()
		break