Resumen
In this study, shrinking and self-shrinking keystream generators are analyzed. These generators can be used in stream ciphering. For each generator the following cryptanalysis problem was considered: given a known keystream fragment, find the corresponding 64-bit secret key. Both problems were reduced to Boolean satisfiability problem (SAT), and then parallel CDCL solvers were used to solve them. Solvers of two types were employed. In solvers of the first type the base CDCL algorithm itself is parallelized. Solvers of the second type decompose an original SAT instance into a family of simpler independent subproblems. Computational experiments were held on a computing cluster. As a result, several cryptanalysis instances of the mentioned type were solved. It turned out, that the parallel solvers of the first type suit better for the considered cryptanalysis problems.