Also known as: SAT solving, SMT solving, Z3

A SAT solver decides whether a Boolean formula can be made true and, if so, returns an assignment; an SMT solver extends this to richer theories such as fixed-width bit-vectors and arrays, which model byte-oriented ciphers directly.¹² In cryptanalysis the unknown key or substitution table becomes a set of variables, every known message becomes a constraint, and the solver searches for the assignment satisfying all of them at once.

An over-determined system (far more constraints than unknowns) collapses to a single table — or the solver proves no such table exists for the assumed structure.

How it works

Modern solvers use conflict-driven clause learning (CDCL): they guess, propagate the consequences, and on contradiction learn a clause that prunes a large part of the search. This makes them far smarter than brute force for structured problems — they can recover a 256-entry table that is hopeless to enumerate. Their weakness is chained table lookups (a value used to index another lookup), where the case-splitting explodes; there a hand-written constraint propagator can be faster. An unsat result is also informative: it proves the assumed structure cannot fit the data.

Relevance to SDR

When a reverse-engineering problem reduces to “find the hidden table consistent with every message,” it is a satisfiability problem. GopherTrunk’s clean-room analysis of the Motorola P25 talker-alias obfuscation (issue #773) posed the unknown internal substitution table as bit-vector variables in Z3 and asserted the known-plaintext constraints; the runs returned unsat across the tractable structure families, narrowing the space rather than yielding the table.

Sources

1. Satisfiability modulo theories — Wikipedia, for SMT and bit-vector/array theories. ↩

2. Boolean satisfiability problem — Wikipedia, for SAT and CDCL search. ↩

See also

• Algebraic attack
• Constraint propagation
• Brute-force attack (exhaustive key search)
• Known-plaintext attack
• RC4 (ARC4) cipher