Minimizing Deduction System and its Application

TL;DR

This paper introduces a MILP-based method for solving minimizing deduction systems, enabling efficient analysis of cryptographic security and significantly reducing problem scale through proposed improvements.

Contribution

It proposes a novel MILP-based approach for minimizing deduction systems, including new concepts and optimization techniques for cryptographic analysis.

Findings

SNOW 2.0 security analysis completed in under 0.1s on a personal laptop.

Enocoro-128v2 analysis achieved within 3 minutes for 18 variables.

Proposed improvements significantly reduce MILP problem size.

Abstract

In a deduction system with some propositions and some known relations among these propositions, people usually care about the minimum of propositions by which all other propositions can be deduced according to these known relations. Here we call it a minimizing deduction system. Its common solution is the guess and determine method. In this paper we propose a method of solving the minimizing deduction system based on MILP. Firstly, we introduce the conceptions of state variable, path variable and state copy, which enable us to characterize all rules by inequalities. Then we reduce the deduction problem to a MILP problem and solve it by the Gurobi optimizer. As its applications, we analyze the security of two stream ciphers SNOW2.0 and Enocoro-128v2 in resistance to guess and determine attacks. For SNOW 2.0, it is surprising that it takes less than 0.1s to get the best solution of 9 known variables in a personal Macbook Air(Early 2015, Double Intel Core i5 1.6GHZ, 4GB DDR3). For Enocoro-128v2, we get the best solution of 18 known variables within 3 minutes. What's more, we propose two improvements to reduce the number of variables and inequalities which significantly decrease the scale of the MILP problem.