solve_lsfr.py

from z3 import *

with open(r"keystream", "rb") as f:
	keystream = f.read()

TOTAL_BITS = len(keystream) * 8

l1 = BitVec("l1", TOTAL_BITS + 48)
l2 = BitVec("l2", TOTAL_BITS + 48)
l3 = BitVec("l3", TOTAL_BITS + 48)

# Go over every byte in the keystream
curr_idx = 48


s = Solver()

print("=== Generating Constraints ===")

l1_init = BitVec("l1_init", 48)
l2_init = BitVec("l2_init", 48)
l3_init = BitVec("l3_init", 48)

s.add(Extract(47, 0, l1) == l1_init)
s.add(Extract(47, 0, l2) == l2_init)
s.add(Extract(47, 0, l3) == l3_init)

for byte in keystream:
	# Go over every bit
	int_val = ord(byte)
	for i in range(8):
		key_bit = (int_val >> (8 - i)) & 1

		l1_bit = Extract(curr_idx, curr_idx, l1)
		l2_bit = Extract(curr_idx, curr_idx, l2)
		l3_bit = Extract(curr_idx, curr_idx, l3)

		# Add constraints for the output bit
		s.assert_and_track(
			l1_bit == 0 ^ Extract(curr_idx - 48, curr_idx - 48, l1) ^ Extract(curr_idx - 48 + 25, curr_idx - 48 + 25, l1),
			"l1_out_" + str(curr_idx)
		)
		s.assert_and_track(
			l2_bit == 0 ^ Extract(curr_idx - 48, curr_idx - 48, l2) ^ Extract(curr_idx - 48 + 34, curr_idx - 48 + 34, l2),
			"l2_out_" + str(curr_idx)
		)
		s.assert_and_track(
			l3_bit == 0 ^ Extract(curr_idx - 48, curr_idx - 48, l3) ^ Extract(curr_idx - 48 + 6, curr_idx - 48 + 6, l3),
			"l3_out_" + str(curr_idx)
		)

		# Add constraint from the keystream
		s.assert_and_track(
			BitVecVal(key_bit, 1) == ((l1_bit & l2_bit) ^ (l2_bit & l3_bit) ^ (l1_bit & l3_bit)),
			"key_out_" + str(curr_idx)
		)

		curr_idx += 1

print("=== Generation Complete ===")

print(s.check())
print(s)
print(s.unsat_core())

modl = s.model()

print(hex(modl[l1_init].as_long()))
print(hex(modl[l2_init].as_long()))
print(hex(modl[l3_init].as_long()))