SAT-baserad kryptoanalys
Att översätta ett chiffer till en jättelik boolesk formel och låta en SAT-lösare leta efter nyckeln.
Fabio Massacci och Laura Marraro kallade det logisk kryptoanalys när de år 2000 kodade DES som ett satisfierbarhetsproblem. Med några få ronder hittade lösaren nyckeln; med fulla DES gav den upp, som väntat. Metoden är en nära släkting till algebraiska attacker, men byter polynom mot klausuler och lånar decennier av ingenjörskonst från hårdvaruverifiering.
Genombrottet var praktiskt snarare än teoretiskt. Mironov och Zhang använde 2006 SAT-lösare för att automatisera delar av kollisionssökningen i MD4 och MD5, och Mate Soos byggde CryptoMiniSat med inbyggt stöd för XOR, chiffrens favoritoperation. Idag är det vanligaste bruket att låta lösaren söka bästa differentialkaraktäristik åt den som designar ett nytt chiffer – snarare än att knäcka gamla.