0CTF 2019 Quals | zer0lfsr

 
from secret import init1,init2,init3,FLAG
import hashlib
assert(FLAG=="flag{"+hashlib.sha256(init1+init2+init3).hexdigest()+"}")

class lfsr():
    def __init__(self, init, mask, length):
        self.init = init
        self.mask = mask
        self.lengthmask = 2**(length+1)-1

    def next(self):
        nextdata = (self.init << 1) & self.lengthmask 
        i = self.init & self.mask & self.lengthmask 
        output = 0
        while i != 0:
            output ^= (i & 1)
            i = i >> 1
        nextdata ^= output
        self.init = nextdata
        return output

def combine(x1,x2,x3):
    return (x1*x2)^(x2*x3)^(x1*x3)

if __name__=="__main__":
    l1 = lfsr(int.from_bytes(init1,"big"),0b100000000000000000000000010000000000000000000000,48)
    l2 = lfsr(int.from_bytes(init2,"big"),0b100000000000000000000000000000000010000000000000,48)
    l3 = lfsr(int.from_bytes(init3,"big"),0b100000100000000000000000000000000000000000000000,48)

    with open("keystream","wb") as f:
        for i in range(8192):
            b = 0
            for j in range(8):
                b = (b<<1)+combine(l1.next(),l2.next(),l3.next())
            f.write(chr(b).encode())

LFSR の問題。 combineで混ぜているせいで単純なアプローチはできない。

が、雑にz3に投げてとける。その他周期が短いLFSRがあることを利用するとか、 tap穴が少ないので値が共通しやすいとかを利用する方法もあるらしい。

注意点として、 上のスクリプトでは テキストモードでwriteしているが、この場合 utf-8にencodeするタイミングで chr(b) と書き込まれる値のバイト値が異なったりする。（例： 0xcc を writeすると 0xc30x8c が書き込まれる）

バイナリモードで読み込むとほしい値が得られないことがあるので、テキストモードで読むこと

hellmanによる解説

https://gist.github.com/hellman/8aceadab98c76d1dd19199b587319fbf

import hashlib
from z3 import *

class lfsr():
    def __init__(self, init, mask, length):
        self.init = init
        self.mask = mask
        self.length = length
        self.lengthmask = 2**(length+1)-1

    def next(self):
        nextdata = (self.init << 1) & self.lengthmask 
        i = self.init & self.mask & self.lengthmask 
        output = 0
        for j in range(self.lengthmask.bit_length() + self.length):
            output ^= LShR(i, j) & 1
        self.init = nextdata ^ output
        return output

def combine(x1,x2,x3):
    return (x1*x2)^(x2*x3)^(x1*x3)

# l1 = lfsr(int.from_bytes(init1,"big"),0b100000000000000000000000010000000000000000000000,48)
# l2 = lfsr(int.from_bytes(init2,"big"),0b100000000000000000000000000000000010000000000000,48)
# l3 = lfsr(int.from_bytes(init3,"big"),0b100000100000000000000000000000000000000000000000,48)

# with open("keystream","wb") as f:
#     for i in range(8192):
#         b = 0
#         for j in range(8):
#             b = (b<<1)+combine(l1.next(),l2.next(),l3.next())
#         f.write(chr(b).encode())

solver = Solver()
init1 = BitVec("init1", 48)
init2 = BitVec("init2", 48)
init3 = BitVec("init3", 48)

l1 = lfsr(init1,0b100000000000000000000000010000000000000000000000,48)
l2 = lfsr(init2,0b100000000000000000000000000000000010000000000000,48)
l3 = lfsr(init3,0b100000100000000000000000000000000000000000000000,48)


with open("keystream", "r") as f:
    keystream = f.read()
stream = []
for i, k in enumerate(keystream):
    for j in range(7, -1, -1):
        stream.append( (ord(k) >> j) & 1 )


for b in stream[:23*8]:
    o = combine(l1.next(), l2.next(), l3.next())
    solver.add(o == b)

print(solver.check())
model = solver.model()
print(model[init1].as_long())
print(model[init2].as_long())
print(model[init3].as_long())