CUSTOMMediumCrypto

UofT LFSR Labyrinth

XESXOR9/10/20267 min read

#crypto#custom#medium#lfsr_state_recovery#sat_cryptanalysis#tseitin_transformation

UofT LFSR Labyrinth

Platform: uoftctf2026 | Category: Crypto | Type: Challenge | Difficulty: Medium | OS: NA | Author: XESXOR | Date: 2026-01-10 | Status: Solved Techniques: lfsr_state_recovery, sat_cryptanalysis, tseitin_transformation

Summary

Given an LFSR with a WG-style (Welch-Gong) nonlinear filter, 80 bits of keystream output, and an encrypted flag.

UofT LFSR Labyrinth — uoftctf2026

Description

"A quirky 48-bit UofT stream taps through a WG-flavoured filter, leaving 80 bits of trace and a sealed flag. The blueprint is public; the hidden state is the dance you need to unravel."

Given an LFSR with a WG-style (Welch-Gong) nonlinear filter, 80 bits of keystream output, and an encrypted flag.

Files

filter_cipher.py - LFSR implementation with WG-style nonlinear filter
crypto.py - ChaCha20-Poly1305 encryption, key derived via HKDF from LFSR state
challenge.json - parameters and data:
- L = 48 (LFSR size)
- feedback_taps = [0, 1, 2, 3, 47]
- filter_taps = [0, 4, 7, 11, 16, 22, 29] (7 taps for WG filter)
- 80 bits keystream
- nonce and ciphertext ‍‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‍

Analysis

LFSR Structure

48-bit state, right shift
Feedback polynomial: x^48 + x^4 + x^3 + x^2 + x + 1
Taps: positions 0, 1, 2, 3, 47

WG Filter

Nonlinear filter in Algebraic Normal Form (ANF):

Takes 7 bits from state at positions [0, 4, 7, 11, 16, 22, 29]
56 ANF terms including degree-6 monomials like (1,2,3,4,5,6)
Output = XOR of AND-products of selected input bits

Key Observation

80 output bits from 48-bit state = overdetermined system!

This is a classic case for SAT attack: we have more equations (80) than unknowns (48). ‍‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‍

Solution

Idea: SAT Encoding

Model the entire cipher as a Boolean satisfiability problem:

48 Boolean variables for the initial LFSR state
For each of the 80 keystream bits:
- Encode the WG filter via Tseitin transformation
- Add constraint: filter output = known keystream bit
- Simulate LFSR clock (XOR feedback, shift)

Tseitin Transformation

Converting ANF to CNF:

AND gate: z = a AND b -> (a OR NOT z) AND (b OR NOT z) AND (NOT a OR NOT b OR z)
XOR gate: via auxiliary variables and XOR chain ‍‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‍

Formula Size

8928 variables
38480 clauses
Solves instantly (< 1 sec)

Solution Code

 python read-only • copy allowed
#!/usr/bin/env python3
"""
SAT-based attack on LFSR with WG-style nonlinear filter
"""
import json
from pysat.solvers import Solver as SATSolver

# Load challenge data
with open('challenge.json', 'r') as f:
    data = json.load(f)

L = data['L']  # 48
feedback_taps = data['feedback_taps']  # [0, 1, 2, 3, 47]
filter_taps = data['filter_taps']      # [0, 4, 7, 11, 16, 22, 29]
keystream = data['keystream']          # 80 bits
‍‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‍

# WG filter ANF terms (56 monomials)
WG_ANF_TERMS = [
    (1, 2, 3, 4, 5, 6), (0, 1, 2, 3, 5), (0, 1, 2, 4, 5), (0, 1, 3, 4, 5),
    (0, 2, 3, 4, 5), (1, 2, 3, 4, 5), (0, 1, 2, 3, 6), (0, 1, 2, 5, 6),
    (0, 1, 3, 5, 6), (0, 2, 3, 5, 6), (1, 2, 3, 5, 6), (0, 1, 4, 5, 6),
    (0, 2, 4, 5, 6), (1, 2, 4, 5, 6), (0, 3, 4, 5, 6), (1, 3, 4, 5, 6),
    (2, 3, 4, 5, 6), (0, 1, 2, 3), (0, 1, 3, 5), (0, 2, 3, 5),
    (1, 2, 3, 5), (0, 1, 4, 5), (0, 2, 4, 5), (1, 2, 4, 5),
    (0, 3, 4, 5), (1, 3, 4, 5), (2, 3, 4, 5), (0, 1, 2, 6),
    (0, 1, 5, 6), (0, 2, 5, 6), (1, 2, 5, 6), (0, 3, 5, 6),
    (1, 3, 5, 6), (2, 3, 5, 6), (0, 4, 5, 6), (1, 4, 5, 6),
    (2, 4, 5, 6), (3, 4, 5, 6), (0, 1, 3), (0, 2, 3),
    (1, 2, 3), (0, 1, 5), (0, 3, 5), (1, 3, 5),
    (2, 3, 5), (0, 4, 5), (1, 4, 5), (2, 4, 5),
    (3, 4, 5), (0, 5, 6), (1, 5, 6), (2, 5, 6),
    (3, 5, 6), (4, 5, 6), (0, 3), (5,)
]
‍‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‍


class CNFBuilder:
    """Build CNF formula with Tseitin encoding"""
    
    def __init__(self):
        self.var_counter = 0
        self.clauses = []
    
    def new_var(self):
        self.var_counter += 1
        return self.var_counter
    
    def add_clause(self, clause):
        self.clauses.append(clause)
    
    def and_vars(self, vars_list):
        """Encode z = AND(vars) using Tseitin transformation"""
        if len(vars_list) == 0:
            # Empty AND = True, return a variable forced to True
            z = self.new_var()
            self.add_clause([z])
            return z
        if len(vars_list) == 1:
            return vars_list[0]
        
        z = self.new_var()
        # z -> (a AND b AND ...) : NOT z OR (a AND b AND ...)
        # Equivalent: for each var v: (NOT z OR v)
        for v in vars_list:
            self.add_clause([-z, v])
        # (a AND b AND ...) -> z : NOT a OR NOT b OR ... OR z
        self.add_clause([-v for v in vars_list] + [z])
        return z
    
    def xor_vars(self, vars_list):
        """Encode z = XOR(vars) using chain of 2-input XORs"""
        if len(vars_list) == 0:
            z = self.new_var()
            self.add_clause([-z])  # Force to False
            return z
        if len(vars_list) == 1:
            return vars_list[0]
        
        result = vars_list[0]
        for v in vars_list[1:]:
            result = self.xor2(result, v)
        return result
    
    def xor2(self, a, b):
        """Encode z = a XOR b"""
        z = self.new_var()
        # z = a XOR b
        # (NOT a OR NOT b OR NOT z) AND (a OR b OR NOT z) AND
        # (a OR NOT b OR z) AND (NOT a OR b OR z)
        self.add_clause([-a, -b, -z])
        self.add_clause([a, b, -z])
        self.add_clause([a, -b, z])
        self.add_clause([-a, b, z])
        return z
    
    def force_true(self, var):
        self.add_clause([var])
    
    def force_false(self, var):
        self.add_clause([-var])
    
    def force_equal(self, var, value):
        if value:
            self.force_true(var)
        else:
            self.force_false(var)
‍‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‍


# Build SAT formula
builder = CNFBuilder()

# Create variables for initial LFSR state
initial_state = [builder.new_var() for _ in range(L)]
state = list(initial_state)

# Process each keystream bit
for ks_bit in keystream:
    # Get filter tap values
    taps = [state[t] for t in filter_taps]
    
    # Encode WG filter: XOR of AND terms
    term_results = []
    for monomial in WG_ANF_TERMS:
        if len(monomial) == 0:
            continue
        term_vars = [taps[i] for i in monomial]
        term_result = builder.and_vars(term_vars)
        term_results.append(term_result)
    
    # XOR all terms
    z = builder.xor_vars(term_results)
    
    # Constrain output to match keystream bit
    builder.force_equal(z, ks_bit == 1)
    
    # Clock LFSR: compute feedback and shift
    feedback_vars = [state[i] for i in feedback_taps]
    fb = builder.xor_vars(feedback_vars)
    state = [fb] + state[:-1]
‍‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‍

print(f"Variables: {builder.var_counter}")
print(f"Clauses: {len(builder.clauses)}")

# Solve
solver = SATSolver(name='g3')
for clause in builder.clauses:
    solver.add_clause(clause)

if solver.solve():
    model = solver.get_model()
    
    # Extract initial state
    recovered_state = []
    for var in initial_state:
        recovered_state.append(1 if model[var-1] > 0 else 0)
    
    print(f"Recovered state: {recovered_state}")
    
    # Convert to bytes for key derivation
    state_bits = ''.join(map(str, recovered_state))
    state_int = int(state_bits, 2)
    state_bytes = state_int.to_bytes(6, 'big')
    
    # Derive key using HKDF and decrypt
    from cryptography.hazmat.primitives.kdf.hkdf import HKDF
    from cryptography.hazmat.primitives import hashes
    from cryptography.hazmat.primitives.ciphers.aead import ChaCha20Poly1305
    import base64
    
    hkdf = HKDF(
        algorithm=hashes.SHA256(),
        length=32,
        salt=None,
        info=b"lfsr-key"
    )
    key = hkdf.derive(state_bytes)
    
    nonce = base64.b64decode(data['nonce'])
    ciphertext = base64.b64decode(data['ciphertext'])
    
    chacha = ChaCha20Poly1305(key)
    plaintext = chacha.decrypt(nonce, ciphertext, None)
    print(f"Flag: {plaintext.decode()}")
else:
    print("UNSAT - no solution found")

‍‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‍

Recovered State

[0, 0, 1, 0, 0, 1, 0, 1, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0]

Alternative Approaches

Algebraic attack - ANF linearization, but 56 terms of degree up to 6 make this impractical
Correlation attack - requires bias in the filter, WG filters are designed to resist this
BDD-based attack - possible, but SAT is simpler to implement

References

Tseitin Transformation
SAT Solvers in Cryptanalysis
WG Stream Cipher Family ‍‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‌‍