Strategies on Algebraic Attacks Using SAT Solvers

SAT solvers are employed in algebraic attacks to stream ciphers in recent years. This attack describes a cipher by a Boolean equation system in the initial state, and then converts the equation system into a SAT instance. After that, attackers use SAT solvers to solve the instance, and thus recover the initial state. In the whole process, many parameters should be optimized and several delicate strategies can be applied to speed up the solving efficiency. In the paper, we propose and summarize these common strategies and, at the same time, we design an automatic tool for algebraic attacks ATAA to give some benchmark analyses and empirical observations based on a stream cipher series named Bivium-n.