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.

Variants

The choice between SAT and SMT is really a choice of encoding level. A pure SAT solver wants everything reduced to Boolean clauses (CNF); a cipher’s arithmetic must be “bit-blasted” into individual gates, which is expressive but verbose. An SMT solver keeps higher-level theories — bit-vectors for word arithmetic, arrays for lookup tables, linear arithmetic — so the same S-box lookup is one array constraint instead of thousands of clauses, and the solver’s internal theory reasoners handle it more efficiently than raw bit-blasting. Practical tools such as Z3, CVC5, and CryptoMiniSat also support incremental solving (add constraints and re-solve without restarting) and unsat cores (a minimal subset of constraints that already conflict), both valuable when narrowing down which structural assumption is wrong.

In practice

The solver is only as good as the model handed to it. A faithful encoding of the assumed cipher structure is essential — an over-constrained or subtly wrong model can return unsat for the wrong reason, appearing to rule out a structure that is actually correct. Analysts therefore validate the encoding on a known toy instance before trusting a sat/unsat verdict on the real problem, and treat unsat as “no solution of this assumed form,” not “no solution at all.”

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
• Differential cryptanalysis