#FlareOn5 12
| #!/usr/bin/env python | |
| from itertools import chain, product | |
| import string | |
| from z3 import * | |
| suffix = '@flare-on.com' | |
| stored = [0xfc7f, 0xf30f, 0xf361, 0xf151, 0xf886, 0xf3d1, 0xdb57, 0xd9d5, 0xe26e, 0xf8cd, 0xf969, 0xd90c, 0xf821, 0xf181, 0xf85f] | |
| c_add = [[], | |
| [10, 15], | |
| [9, 14], | |
| [9, 14, 10, 15], | |
| [8, 13], | |
| [8, 13, 10, 15], | |
| [8, 13, 9, 14,], | |
| [8, 13, 9, 14, 10, 15], | |
| [7, 12], | |
| [7, 12, 10, 15], | |
| [7, 12, 9, 14], | |
| [7, 12, 9, 14, 10, 15], | |
| [7, 12, 8, 13], | |
| [7, 12, 8, 13, 10, 15], | |
| [7, 12, 8, 13, 9, 14]] | |
| LEN = 30 | |
| x = [BitVec("x%d"%i, 32) for i in range(0, LEN)] | |
| sum1 = BitVecVal(0, 32) | |
| diff = BitVecVal(0, 32) | |
| s = Solver() | |
| for i in range(0, len(x)): | |
| s.add(x[i] >= 0x21, x[i] <= 0x7a) | |
| for i in range(0, LEN - len(suffix)): | |
| diff -= 0xc00 | |
| sum1 += x[i] | |
| j = i + 1 | |
| sum1 -= diff | |
| sum1 &= 0xffff | |
| sl = len(suffix) | |
| for i in range(j+1, sl): | |
| s.add(x[j + 1 + i] == ord(suffix[i])) | |
| for i in range(0, int(len(x) / 2)): | |
| xcurr = ((x[i*2 + 1] - 0x20) << 7) + (x[i*2 + 0]) - 0x20 | |
| if not i: | |
| xprev = xcurr | |
| else: | |
| for ii in range(0, 16): | |
| xcurr = xcurr * 2 + 1 | |
| xprev = (xprev * 2) | |
| is_h = 0 | |
| if ii in c_add[i]: | |
| is_h = 1 | |
| xprev += (((xcurr) >> 16) ^ is_h) | |
| xprev &= 0xffff | |
| xcurr &= 0xffff | |
| s.add((xprev + sum1) & 0xffff == stored[i]) | |
| if(s.check() == sat): | |
| m = s.model() | |
| pr = '' | |
| for i in range(0, len(x)): | |
| try: | |
| pr += chr(int(str(m[x[i]]))) | |
| except ValueError: | |
| pr = '<unprintable>' | |
| break | |
| print(pr) | |
| else: | |
| print("unsat") |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment