UofT LFSR Labyrinth
XESXOR9/2/20267 min read
#crypto#custom#medium#lfsr_state_recovery#sat_cryptanalysis#tseitin_transformation
UofT LFSR Labyrinth
Platform: CUSTOM | Category: Crypto | Type: Challenge | Difficulty: Medium | OS: N/A | **Author: XESXOR Techniques: lfsr_state_recovery, sat_cryptanalysis, tseitin_transformation
Summary
Walkthrough of the CUSTOM Crypto UofT LFSR Labyrinth. Given an LFSR with a WG-style (Welch-Gong) nonlinear filter, 80 bits of keystream output, and an encrypted flag.
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 filtercrypto.py- ChaCha20-Poly1305 encryption, key derived via HKDF from LFSR statechallenge.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
Key Takeaways / Lessons
- Mastering lfsr_state_recovery, sat_cryptanalysis, tseitin_transformation was key to this challenge.
- Always check for common misconfigurations and verify assumptions.
Crafted by XESXOR Research • 2026-01-10 • CUSTOM • UofT LFSR Labyrinth • Difficulty: Medium