You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
46 lines
1.4 KiB
46 lines
1.4 KiB
# coding: utf-8
|
|
import os, sys
|
|
from z3 import *
|
|
|
|
|
|
# 'hashed' password we have from the 'binary'
|
|
hashed_password=168372036536695091
|
|
|
|
# we are going to try different lengths of passwords
|
|
for password_length in range(5,15):
|
|
# init solver, this will wipe any residual constraints in each loop
|
|
solver = Solver()
|
|
|
|
# initialize constraints for each character of the password
|
|
# we are only going to allow ascii values from 'a' to 'z'
|
|
chars = [Int(c) for c in range(password_length)]
|
|
|
|
# initialization value
|
|
n = 7
|
|
# the 'hashing' algorithm we have extracted from the binary
|
|
for c in chars:
|
|
# this essentially extends the symbolic constraints associated with each 'c'
|
|
n = n * 27 + c * 5
|
|
|
|
# the solver should return sat iff
|
|
# the hashed input is equal the hashed_password
|
|
solver.add(n == hashed_password)
|
|
|
|
for c in chars:
|
|
# each 'c' should be a lowercase ascii character
|
|
solver.add(And(c >= ord('a'),
|
|
c <= ord('z')))
|
|
|
|
|
|
res = solver.check()
|
|
if res != sat:
|
|
print("No possible password found...")
|
|
continue
|
|
|
|
# print the model/password found
|
|
m = solver.model()
|
|
for d in m.decls():
|
|
print("%s = %s -> %c" % (d.name(), m[d], chr(m[d].as_long())))
|
|
password = ''.join(chr(m[c].as_long()) for c in chars)
|
|
print("Trying '" + password + "' as password")
|
|
os.system("./password_storage.sh {}".format(password))
|