Cello Rule - Tokyo Westerns / MMA CTF 2nd 2016

solve.py

# -*- coding: utf-8 -*-
from z3 import *

s = Solver()

seed1 = [BitVec('s1_%d' % i, 64) for i in range(64+1)]
seed2 = [BitVec('s2_%d' % i, 64) for i in range(64+1)]
r1 = BitVec('r1', 64)
r2 = BitVec('r2', 64)

bit = lambda n, x: Extract(n, n, x)

def solve(seed, r):
    for t1 in range(63, -1, -1):
        s.add(bit(0, seed[t1+1]) == bit(t1, r))
        for t2 in range(64):
            tmp = (seed[t1+1] << ((0x41 - t2)&0x3f) | LShR(seed[t1+1], ((t2 - 0x1)&0x3f))) & 7
            v = LShR(0x1e, tmp)
            s.add(bit(t2, seed[t1]) == bit(0, v))

solve(seed1, r1)
solve(seed2, r2)
s.add(seed1[0] == seed2[64])
s.add(r1 == 0x71fa5788e562362b)
s.add(r2 == 0xf18dd1fb9805c360)

if s.check() == sat:
    m = s.model()
    print '%x' % m[seed1[64]].as_long()