Algebraic cryptanalysis of 9 rounds of lightweight block cipher Simon32/64

A lightweight block cipher Simon32/64 from the Simon family is considered. Its full version consists of 32 rounds. Cryptanalysis of the first 8 rounds has already been repeatedly performed via SAT, i.e., by reducing to the Boolean satisfiability problem and applying SAT solvers. However, for 9 rounds this is still a challenging problem for the SAT approach. In the paper, a SAT encoding for cryptanalysis of the first 9 rounds of Simon32/64 is constructed. Three classes of cryptanalysis problems are formed depending on how the plain text is chosen. Provided that 16 out of 64 bits of each secret key are known, all the problems were solved via a parallel SAT solver.