Algebraic attacks using SAT-solvers

Algebraic attacks lead to the task of solving polynomial systems over 𝔽 2 . We study recent suggestions of using SAT-solvers for this task. In particular, we develop several strategies for converting the polynomial system to a set of CNF clauses. This generalizes the approach in [Bard, Courtois, Jefferson, Cryptology ePrint Archive 2007, 2007]. Moreover, we provide a novel way of transforming a system over 𝔽 2 e to a (larger) system over 𝔽 2 . Finally, the efficiency of these methods is examined using standard examples such as CTC, DES, and Small Scale AES.