Application of SAT oracles for generation of additional linear constraints in cryptanalysis of some lightweight ciphers

In the paper, we propose a new technique that is aimed at algebraic cryptanalysis problems. Using this technique we construct additional linear equations over $\rm{GF}(2)$ which augment the system of algebraic equations presenting the cryptanalysis of the considered cipher. We use a SAT solver to generate such new linear equations. It was shown that the proposed technique allows one to increase the efficiency of guess-and-determine attacks which are based on the linearization sets. Effectiveness of the proposed technique was confirmed by computational experiments in which we considered the cryptanalysis of some variants of well-known stream cipher Trivium with a decreased number of steps in the initialization phase.