SAT-basierte Kryptanalyse
Eine Chiffre in eine gigantische boolesche Formel übersetzen und einen SAT-Solver nach dem Schlüssel suchen lassen.
Fabio Massacci und Laura Marraro nannten es logische Kryptanalyse, als sie 2000 DES als Erfüllbarkeitsproblem kodierten. Bei wenigen Runden fand der Solver den Schlüssel; beim vollen DES gab er erwartungsgemäß auf. Der Ansatz ist ein enger Verwandter algebraischer Angriffe, tauscht aber Polynome gegen Klauseln und profitiert von Jahrzehnten Ingenieurarbeit aus der Hardware-Verifikation.
Der Durchbruch war praktischer, nicht theoretischer Natur. 2006 nutzten Mironov und Zhang SAT-Solver, um Teile der Kollisionssuche für MD4 und MD5 zu automatisieren, und Mate Soos baute CryptoMiniSat mit nativer Unterstützung für XOR, die Lieblingsoperation jedes Chiffre-Entwicklers. Heute lässt man den Solver meist die beste differentielle Charakteristik für jemanden suchen, der eine neue Chiffre entwirft – statt alte zu brechen.