UofTCTF 2026 - UofT LFSR Labyrinth

Overview

We are presented with a custom stream cipher implementation involving a Linear Feedback Shift Register (LFSR) and a nonlinear filter function.

Category	Difficulty	Flag
Crypto	Medium	`uoftctf{l33ky_lfsr_w17h_n0n_l1n34r_fl4v0rrrr}`

Analysis

The system describes a classic Nonlinear Filter Generator.

Source Files: crypto.py handles key derivation and encryption, while filter_cipher.py implements the LFSR logic.
Parameters: The LFSR has a state size of 48 bits.
Data: We are given 80 bits of generated keystream, a nonce, and the ct (ciphertext).

System Properties

State Size: The internal state is 48 bits ( $2^{48}$ possibilities). While brute-forcing this is computationally expensive, it is small enough for algebraic attacks.
Overdefined System: We have 48 unknown variables (the initial state bits) but are given 80 bits of output (equations). This suggests the system is solvable.
Vulnerability: The complexity of the filter function (WG-style ANF terms) is high, but the state transitions are linear. A SAT solver (like Z3) can easily model the linear shifts and the nonlinear constraints to recover the initial state essentially instantly.

Solution Strategy

We will perform an algebraic attack using Z3:

Symbolic State: Define 48 symbolic boolean variables representing the initial LFSR state.
Simulation: Replicate the clock() function from filter_cipher.py using Z3 operations. For each of the 80 known keystream bits:
- Calculate the symbolic output of the filter function.
- Add a constraint that this symbolic output must equal the actual keystream bit.
- Symbolically update the LFSR state (shift and XOR feedback).
Solve & Decrypt: Ask Z3 to find a satisfying model (the initial bits). Use these bits to derive the key via HKDF and decrypt the flag using ChaCha20-Poly1305.

1
graph TD
2
    A[Symbolic State (48 vars)] --> B{Loop 80 times}
3
    B --> C[Calc Filter Output]
4
    C --> D[Add Constraint: out == keystream[i]]
5
    D --> E[Clock LFSR State]
6
    E --> B
7
    B -- Done --> F[Z3 Solve]
8
    F --> G[Recover Initial State]
9
    G --> H[Derive Key & Decrypt]

Solver Script

1
import binascii
2
from z3 import *
3
from cryptography.hazmat.primitives.ciphers.aead import ChaCha20Poly1305
4
from cryptography.hazmat.primitives.kdf.hkdf import HKDF
5
from cryptography.hazmat.primitives import hashes
6

7
# --- Challenge Parameters ---
8
L = 48
9
feedback_taps = [0, 1, 2, 3, 47]
10
filter_taps = [0, 4, 7, 11, 16, 22, 29]
11
keystream = [
12
    1, 1, 1, 0, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 1, 0, 0, 0, 0, 1, 1,
13
    1, 1, 1, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 0, 0, 1, 0, 0, 1,
14
    0, 0, 0, 1, 0, 0, 1, 0, 1, 1, 1, 1, 0, 1, 0, 1
15
]
16
nonce_hex = "8592d59a1c2c0491dab7ed39"
17
ct_hex = "d2a9a529dfcb9b02ad497f9ed915285cc175edbd9c2e1c6f2144a7228fd00c2ba2db21470abb6f4de0bdec24c0eeddf13fa1a2935f735d5d429f932a21"
18

19
# ANF Terms (WG-style transformation)
20
WG_ANF_TERMS = [
21
    (1, 2, 3, 4, 5, 6), (0, 1, 2, 3, 5), (0, 1, 2, 4, 5), (0, 1, 3, 4, 5),
22
    (1, 2, 3, 4, 5), (0, 1, 2, 4, 6), (0, 2, 3, 4, 6), (1, 2, 3, 4, 6),
23
    (0, 1, 2, 5, 6), (0, 2, 3, 5, 6), (1, 2, 3, 5, 6), (0, 3, 4, 5, 6),
24
    (1, 3, 4, 5, 6), (0, 1, 2, 4), (0, 1, 2, 5), (1, 2, 3, 5),
25
    (0, 1, 4, 5), (1, 3, 4, 5), (2, 3, 4, 5), (1, 2, 3, 6),
26
    (0, 1, 4, 6), (1, 2, 4, 6), (0, 3, 4, 6), (1, 3, 4, 6),
27
    (1, 2, 5, 6), (0, 3, 5, 6), (1, 4, 5, 6), (2, 4, 5, 6),
28
    (3, 4, 5, 6), (0, 1, 2), (0, 1, 4), (0, 2, 4),
29
    (1, 2, 4), (0, 1, 5), (0, 3, 5), (1, 3, 5),
30
    (2, 3, 5), (3, 4, 5), (0, 1, 6), (0, 3, 6),
31
    (2, 3, 6), (3, 4, 6), (0, 5, 6), (2, 5, 6),
32
    (4, 5, 6), (2, 3), (3, 4), (0, 5),
33
    (3, 5), (1, 6), (3, 6), (4, 6),
34
    (0,), (3,), (5,), (6,)
35
]
36

37
def solve():
38
    print("[*] Setting up Z3 Solver...")
39
    solver = Solver()
40

41
    # 1. Initialize Symbolic State (48 bits)
42
    initial_state = [BitVec(f's_{i}', 1) for i in range(L)]
43
    current_state = list(initial_state)
44

45
    # 2. Simulate LFSR steps
46
    for k_bit in keystream:
47
        # Extract taps for filter function
48
        taps = [current_state[i] for i in filter_taps]
49

50
        # Calculate symbolic output using ANF terms
51
        z_out = BitVecVal(0, 1)
52
        for term in WG_ANF_TERMS:
53
            term_val = BitVecVal(1, 1)
54
            for idx in term:
55
                term_val &= taps[idx] # Logical AND
56
            z_out ^= term_val         # Logical XOR
57

58
        # Constraint: Symbolic output == Known keystream bit
59
        solver.add(z_out == k_bit)
60

61
        # Clock LFSR: Calculate feedback and shift
62
        fb = BitVecVal(0, 1)
63
        for idx in feedback_taps:
64
            fb ^= current_state[idx]
65
        current_state = [fb] + current_state[:-1]
66

67
    # 3. Solve
68
    print("[*] Solving constraints...")
69
    if solver.check() == sat:
70
        print("[+] SAT! Model found.")
71
        model = solver.model()
72
        recovered_bits = [model[v].as_long() for v in initial_state]
73
        print(f"[+] Recovered Initial State: {recovered_bits}")
74
        return recovered_bits
75
    else:
76
        print("[-] UNSAT. Constraints are impossible.")
77
        return None
78

79
def decrypt_flag(state_bits):
80
    print("[*] Deriving key and decrypting...")
81
    # Helper from crypto.py
82
    data = bytes(state_bits)
83
    hkdf = HKDF(algorithm=hashes.SHA256(), length=32, salt=None, info=b"nlfg-ctf")
84
    key = hkdf.derive(data)
85

86
    nonce = binascii.unhexlify(nonce_hex)
87
    ct = binascii.unhexlify(ct_hex)
88
    aead = ChaCha20Poly1305(key)
89

90
    try:
91
        flag = aead.decrypt(nonce, ct, associated_data=None)
92
        print(f"\n[+] FLAG: {flag.decode()}")
93
    except Exception as e:
94
        print(f"[-] Decryption Error: {e}")
95

96
if __name__ == "__main__":
97
    state = solve()
98
    if state:
99
        decrypt_flag(state)

Flag: uoftctf{l33ky_lfsr_w17h_n0n_l1n34r_fl4v0rrrr}