I have a problem somebody help me

Jan 16, 2015 at 7:35 AM
Edited Jan 16, 2015 at 7:36 AM
I want to solve problem.

I wish get some hint for it.
#!/usr/bin/env python
from z3 import *

## problem
key = 0
tag = "1234" # -> 0x284c912c

def ror(v):
    return ((v << 25) | (v >> 7)) & 0xffffffff

for c in tag:
    key = ror(key)
    key += ord(c) & 0xdf

key = ror(key) + 0x1c
print hex(key)

## solve
s = Solver()
tag = BitVecs('a b c d', 32)
for x in xrange(len(tag)):
    key = ror(key)
    key += tag[x] & 0xdf
key = ror(key) + 0x1c
s.add(tag[0] > 0, tag[0] < 256)
s.add(tag[1] > 0, tag[1] < 256)
s.add(tag[2] > 0, tag[2] < 256)
s.add(tag[3] > 0, tag[3] < 256)
s.add(key == 0x284c912c)
print s.check()
if s.check() == "sat":
    print s.model()
I tried above code but It doesn't work. what I wrong?
Coordinator
Jan 16, 2015 at 4:14 PM
I can only see some code which executes just fine on my machine. The output is as follows:
0x284c912cL
unsat
Could you elaborate on why there seems to be a problem?