Improved MILP modeling for automatic security evaluation and application to fox

Counting the number of differentially active S-boxes is of great importance in evaluating the security of a block cipher against differential attack. Mouha et al. proposed a technique based on Mixed-Integer Linear Programming (MILP) to automatically calculate a lower bound of the number of differentially active S-boxes for word-oriented block ciphers, and applied it to symmetric ciphers AES and Enocoro-128v2. Later Sun et al. extended the method by introducing bit-level representations for Sboxes and new constraints in the MILP problem, and applied the extended method to PRESENT-80 and LBlock. This kind of methods greatly depends on the constraints in the MILP problem describing the differential propagation of the block cipher. A more accurate description of the differential propagation leads to a tighter bound on the number of differentially active S-boxes. In this paper, we refine the constraints in the MILP problem describing XOR operations, and apply the refined MILP modeling to determine a lower bound of the number of active S-boxes for the Lai-Massey type block cipher FOX in the model of single-key differential attack, and obtain a tighter bound in FOX64 than existing results. Experimental results show that 6, instead of currently known 8, rounds of FOX64 is strong enough to resist against basic single-key differential attack since the differential characteristic probability is upper bounded by 2-64, and thus the maximum differential characteristic probability of 12-round FOX64 is upper bounded by 2-128, where 128 is the key-length of FOX64. We also get the lower bound of the number of differentially active S-boxes for 5-round FOX128, and proved the security of the full-round FOX128 with respect to single-key differential attack.