41 lines
949 B
Python
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.")
|