Estimations of cryptographic resistance of ciphers in the Trivium family to SAT-based cryptanalysis

Here we present the cryptanalysis results for three stream ciphers in the Trivium family: Bivium, Trivium toy, and Bivium toy. The cryptanalysis was performed via reducing the inversion problems for corresponding discrete functions to Boolean satisfiability problem (SAT). This approach made it possible to perform the cryptanalysis of Bivium toy cipher using common sequential SAT solvers. On average, to solve one cryptanalysis instance for Bivium toy on one core of AMD Opteron 6276 processor, it took about two minutes. For cryptanalysis of Bivium, we designed a variant of “guess-and-determine” attack, in which it is assumed that the values of the last 9 cells at the end of the second Bivium register are known. Thus, the problem is to find values of 168 remaining cells of Bivium registers (the total length of two registers used in Bivium is 177 bits). For this purpose, we analyze 200 bits of keystream. To solve one corresponding cryptanalysis instance, it took about two weeks of work of volunteer computing project SAT@home. The Trivium toy cipher, in its non-weakened form, turned out to be highly resistant to SAT-based cryptanalysis. It proves once more that the general design of the Trivium cipher is very good. We considered the recovery problem for values of registers in Trivium toy based on 100 bits of keystream. At the current stage, we only managed to perform in a reasonable time the variant of “guess-and-determine” attack, in which we know the initial values of the first 16 cells of the second register. Thus, in the corresponding cryptanalysis instances, we need to find values of remaining 80 out of 96 cells. Using the computing cluster of Irkutsk Supercomputer center SB RAS, we managed to solve several instances of Trivium toy cryptanalysis. For this purpose, we used the PD-SAT parallel solver developed in ISDCT SB RAS. On average, to solve one instance using 320 cores of AMD Opteron 6276, it took about one day.