Exploring Practicability for Solving a Task Based on the Generalized Cellular Automata via SAT Solvers

The paper deals with exploring practicability to solve a task of the recovery key of generalized cellular automata via SAT solvers. The problem, which we call a task of the key recovery of generalized cellular automata, is under consideration. This task is formulated as follows. The generalized cellular automata, the positive integer s, the initial values of some cells, and the values of some cells after the s steps of the automata are given. It is required to find the initial values of the remaining cells (their number will be called the key length). To solve the task, were tested Picosat, MiniSat, Glucose, Lingeling, and CryptoMiniSat SAT solvers. In further computational experiments, was used the MiniSat, which was the best. The key recovery task was solved for the generalized cellular automata of a small size via the MiniSat SAT solver. Pizer's graphs were used as graphs of the automata. The key length was approximately half the number of the cells in the automata. As a result of the study, it turned out that operation time of a SAT solver quite significantly (several orders of magnitude) exceeds the estimated time of solution using the FPGA exhaustive method, and the empirical dependencies of the SAT-solver operation time on the key length are exponential. The obtained results confirm that SAT solvers disable effective solving a task under consideration. This allows giving the better reasons for the cryptographic security of the crypto-algorithms based on the generalized cellular automata with regard to the cryptanalysis methods using SAT solvers.