MILP-Based Automatic Search Algorithms For Differential And Linear Trails For ARX Cipher And SMT Model For Additive Differential

With the development of internet, the information security has been more and more important. The cryptography has also been a hot topic. There are two research field in cryptography. One is symmetric cryptography and the other is public key cryptography. The block cipher is an important part of symmetric cryptography. Because of simple structure, the block cipher is widely used in data encryption. The research of block cipher has drawn wide attention.The cryptographers has proposed many method to attack block cipher. The differential attack and linear attack are two most useful method. The most important thing for two method is to find a good differential trail or linear trail. So, how to automatic search the differential and linear trials has drawn wide attention.In recent years, Mixed Integer Linear Programming (MILP) has been successfully applied in searching for differential characteristics and linear ap-proximations in block ciphers and has produced the significant results for some ciphers such as SIMON (a family of lightweight and hardware-optimized block ciphers designed by NSA) etc. However, in the literature, the MILP-based automatic search algorithm for differential characteristics and linear approxi-mations is still infeasible for block ciphers such as ARX constructions.In this paper, we propose an MILP-based method for automatic search for differential characteristics and linear approximations in ARX ciphers. By researching the properties of differential characteristic and linear approxima-tion of modular addition in ARX ciphers, we present a method to describe the differential characteristic and linear approximation with linear inequali-ties under the assumptions of independent inputs to the modular addition and independent rounds. We use this representation as an input to the pub-licly available MILP optimizer Gurobi to search for differential characteristics and linear approximations for ARX ciphers. As an illustration, we apply our method to Speck, a family of lightweight and software-optimized block ciphers designed by NSA, which results in the improved differential characteristics and linear approximations compared with the existing ones. Moreover, we provide the improved differential attacks on Speck48, Speck64, Speck96 and Speck 128, which are the best attacks on them in terms of the number of rounds.In addition, Satisfiability Modulo Theories(SMT) is also interest the cryp-tographers. SMT can also be used to search the differential trails for ARX ciphers. In this paper, we also talk about how to construct the SMT model to search the additive differential trails for ARX ciphers and give a new method to achieve our goal.