Skip to content

Instantly share code, notes, and snippets.

@shahril96
Created Nov 4, 2019
Embed
What would you like to do?
from z3 import *
import struct
a = [BitVec("a{}".format(i), 8) for i in range(5)]
s = Solver()
def is_valid(x):
return Or(
And(x >= ord('1'), x <= ord('9')),
And(x >= ord('a'), x <= ord('z')),
And(x >= ord('A'), x <= ord('Z'))
)
s.add(
22 == (88 ^ a[4]),
a[3] % 65 == 0,
a[2] + 30 >= 130,
a[1] + a[2] == 161,
2 == (a[0] ^ a[4]),
26 == (a[0] ^ a[1] ^ a[2] ^ a[3] ^ a[4]),
is_valid(a[1]),
is_valid(a[2])
)
if s.check() == sat:
m = s.model()
p = ""
for x in a:
p += chr(m[x].as_long())
print(p)
else:
print("Unsat")
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment