Skip to content

Instantly share code, notes, and snippets.

@akiym
Created Sep 7, 2016
Embed
What would you like to do?
Cello Rule - Tokyo Westerns / MMA CTF 2nd 2016
# -*- 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()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment