CTFZONE 2021 OTP30

solve.py

#!/usr/bin/env python3
import functools
import operator
import sys
import z3


def rev(state):
  s = z3.Solver()
  old = z3.Bools(' '.join(f'a{i}' for i in range(len(state))))
  new = z3.Bools(' '.join(f'b{i}' for i in range(len(state))))
  for i in range(len(state)):
    s.add(new[i] == z3.Xor(old[(i - 1) % len(state)], z3.Or(old[i], old[(i + 1) % len(state)])))
    s.add(new[i] == bool(state[i]))
  assert s.check() == z3.sat
  m = s.model()
  res = [int(bool(m[t])) for t in old]
  
  t = False
  for i in range(len(old)):
    t = z3.Or(t, old[i] != bool(res[i]))
  s.add(z3.simplify(t))
  assert s.check() == z3.unsat

  return res


def bit(state):
  return functools.reduce(operator.xor, state)


def main():
  state = open('state.txt').read().split('\n')[0]
  state = list(map(int, state))
  enc = open('encrypted_flag.bin', 'rb').read()
  key = []
  total = len(enc) * 8
  for i in range(total):
    print('\r', i, '/', total, end='')
    sys.stdout.flush()
    key.append(bit(state))
    state = rev(state)
  key = key[::-1]
  print('\r', key)
  key = [int(''.join(map(str, key[i:i+8])), 2) for i in range(0, len(key), 8)]
  print(key)
  print(bytes([x^y for x,y in zip(enc, key)]))


if __name__ == '__main__':
  main()