A bit-vector differential model for the modular addition by a constant and its applications to differential and impossible-differential cryptanalysis (Q2161424)

ARX algorithms are a class of symmetric-key algorithms constructed by addition, rotation, and XOR. To evaluate the resistance of an ARX cipher against differential and impossible differential cryptanalysis, the recently automated methods employ constraint satisfaction solvers to search for optimal characteristics or impossible differentials. The main difficulty in formulating this search is finding the differential models of the non-linear operations. While an efficient bit-vector differential model was obtained for the modular addition with two variable inputs, no differential model for the modular addition by a constant has been proposed so far, preventing ARX ciphers including this operation from being evaluated with automated methods. In this paper, the authors present the first bit-vector differential model for the n-bit modular addition by a constant input. Their model contains \(O(\log_2(n))\) basic bit-vector constraints and describes the binary logarithm of the differential probability. They describe an SMT-based automated method that includes their model to search for differential characteristics of ARX ciphers including constant additions. They also introduce a new automated method for obtaining impossible differentials where they do not search over a small pre-defined set of differences, such as low-weight differences, but let the SMT solver search through the space of differences. Moreover, They implement both methods in their open-source tool ArxPy to find characteristics and impossible differentials of ARX ciphers with constant additions in a fully automated way. As some examples, they provide related-key impossible differentials and differential characteristics of TEA, XTEA, HIGHT, LEA, SHACAL-1, and SHACAL-2, which achieve better results compared to previous works.