SAT tabanlı kriptanaliz
Bir şifreyi devasa bir Boole formülüne çevirip anahtarı bulmayı bir SAT çözücüye bırakmak.
Fabio Massacci ve Laura Marraro, 2000’de DES’i bir sağlanabilirlik problemi olarak kodladıklarında buna mantıksal kriptanaliz dediler. Birkaç turda çözücü anahtarı buldu; tam DES’te beklendiği gibi pes etti. Yaklaşım, cebirsel saldırıların yakın akrabasıdır, ama polinomların yerine yan tümceler (clause) kullanır ve donanım doğrulamasından on yıllarca mühendislik birikimi ödünç alır.
Atılım kuramsal değil pratikti. 2006’da Mironov ve Zhang, MD4 ve MD5 için çarpışma aramasının bazı kısımlarını otomatikleştirmek için SAT çözücüleri kullandı; Mate Soos ise şifre tasarımcısının en sevdiği işlem olan XOR’u doğrudan destekleyen CryptoMiniSat’ı yaptı. Bugün en yaygın kullanım, eski şifreleri kırmaktan çok, yeni bir şifre tasarlayan biri adına çözücünün en iyi diferansiyel karakteristiği aramasıdır.