Solution for laz3y (350) - Byte Bandits CTF 2018

solve-laz3y.py

#!/usr/bin/env python
from z3 import *

''' JS Code =>
190     value[29] == "!" &&           //X// payload[29]         = '!'
191     value[4] == value[8] &&       //X// 08 & 04             = '_'
192     value[17] == "_" &&           //X// payload[17]         = '_'
193     value[4] == "_" &&            //X// payload[4]          = '_'
194     leng(value) &&                //X// len(payload)       == 30
195     crypto(value) &&              //X// payload[18:29]     == 0bfuscati0n
196     value[10] == value[14] &&   // p[10] == p[14]
197     a(value) &&                 // p[3] - p[0] == 32 && p[5] - p[12] == 71
198     b(value) &&                   //X// p[12] == p[15] &&
199                                   //X// p[11] == "l" &&
200                                   //X// p[12] == "0" &&
201                                   //X// p[13] == "T" &&
202                                   //X// p[0]  == p[13]
203     c(value) &&                 // p[9] + p[6] - p[1] == 58;
204     d(value) &&                 // (p[0] * p[1] * p[2] * p[3]) / 128 === 767949;
205     f(value)) {                 // (p[5] * p[6] * p[7]) / 25 === 35581;
'''

partial = 'T???_???_??l0T?0?_0bfuscati0n!'
s = Solver()
flag = [Int(i) for i in xrange(30)]

for x in range(0, 30):
  s.add(flag[x] >= ord('!') and flag[x] <= ord('z'))

for x in range(len(partial)):
  if partial[x] is not '?':
    s.add(flag[x] == ord(partial[x]))

s.add(flag[10] == flag[14])
s.add(flag[3] - flag[0] == 32)
s.add(flag[5] - flag[12] == 71)
s.add(flag[9] + flag[6] - flag[1] == 58)
s.add((flag[0] * flag[1] * flag[2] * flag[3]) / 128 == 767949)
s.add((flag[5] * flag[6] * flag[7]) / 25 == 35581)

# fix errors:
s.add(flag[1] == ord('h'))
s.add(flag[9] != ord('/'))
s.add(flag[10] == ord('_'))

if s.check() == sat:
  m = s.model()
  print 'Flag{' + ''.join([chr(m[x].as_long()) for x in flag]) + '}'
else:
  print 'Not Found.'