56 lines
1.1 KiB
Python
56 lines
1.1 KiB
Python
import z3
|
|
import struct
|
|
|
|
N = 624
|
|
L = N
|
|
|
|
with open("init_state.txt", "r") as f:
|
|
init_mt = [int(x.strip()) for x in f]
|
|
|
|
def crack():
|
|
s = z3.Solver()
|
|
|
|
init_key = [z3.BitVec(f"init_key_{i}", 32) for i in range(L)]
|
|
mt = [z3.BitVecVal(x, 32) for x in init_mt]
|
|
|
|
i = 1
|
|
j = 0
|
|
k = N
|
|
while k > 0:
|
|
mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 30)) * z3.BitVecVal(1664525, 32))) + init_key[j] + z3.BitVecVal(j, 32)
|
|
i += 1
|
|
j += 1
|
|
if i >= N:
|
|
mt[0] = mt[N-1]
|
|
i = 1
|
|
if j >= L:
|
|
j = 0
|
|
|
|
k -= 1
|
|
|
|
k = N - 1
|
|
while k > 0:
|
|
mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 30)) * z3.BitVecVal(1566083941, 32))) - z3.BitVecVal(i, 32)
|
|
i += 1
|
|
if i >= N:
|
|
mt[0] = mt[N-1]
|
|
i = 1
|
|
|
|
k -= 1
|
|
|
|
for idx in range(1, N):
|
|
s.add(mt[idx] == 0)
|
|
|
|
s.check()
|
|
m = s.model()
|
|
|
|
x = bytearray()
|
|
for ik in init_key:
|
|
ikv = m[ik].as_long()
|
|
x += struct.pack("<I", ikv)
|
|
|
|
print(hex(int.from_bytes(x, byteorder='little')))
|
|
|
|
if __name__ == "__main__":
|
|
crack()
|