Towards Complete SAT-based Cryptanalysis of RC5 Cipher

There are many concepts and methods of ciphers cryptanalysis. It depends on the type of the cipher investigated or sometimes modes of operations. Usually, cryptanalysts would like to check some important properties of well known and used ciphers, where so far there is no possibility to break them. Investigators try sometimes break a weaker version of the cipher for understanding which and how proper cipher's parts are cryptographically strong. SAT-based cryptanalysis is one of the used and efficient ways to investigate important properties of some symmetric ciphers. In this paper, we show our investigations and new experimental results in the case of SAT-based, direct cryptanalysis of the RC5 cipher. For this solution, having a given cipher, we firstly built a propositional logical formula that encodes the RC5 algorithm. Next, we randomly generate plaintext and a key. Then we compute the ciphertext. At the end of our computations, we use SAT-solvers, specially designed tools for checking about satisfiability of the Boolean formulas. For our experiments, we explore RC5 properties in the case of cryptanalysis with plaintext and ciphertext. In our investigations, we use and compare several SAT solvers: a few new ones and a few rather old but still efficient. We present our results in the case of a little bit weaker version of the RC5 cipher.