Mixed Integer Linear Programming (MILP) solvers are regularly used by designers for providing security arguments and by cryptanalysts for searching for new distinguishers. For both applications, bitwise models are more refined and permit to analyze properties of primitives more accurately than word-oriented models. Yet, they are much heavier than these last ones. In this talk, we first propose many new algorithms for efficiently modeling any subset of $F_2^n$ with MILP inequalities. This permits, among others, to model differential or linear propagation through Sboxes. We manage notably to represent the differential behaviour of the AES Sbox with three times less inequalities than before. Then, we present two new algorithms inspired from coding theory to model complex linear layers without dummy variables. This permits us to represent many diffusion matrices, notably the ones of Skinny-128 and AES in a much more compact way. Finally, we demonstrate the impact of our new models on the solving time with different experiments.
This is a joint work with Christina Boura.