46 lines
891 B
Python
46 lines
891 B
Python
from z3 import Solver, BitVec, sat
|
|
|
|
def rng(x, size):
|
|
return (x*A+B) & ((2**size)-1)
|
|
|
|
def gen_random(seed, bits, mask):
|
|
state = seed
|
|
while True:
|
|
state = rng(state, bits)
|
|
yield state & mask
|
|
|
|
A = BitVec("A", 56)
|
|
B = BitVec("B", 56)
|
|
SEED = BitVec("seed", 56)
|
|
BITS = 56
|
|
MASK = 0xFF
|
|
|
|
state = SEED
|
|
|
|
with open("./msg.txt", "r") as f:
|
|
nums = [int(n) for n in f.readlines()[1:]]
|
|
print(nums)
|
|
|
|
flag_bytes = [BitVec(f'flag_{i}', 56) for i in range(142)]
|
|
|
|
solver = Solver()
|
|
|
|
for i, n in enumerate(nums):
|
|
state = rng(state, BITS)
|
|
cur_num = state & MASK
|
|
solver.add(n == cur_num ^ flag_bytes[i])
|
|
solver.add(flag_bytes[i] >= 32, flag_bytes[i] <= 126)
|
|
|
|
if solver.check() == sat:
|
|
model = solver.model()
|
|
flag = ''.join([chr(model[flag_bytes[i]].as_long()) for i in range(142)])
|
|
print(model)
|
|
print(flag)
|
|
else:
|
|
print("Not solveable")
|
|
|
|
|
|
|
|
|
|
|