Mixed-Integer Linear Programming in the Analysis of Trivium and Ktantan
In this paper, the authors present a rather new approach to apply mixed-integer optimization to the cryptanalysis of cryptographic primitives. They focus on the stream cipher Trivium, that has been recommended by the eSTREAM stream cipher project, and the lightweight block cipher Ktantan. Using these examples they explain how the problem of solving a non-linear multivariate Boolean equation system can be formulated as a mixed-integer linear programming problem. Their main focus is the formulation of the mixed-integer programming model (MIP model), which includes amongst others the choice of a conversion method to convert the Boolean equations into equations over the reals, different guessing strategies and the selection of binary variables. They apply the commercial solver Cplex to their problems.