Aero CTF 2020 - Magic II (Crypto, 496pts) Writeup (part 2)

solve.py

from z3 import *

outputs = '011110100001111101000100001101011111010110000110100010101011101110110110100000101110000011101000001001011010100111000110100111011100001000010010111100000000000001001011000010110001001111111011100010010110101001000001110111111110000111110000010001011101101101100010111011101101001010110000001011010110011110011101001001000111101000011001100111001010011101100000011111001101001111000010000010101111000111101100000111010000010110100010011100111010001000100000000110100110110101110000110111111000001010111100000100110011001011100111101110011111001011110010000000101110010011001101101011101011001100111010101111010111011100011110111010001100111010100010110000101010100100010001010110101100101000111001111000111011000000001000001110100000110000101101110111000000000010011011'

initial_state = BoolVector('state', 64)
solver = Solver()

state = initial_state
for _ in range(512):
  new_state = [None] * 64
  for i in range(64):
    a = state[(i - 1) % 64]
    b = state[i % 64]
    c = state[(i + 1) % 64]
    new_state[i] = Xor(Or(a, b), c)
  state = new_state
for output in outputs:
  new_state = [None] * 64
  for i in range(64):
    a = state[(i - 1) % 64]
    b = state[i % 64]
    c = state[(i + 1) % 64]
    new_state[i] = Xor(Or(a, b), c)
  state = new_state
  solver.add(state[0] == (output == '1'))

print('Solving...')
assert(solver.check() == sat)
model = solver.model()
print('SAT', model)

Writeup: https://hackmd.io/@hakatashi/B1OM7HFVI