Towards non-independence of modular additions in searching differential trails of ARX ciphers: new automatic methods with application to SPECK and Chaskey

ARX-based ciphers, constructed by the modular addition, rotation and XOR operations, have been receiving a lot of attention in the design of lightweight symmetric ciphers. For their differential cryptanalysis, most automatic search methods of differential trails adopt the assumption of independence of modulo additions. However, this assumption does not necessarily hold when the trail includes consecutive modular additions (CMAs). It has already been found that in this case some differential trails searched by automatic methods before are actually impossible, but the study is not in depth yet, for example, few effort has been paid to exploiting the root causes of non-independence between CMAs and accurate calculation of probabilities of the valid trails. In this paper, we devote to solving these two problems. By examing the differential equations of single and consecutive modular additions, we find that the influence of non-independence can be described by relationships between constraints on the intermediate state of two additions. Specifically, constraints of the first addition can make some of its output bits non-uniform, and when they meet the constraints of the second addition, the differential probability of the whole CMA may be different from the value calculated under the independence assumption. As a result, we can build SAT models to verify the validity of a given differential trail of ARX ciphers and #SAT models to calculate the exact probabilities of the differential propagation through CMAs in the trail, promising a more accurate evaluation of probability of the trail. Our automic methods and searching tools are applied to search related-key differential trails of SPECK and Chaskey including CMAs in the key schedule and the round function respectively.