ARX密码差分迹搜索中模加法的非独立性：新的自动化方法及其在SPECK和Chaskey中的应用
Towards non-independence of modular additions in searching differential trails of ARX ciphers: new automatic methods with application to SPECK and Chaskey
摘要：
基于ARX的密码算法是由模加、模旋转和模异或运算构成的，在轻量级对称密码算法的设计中受到了广泛的关注。对于差分密码分析，大多数差分路径的自动搜索方法都采用模加法独立的假设。然而，当线索包括连续的模加法（CMA）时，这个假设不一定成立。已经发现，在这种情况下，以前通过自动方法搜索的一些差分踪迹实际上是不可能的，但是研究还不深入，例如，很少努力利用CMA之间的非独立性的根本原因和准确计算有效踪迹的概率。本文致力于解决这两个问题。通过考察单次和连续模加法的微分方程，我们发现非独立性的影响可以用两次加法的中间状态上的约束之间的关系来描述。具体地，第一次加法的约束可以使其输出比特中的一些不均匀，并且当它们满足第二次加法的约束时，整个CMA的差分概率可能不同于在独立性假设下计算的值。因此，我们可以建立SAT模型来验证ARX密码差分路径的有效性，并建立#SAT模型来计算差分路径通过CMA传播的确切概率，从而更准确地评估路径的概率。我们的自动化方法和搜索工具被应用到搜索相关的关键差分轨迹的SPECK和Chaskey包括CMA的关键调度和轮函数分别。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
