Improved Modeling Methods for Automated Differential Analysis of Block Ciphers: Applications to uBlock-256 and PRESENT

Differential analysis for block ciphers based on automated solving tools such as Mixed-Integer Linear Programming (MILP) and Boolean Satisfiability Problem (SAT) has become one of the key technologies in modern cryptographic research. Currently, existing automated analysis methods face efficiency bottlenecks in solving complex models, which limits their effectiveness in block cipher analysis. To address these challenges, we propose two improved modeling methods for differential analysis of block ciphers, aiming to enhance both solving efficiency and accuracy. Regarding the MILP approach, we introduce the “Choice-Based Constraint” technique to model the propagation of differentials through linear layers. Applying this method to the 4-round differential analysis of uBlock-256, more compact and precise differential security bounds than existing results are obtained for the first time, demonstrating that 4-round uBlock-256 has at least 34 active differential S-boxes. For the SAT approach, we propose the "Weighted Encoding" method, which reduces the number of variables and constraints in the model, thereby significantly improving solving efficiency. This method was employed in the optimal differential characteristic search process for 2 to 28 rounds of the PRESENT. Compared to existing “sequential encoding” methods, the solving time was reduced by an average of 40%. The results have demonstrated the effectiveness and practicality of the proposed improved modeling methods in automated differential analysis of block ciphers.