Skip to content

Instantly share code, notes, and snippets.

@sudhackar
Created October 9, 2017 08:09
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save sudhackar/ccd20ec5b412f8aae4fba651be8e8429 to your computer and use it in GitHub Desktop.
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