More Accurate Division Property Propagations Based on Optimized Implementations of Linear Layers.

As a generalized integral property, the division property can be used to search integral distinguishers of symmetric ciphers by taking the advantage of automatic tools, such as Mixed Integer Linear Programming (MILP) and Boolean Satisfiability Problem (SAT) solvers. In this case, the accuracy of corresponding models will influence the resulting distinguishers. In this paper, we present a new technique to characterize the division property propagation of linear layers. Firstly, we study the impact of a linear layer implementation on its division property propagations. We found that division trails derived from an optimized implementation of a linear layer can be more accurate than the S method, and different implementations can eliminate some different invalid division trails. Thus, we can eliminate a large number of invalid division trails by combining different implementations. As an application of our technique, we have searched distinguishers for Midori64, Skinny64 and LED. As a result, we can obtain the same longest distinguishers as the ZR method and the HW method, which are the exact modeling of linear layers. Moreover, our method can be used with both MILP and SAT, while the HW method can only work with SAT. In addition, the number of constraints with the HW method increases quadratically, however it increases linearly with our method.