# Create to bit-vectors of size 32 from z3 import * x, y, z = BitVecs('x y z', 64) s = Solver() KeyStream = [0] * 40 key1 = [101, 5, 80, 213, 163, 26, 59, 38, 19, 6, 173, 189, 198, 166, 140, 183, 42, 247, 223, 24, 106, 20, 145, 37, 24, 7, 22, 191, 110, 179, 227, 5, 62, 9, 13, 17, 65, 22, 37, 5] num = -1 for i in range(320): x = (((x >> 29 ^ x >> 28 ^ x >> 25 ^ x >> 23) & 1) | x << 1) y = (((y >> 30 ^ y >> 27) & 1) | y << 1) z = (((z >> 31 ^ z >> 30 ^ z >> 29 ^ z >> 28 ^ z >> 26 ^ z >> 24) & 1) | z << 1) flag = i % 8 == 0 if flag: if i!=0: s.add(KeyStream[num] == key1[num]) num += 1 KeyStream[num] = (KeyStream[num] << 1) | (((z >> 32 & 1 & (x >> 30 & 1)) ^ (((z >> 32 & 1) ^ 1) & (y >> 31 & 1)))) print(s.check()) print(s.model()) # [y = 868387187, x = 156324965, z = 3131229747]
标签：24,26,22,挨打,30,29,32 From： https://www.cnblogs.com/Jh12/p/16615311.html