| from z3 import *
s = Solver()
x = 0
y = 0
key = [BitVec("i%s" % i, 8) for i in range(6)]
allowed_chars = \
list(range(ord('a'), ord('z')+1))
for byte in key:
# Add individual constraints for each byte
s.add(Or([byte == ch for ch in allowed_chars]))
known = "secret"
for i in range(6):
x += i ^ ord(known[i])
for j in range(6):
y += j ^ key[j]
s.add(x == y)
if s.check() == z3.sat:
m = s.model()
res = ''.join([chr(m.evaluate(key[i]).as_long()) for i in range(6)])
print(f"Solution: {res}") |
==> |