Registre à Décalage à Rétroaction linéaire a.k.a Linear Feedback Shift Register are commonly used as a building block of stream cipher, but they cannot be used alone as Berlekamp Massey algorithm would break it easily. Their security can be enhanced by using a nonlinear filter function like in this challenge. But here the filter isn’t “strong” enough because of it’s low degree and it’s low algebraic immunity (see Claude Carlet’s book to know more about boolean function’s security), so for a solver like z3 the key recovery is easy.
- Length of the LFSR : 64
- Feedback polynomial of the LFSR : $1 + X + X^2 + X^4 + X^5$
- Filter function f : $f(x) = x_{16} + x_0x_{16} + x_0x_{32}x_{48} + x_{16}x_{32} + x_{16}x_{48} + x_{16}x_{48}x_{32}$ ($x_i$ correspond to state[i] in the code)
Necessary lib :
import os
import sys
import bitarray
import random
import subprocess
from z3 import *
Getting the begining of the keystream
We can see thanks to the name of the encrypted file that the flag file is a png image, so we automatically know 18 bytes of plain data from the usual png header. So we can recover 18 bytes of the keystream simply by xoring a png header to the encrypted flag :
#The encrypted flag image
f = open("flag.png.enc", 'rb')
#Just a random png image
g = open("img.png", 'rb')
#Getting the 18 first bytes of the keystream by xoring the png header and the begining of the encrypted flag
for k in range(18):
byte1 = f.read(1)
byte2 = g.read(1)
plain.append(xor(byte1, byte2))
bIn = bitarray.bitarray()
bIn.frombytes(plain)
l = len(bIn)
keystream = [bIn[i] for i in range(l)]
#keystream =[0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1]
Then to make easier the use of z3 we create an LFSR class and a Filter class corresponding to the ones used in the challenge :
class LFSR:
def __init__(self, key, taps):
d = max(taps)
assert len(key) == d, "Error: key of wrong size."
self._s = key
self._t = [d - t for t in taps]
def _sum(self, L):
s = 0
for x in L:
s = s ^ x
return s
def _clock(self):
b = self._s[0]
self._s = self._s[1:] + [self._sum(self._s[p] for p in self._t)]
return b
def bit(self):
return self._clock()
class Filter:
def __init__(self, key):
#The LFSR of the challenge is [0, 1, 3, 4] and of length 64
self.LFSR = LFSR(key, [64 - 0, 64 - 1, 64 - 3, 64 - 4])
def bit(self):
#Our filtering function
state = self.LFSR._s
b = 0
b ^= state[0]*state[N//4]
b ^= state[0]*state[2*N//4]*state[3*N//4]
b ^= state[N//4]*state[2*N//4]*state[3*N//4]
b ^= state[N//4]*state[2*N//4]
b ^= state[N//4]*state[3*N//4]
b ^= state[N//4]
self.LFSR.bit()
return b
The key recovery
#And z3 do the job
s = Solver()
KEY = [BitVec(f"k_{i}", 1) for i in range(N)]
F = Filter(KEY)
for b in keystream:
s.add(F.bit() == b)
assert s.check() == sat
initial_state = ''.join([str(s.model()[k]) for k in KEY])
hstate = str(hex(int(initial_state, 2)))
#hstate = 0x3cdec6e5824d758a
Finaly we just decrypt the flag
subprocess.run("python3 cipher.py flag.png.enc " + hstate + " > flag.png", shell = True, executable="/bin/bash")
Bonus
I said that the filter function f have a low algebraic immunity (AI(f)), to be more precise AI(f) = 1 as the function $g(x) = 1 + x_0 + x_{16} + x_{32} + x_{48}$ is of degree 1 and $\forall x, g(x) * f(x) = 0$ (easy to see doing the calculus with the expression of f).
Knowing that we have new equations of degree 1 instead of degree 3 (the degree of f) which make the system easier to solve. That may possibly be what z3 is using in it’s process (but not only). We can even give those new equations to z3 but it does not fasten the solve (it even make it slower of half a second) :
#In the Filter class we add the annihilator function
def annihilator(self):
state = self.LFSR._s.copy()
self.bit()
return 1 ^ state[0] ^ state[N//4] ^ state[2*N//4] ^ state[3*N//4]
Then :
for b in keystream:
if b :
s.add(F.annihilator() == 0)
else :
s.add(F.bit() == b)