SAT-gebaseerde cryptanalyse
Een cijfer vertalen naar een enorme booleaanse formule en een SAT-solver op zoek sturen naar de sleutel.
Fabio Massacci en Laura Marraro noemden het logische cryptanalyse toen ze in 2000 DES als vervulbaarheidsprobleem codeerden. Bij een paar rondes vond de solver de sleutel; bij volledig DES gaf hij het op, zoals te verwachten. De aanpak is een naaste verwant van algebraïsche aanvallen, maar ruilt polynomen in voor clausules en leent decennia aan techniek uit hardwareverificatie.
De doorbraak was praktisch eerder dan theoretisch. In 2006 gebruikten Mironov en Zhang SAT-solvers om delen van de botsingszoektocht voor MD4 en MD5 te automatiseren, en Mate Soos bouwde CryptoMiniSat met ingebouwde ondersteuning voor XOR, de favoriete bewerking van de cijferontwerper. Tegenwoordig laat men de solver vooral zoeken naar de beste differentiële karakteristiek ten behoeve van wie een nieuw cijfer ontwerpt – in plaats van oude te breken.