SATベース暗号解読

ファビオ・マッサッチとローラ・マラーロは、2000年にDESを充足可能性問題として符号化し、これを「論理的暗号解読」と呼んだ。ラウンド数が少なければソルバーは鍵を見つけたが、フルDESでは予想どおり諦めた。この手法は代数的攻撃の近縁だが、多項式の代わりに節を使い、ハードウェア検証で培われた数十年分の工学を借りている。

突破口は理論ではなく実践にあった。2006年にMironovとZhangが、MD4とMD5の衝突探索の一部をSATソルバーで自動化し、Mate Soosは暗号設計者の好きなXORをネイティブに扱えるCryptoMiniSatを作った。現在もっとも多い用途は、古い暗号を破ることではなく、新しい暗号の設計者に代わって、最良の差分特性をソルバーに探させることだ。