An All-SAT Algorithm And Its Applications Of Analysis On Trivium And Lex

Over the last twenty years, efficient and practical SAT algorithms have always been theresearch hotspot in the fields of Artificial Intelligence, Integrated Circuit, Graph Theory, andothers. People become interested in SAT algorithm’s applications in cryptology since MiniSAT, aclassic SAT solver, was used to solve nonlinear multivariable equations for the first time in2007.And SAT solvers performed amazing when they were used to implement algebraic attacks onseveral block ciphers and stream ciphers, such as DES, Keeloq, Crypto-1, HiTag2, and Bivium.However, normal SAT solvers will terminate when finding one solution. It cannot deal withthe situation in which there is more than one solution. And the ALL-SAT solver, which mainlyappears in EDA (Electric Design Automation), is not researched wildly nowadays and based onthe circuit representation mostly. It will be inefficient that applying the existing ALL-SATsolvers to cryptanalysis directly.In this paper, we introduced an ALL-SAT algorithm for solving nonlinear multivariableequations specifically. Its correctness and categoricalness were been proved as well. When therewere a large number of solutions of the equations, the average solving time of each solutionsolved by the ALL-SAT solver would be far below the solving time of one solution solved by anormal SAT solver.In2008, Alex Biryukov et al found the key/IV slid pairs in Trivium up to112shifts, andestimated that it needed about64days to find slid pairs of115shifts. With the ALL-SAT solverintroduced in this paper, we found all the slid pairs of120shifts in Trivium in90minutes.An algebraic attack was given on Lex(2,2,4) in2010, which was a small scale variant ofstream cipher Lex and had only2subkeys used in the keystream generation process. With theALL-SAT solver, an attacker can implement an algebraic attack on Lex(10,2,2,4) in which10subkeys are used in the keystream generation process, and recover the secret key in15minutes.Jianyong Huang presented a differential fault analysis on Lex in2010, which required40faults, and the secret key could be recovered with operations. An attacker can adopt asimilar method presented in this paper to recover the secret key immediately by inserting only20faults. According to the method of algebraic analysis, an attacker can also recover the secret keyin about6seconds with the ALL-SAT solver, by inserting16faults.