Criptoanálisis basado en SAT
Traducir un cifrado a una fórmula booleana gigantesca y dejar que un solucionador SAT busque la clave.
Fabio Massacci y Laura Marraro lo llamaron criptoanálisis lógico cuando, en 2000, codificaron DES como un problema de satisfacibilidad. Con pocas rondas el solucionador encontraba la clave; con DES completo se rendía, como era de esperar. El enfoque es pariente cercano de los ataques algebraicos, pero cambia polinomios por cláusulas y aprovecha décadas de ingeniería procedentes de la verificación de hardware.
El avance fue más práctico que teórico. En 2006 Mironov y Zhang usaron solucionadores SAT para automatizar parte de la búsqueda de colisiones en MD4 y MD5, y Mate Soos creó CryptoMiniSat con soporte nativo para XOR, la operación favorita de los diseñadores de cifrados. Hoy su uso más habitual es buscar la mejor característica diferencial para quien diseña un cifrado nuevo, más que romper los viejos.