150 lines
3.1 KiB
Python
150 lines
3.1 KiB
Python
#!/usr/bin/env python
|
|
|
|
import pwn
|
|
import sys
|
|
import re
|
|
import binascii
|
|
import random
|
|
|
|
N = 128
|
|
_ROL_ = lambda x, i : ((x << i) | (x >> (N-i))) & (2**N - 1)
|
|
_ROR_ = lambda x, i : ((x >> i) | (x << (N-i))) & (2**N - 1)
|
|
|
|
class HashRoll:
|
|
def __init__(self):
|
|
self.reset_state()
|
|
|
|
def hash_step(self, i):
|
|
r1, r2 = self.state[2*i], self.state[2*i+1]
|
|
r = _ROL_(self.state[-2], r1) ^ _ROL_(self.state[-1], r2)
|
|
print(f'h{i} = {r}')
|
|
return r
|
|
|
|
def update_state(self, state=None):
|
|
if not state:
|
|
self.state = [0] * 6
|
|
self.state[:4] = [random.randint(0, N) for _ in range(4)]
|
|
self.state[-2:] = [random.randint(0, 2**N) for _ in range(2)]
|
|
else:
|
|
self.state = state
|
|
|
|
def reset_state(self):
|
|
self.update_state()
|
|
|
|
def digest(self, buffer):
|
|
buffer = int.from_bytes(buffer, byteorder='big')
|
|
m1 = buffer >> N
|
|
m2 = buffer & (2**N - 1)
|
|
self.h = b''
|
|
for i in range(2):
|
|
self.h += int.to_bytes(self.hash_step(i) ^ (m1 if not i else m2), length=N//8, byteorder='big')
|
|
return self.h
|
|
|
|
|
|
def parity(x):
|
|
res = 0
|
|
while x:
|
|
res ^= x & 1
|
|
x >>= 1
|
|
return res
|
|
|
|
|
|
def compute_yc(x):
|
|
import z3
|
|
s = z3.Solver()
|
|
y = z3.BitVec("y", N)
|
|
c = z3.BitVec("c", N)
|
|
s.add((y ^ z3.RotateLeft(y,c)) == x)
|
|
s.check()
|
|
m = s.model()
|
|
|
|
return m[y].as_long(), m[c].as_long()
|
|
|
|
# h = m1 ^ h(0) + m2 ^h(1)
|
|
# h(x) = rol(s1, vx1) ^ rol(s2, vx2)
|
|
|
|
# given x, y is it possible to find:
|
|
# s1, s2, r1, r2, r3, r4,
|
|
# so that rol(s1, r1) ^ rol(s2, r2) = x
|
|
# and rol(s1, r3) ^ rol(s2, r4) = y
|
|
# r1 = 0, r2 = 0, r3 = 0
|
|
# x = s1 ^ s2
|
|
# rol(s1, r3) ^ rol(s2, r4) = y
|
|
|
|
# h0 = rol(s1, r1) ^ rol(s2, r2)
|
|
# s1 = (h0^y)
|
|
# r1, r2 = 0
|
|
# s2 = y
|
|
# r3 = 0, r4 = c
|
|
def solve_round(h1, h2):
|
|
"""
|
|
Return r1,r2,r3,r4,s1,s2 such that
|
|
_ROL_(s1, r1) ^ _ROL(s2, r2) == h1
|
|
_ROL_(s1, r3) ^ _ROL(s2, r4) == h2
|
|
"""
|
|
y,c = compute_yc(h1^h2)
|
|
|
|
s1 = h1^y
|
|
s2 = y
|
|
r1, r2, r3, r4 = 0, 0, 0, c
|
|
j = 1
|
|
|
|
|
|
# ensure non-zero vals
|
|
return [r1+j, r2+j, r3+j, (r4+j) % N, _ROR_(s1, j), _ROR_(s2, j)]
|
|
|
|
r = pwn.remote(sys.argv[1], int(sys.argv[2]))
|
|
|
|
|
|
|
|
|
|
hashfunc = HashRoll()
|
|
|
|
|
|
|
|
|
|
ROUNDS = 3
|
|
|
|
for i in range(ROUNDS):
|
|
r.recvuntil(b"/3!\n")
|
|
l = r.recvuntil(b"\n").decode()
|
|
print(l)
|
|
|
|
|
|
m = re.search(r'H\(([0-9a-f]+)\) = ([0-9a-f]+)', l)
|
|
|
|
|
|
message, h = map(lambda x: int(x, 16), m.groups())
|
|
|
|
m1 = message >> N
|
|
m2 = message & (2**N - 1)
|
|
|
|
th1 = h >> N
|
|
th2 = h & (2**N - 1)
|
|
|
|
print(f'H({hex(message)[2:]}) = {hex(h)[2:]}')
|
|
|
|
h0 = th1 ^ m1
|
|
h1 = th2 ^ m2
|
|
|
|
state = solve_round(h0, h1)
|
|
hashfunc.update_state(state)
|
|
print(hashfunc.digest(message.to_bytes(N, byteorder='big')))
|
|
print(h.to_bytes(2*N//8, byteorder='big'))
|
|
print(hashfunc.digest(message.to_bytes(N, byteorder='big')) == h.to_bytes(2*N//8, byteorder='big'))
|
|
print(state)
|
|
|
|
r.recvuntil(b' :: ')
|
|
|
|
r.sendline(b','.join(map(lambda x: str(x).encode(), state)))
|
|
|
|
print(r.recvline().decode())
|
|
print(r.recvline().decode())
|
|
|
|
|
|
|
|
# we want hashstep(0) to be m3 ^ m1
|
|
# we want hashstep(1) to be m4 ^ m2
|
|
|
|
|