from z3 import Function, BitVec, BitVecSort,RealSort
from Crypto.Util.number import long_to_bytes
from hashlib import sha256
Pbox=[1, 5, 9, 13, 2, 6, 10, 14, 3, 7, 11, 15, 4, 8, 12, 16]
Sbox=[14, 13, 11, 0, 2, 1, 4, 15, 7, 10, 8, 5, 9, 12, 3, 6]
self.key = [BitVec(f'k_{i}', 1) for i in range(32)]
self.sbox = [14, 13, 11, 0, 2, 1, 4, 15, 7, 10, 8, 5, 9, 12, 3, 6]
self.pbox = [1, 5, 9, 13, 2, 6, 10, 14, 3, 7, 11, 15, 4, 8, 12, 16]
self.f = z3.Function('sbox', z3.BitVecSort(1), z3.BitVecSort(1), z3.BitVecSort(1), z3.BitVecSort(1), z3.BitVecSort(4))
def round_func(self, X, r, K):
XX[i] = X[i] ^ K[kstart + i]
s_value = self.f(XX[4 * i:4 * i + 4])
s_list = [z3.Extract(i, i, s_value) for i in range(4)]
XX[4 * i], XX[4 * i + 1], XX[4 * i + 2], XX[4 * i + 3] = s_list[0], s_list[1], s_list[2], s_list[3]
Y = self.round_func(X, 1, K)
Y = self.round_func(Y, 2, K)
Y = self.round_func(Y, 3, K)
Y = self.round_func(Y, 4, K)
cs = [[0, 0, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1],
[0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 1, 1, 0],
[0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 1],
[0, 1, 1, 1, 1, 0, 1, 0, 1, 0, 0, 0, 0, 1, 1, 1]]
s.add(c.f([int(_) for _ in list(bin(i)[2:].rjust(4, '0'))]) == c.sbox[i])
s.add(z3.simplify(hint[j]) == cs[i][j])
print('----------------')
mb_key = int(''.join([str(m.evaluate(key).as_long()) for key in c.key]), 2)
hash_value = sha256(long_to_bytes(mb_key)).hexdigest()
print("L3HCTF{" + hash_value + "}")
# L3HCTF{852e3b2ae059c411ee14c7c460dcbaed483b3858cb680e10d211e256cf4b639e}