Z3-based solution of ctf.moscow task "line"

solve_line.py

from z3 import *
from cypher import L3LFSR

KEY_LEN = 128
KNOWN = 'CTF.Moscow{eyJ0eXAiOiJKV1QiLCJhbGciOiJFUzI1NiJ9'
#KNOWN = 'CTF.Moscow{e'
KNOWN = 'CTF.Moscow{eyJ0eX'
KNOWN_INT = int.from_bytes(bytes(KNOWN, 'ascii'), 'big')
KNOWN_BITS = list(map(int, bin(KNOWN_INT)[2:]))
KNOWN_LEN = len(KNOWN)
KNOWN_LEN_BITS = KNOWN_LEN * 8

#set_param(verbose=10)
s = Solver()

key = [BitVec('key[%d]' % i, 1) for i in range(KEY_LEN)]

l = L3LFSR(key)

keystream = [l.next_bit() for _ in range(KNOWN_LEN_BITS)]

stream = list(map(int, bin(15431654674465677146819454827465233171964571350967499236697725359993231286059757627400008597646865144639050046270818853942686157345830582813322129182512046270176579954472699404043953165374645857270991371175662784646383631275941900174595887196799412373618038938639208780032241385734529883732286330365045553802901857024695515783622075053490651813863743168720457285662917634129559887260609181306577821695989104064884875844523829716012970088777241874098923781913032792162277)[2:]))

print (len(KNOWN_BITS), len(keystream), len(stream))

for i in range(len(KNOWN_BITS)):
    s.add(stream[i] ^ KNOWN_BITS[i] == keystream[i])

#print(key)
print('check')
print(s.check())
m = s.model()

x = 0
bits = []
for el in key:
    bits.append(m[el].as_long())

print( bits)
for b in bits:
    x = x * 2 + b
print(hex(x))