Fsec2017 z3 solution

fsec_solve.py

from z3 import *
import struct

# calculate e,f,d for a given input password
def calc(m):
    e = 0
    f = 0
    d = 0
    for i in xrange(0, len(m)):
        c = ord(m[i])
        e += c
        f ^= c
        d = (struct.unpack("i",struct.pack("I",(d << 0x5)&0xffffffff))[0] - d) + c;
    return d,e,f

# try z3 for a given password length
def check(length):
    print "Try to find a valid password for length: {}".format(length)
    s =  Solver()
    
    # a character has to be one of: APSYD0GNIL1_
    def is_valid(x):
        return Or(
                (x == ord('A')),
                (x == ord('P')),
                (x == ord('S')),
                (x == ord('Y')),
                (x == ord('D')),
                (x == ord('0')),
                (x == ord('G')),
                (x == ord('N')),
                (x == ord('I')),
                (x == ord('L')),
                (x == ord('1')),
                (x == ord('_')))

    # dynamically create a Bit vector for the password length
    vec=""
    for i in xrange(0,length):
        vec += "pw[{}] ".format(i)

    m = BitVecs(vec, 8)

    # add the rules for the alphabet to each character
    for i in xrange(0, length):
        s.add(is_valid(m[i]))

    # init e and f with 0
    e=0
    f=0

    # perform the calculations that can be solved with z3
    # d not included
    for i in xrange(0, length):
        e += m[i]
        f ^= m[i]

    # The extracted rules
    s.add(e == 0x56a)
    s.add(f == 0x28) 
    s.add(((BV2Int(m[0x1]) * BV2Int(m[0x2]) * BV2Int(m[0x3])) / 0x104) == 0x69b) 
    s.add(((BV2Int(m[0x4]) + BV2Int(m[0x5]) - BV2Int(m[0x6])) + BV2Int(m[0x7])) == 0x97) 
    s.add(m[0xd] == m[0xe]) 
    s.add(m[0x2] == m[0x8]) 
    s.add(m[0x7] == m[0xb]) 

    # unecessary: s.add(m[0xc] == (length << 0x2))
    # unecessary: s.add((m[0x0] - m[0x1]) == 0x4) 

    # explorative part. Set certain values by hand
    s.add(m[0] == ord('P'))
    s.add(m[1] == ord('L'))
    s.add(m[2] == ord('A'))
    s.add(m[3] == ord('Y'))
    s.add(m[4] == ord('1'))
    s.add(m[5] == ord('N'))
    s.add(m[6] == ord('G'))
    s.add(m[7] == ord('_'))
    s.add(m[8] == ord('A'))
    s.add(m[9] == ord('N'))
    s.add(m[10] == ord('D'))
    

    # check if there is a solution to those rules
    while s.check() == z3.sat:
        # get a model that satisfies the rules
        model = s.model()
        out = ""
        nope = []
        #print "\n#### Model ####"
        for i in m:
            if str(i):
                out += chr(model[i].as_long()&0xff)
            nope.append(i!=model[i])

        # prevent this solution to come up again
        s.add(Or(nope[:-1]))

        # check if the password satisfies d
        d,e,f = calc(out)
        print length, out, hex(d),hex(e),hex(f), d ==-2098257644
        if d==-2098257644 or d == 0xC177908A:
            print out
            exit()
    print s.check()

for x in [17,19,20]:
    check(x)