Complete SAT based Cryptanalysis of RC5 Cipher

Keeping the proper security level of ciphers used in communication networks is today a very important problem. Cryptanalysts ensure a constant need for improvement complexity and ciphers' security by trying to break them. Sometimes they do not instantly try to break the strongest version of the cipher, but they are looking for weaknesses by splitting it and independently checking all algorithm components. Often cryptanalysts also attempt to break cipher by using its weaker version or configuration. There are plenty of mechanisms and approaches to cryptanalysis to solve those challenges. One of them is SAT-based method, that uses logical encoding. In this article, we present our wide analysis and new experimental results of SAT-based, direct cryptanalysis of the RC5 cipher. To perform such actions on the given cipher, we initially create a propositional logical formula, that describes and represents the entire RC5 algorithm. The second step is to randomly generate key and plaintext. Then we determine the ciphertext. In the last step of our computations, we use SAT-solvers. They are particularly designed tools for checking the satisfiability of the Boolean formulas. In our research, we make cryptanalysis of RC5 cipher in the case with plaintext and ciphertext. To get the best result, we compared many SAT-solvers and choose several. Some of them were relatively old, but still very efficient and some were modern and popular.