gctf2023/intro/skilift/solver.py

41 lines
949 B
Python

from z3 import *
# Create a Z3 BitVec variable for key
key = BitVec('key', 64)
# Create Z3 variables for tmp1, tmp2, tmp3, tmp4
tmp1 = BitVec('tmp1', 64)
tmp2 = BitVec('tmp2', 64)
tmp3 = BitVec('tmp3', 64)
tmp4 = BitVec('tmp4', 64)
# Create a Z3 Solver instance
solver = Solver()
# Stage 1
stage1_formula = tmp1 == (key & 0xF0F0F0F0F0F0F0F0)
solver.add(stage1_formula)
# Stage 2
stage2_formula = tmp2 == ((tmp1 << 5) & 0xFFFFFFFFFFFFFFFF)
solver.add(stage2_formula)
# Stage 3
stage3_formula = tmp3 == (tmp2 ^ 0x4841434B45525321)
solver.add(stage3_formula)
# Stage 4
stage4_formula = tmp4 == (tmp3 - 12345678)
solver.add(stage4_formula)
# Final constraint
final_constraint = tmp4 == 0x5443474D489DFDD3
solver.add(final_constraint)
# Check for a solution
if solver.check() == sat:
model = solver.model()
key_value = model[key].as_long()
print(f"The correct value of key is: {hex(key_value)}")
else:
print("No solution found.")