#!/usr/bin/env python

# Copyright (c) 2016 - Digital Operatives LLC
# All rights reserved
#
# Written by Evan Sultanik, Ph.D.
# evan@sultanik.com
# 
# This source code is licensed under the GNU GENERAL PUBLIC LICENSE
# Version 2.
# 
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
# A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT
# OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
# SPECIAL EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
# LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
# DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
# THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
# (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

import z3

def hash_it_spyeye(name):
    j = 0
    for c in name:
        left = (j << 0x07) & 0xFFFFFFFF
        right = (j >> 0x19)
        j = left | right
        j = j ^ ord(c)
    return j

def build_problem(solver, string_length, prev_hash = None, _char_vars = None):
    if _char_vars is None:
        _char_vars = []
    if prev_hash is None:
        prev_hash = z3.BitVec("init_hash", 32)
        solver.add(prev_hash == 0)
    if string_length <= 0:
        return prev_hash, _char_vars
    else:
        c = z3.BitVec("c" + str(string_length), 32)
        solver.add(c >= 65)
        solver.add(c <= 90)
        _char_vars.append(c)
        h = z3.BitVec("hash" + str(string_length), 32)
        solver.add(h == ((prev_hash << 0x07) | z3.LShR(prev_hash, 0x19)) ^ c)
        return build_problem(solver, string_length - 1, h, _char_vars)

def solve(hash_to_collide, starting_length = 1):
    i = starting_length
    yielded = False
    while not yielded:
        print "Trying string length %d..." % i

        solver = z3.Solver()

        h, char_vars = build_problem(solver, i)

        solver.add(h == hash_to_collide)
        
        while solver.check() == z3.sat:
            m = solver.model()
            yield "".join(map(chr, map(lambda c : m[c].as_long(), char_vars)))
            yielded = True
            asmts = []
            for c in char_vars:
                asmts.append(c != m[c])
            solver.add(z3.Or(*asmts)) # prevent next model from using the same assignment as a previous model
            
        i += 1

if __name__ == "__main__":
    import sys
    to_collide = hash_it_spyeye(sys.argv[1])
    print "Finding a hash collision for string \"%s\" (hash = %s)" % (sys.argv[1], hex(to_collide))
    for collision in solve(to_collide, len(sys.argv[1])):
        print "Collision: %s\t(hash = %s)" % (collision, hex(hash_it_spyeye(collision)))
        sys.stdout.flush()