Generalized Procedure for Cryptanalysis of ARX-Based Block Ciphers

Satisfiability Modulo Theories (SMT) investigate the functionality of first-order formulas that utilize operations from various theories, including Booleans, bit-vectors, arithmetic, arrays, and recursive data forms. SMT solvers can efficiently resolve a wide range of logic, evaluate hardware and software security, and determine solutions in polynomial time. This paper introduces an algebraic cryptanalysis algorithm that effectively and precisely detects vulnerabilities in bit-level operations by utilizing the SMT solver. The proposed method changes a cryptographic algorithm into a format that an SMT solver can understand. The solver then finds keys for plaintext–ciphertext pairs. This method can also be used to develop new cryptanalytic methods to find cryptographic algorithm weaknesses. Furthermore, this approach is also useful for automated verification, testing of cryptographic algorithms and developing new cryptographic algorithms that are more immune to cryptanalytic attacks. The case study shows the SPECK block cipher cryptanalysis results of the proposed method. For instance, the case study showed how the SPECK block cipher could recover a partial round (up to 4 rounds) key in less than 1214 minutes using the proposed approach, which would have taken more than a day to get a key using traditional cryptanalytic techniques. Overall, this method provides an effective way to analyze cryptographic algorithms and is a powerful tool for analysts.