Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
from z3 import *
import sys
login = sys.argv[1]
start_end_two = login[:2]+login[-2:]
asciiSum = sum(map(ord,login))
magicValueLogin = 0xfec0135a ^ int(start_end_two.encode('hex'), 16) ^ asciiSum
password = BitVec("password",64)
magicValuePass = BitVec("magicValuePass",64)
s = Solver()
idx = 7
magicValuePass = (((password&(0xff<<(8*idx)))>>(8*idx))^ (32 * 0xadde + 1) ^ 0xdeadbeef) & 0xffffffff
for i in xrange(6,0,-1):
magicValuePass = (((password&(0xff<<(8*i)))>>(8*i))^ (32 * magicValuePass + 1) ^ 0xdeadbeef) & 0xffffffff
s.add(magicValuePass == magicValueLogin)
if s.check() == sat:
print hex(s.model()[password].as_long())
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.