论文标题
最小化扣除系统及其应用
Minimizing Deduction System and its Application
论文作者
论文摘要
在这些命题之间具有一些命题和一些已知关系的推论系统中，人们通常关心可以根据这些已知关系推导所有其他命题的命题的最低要求。在这里，我们将其称为最小化扣除系统。它的常见解决方案是猜测和确定方法。在本文中，我们提出了一种解决基于MILP的最小化扣除系统的方法。首先，我们介绍了状态变量，路径变量和状态副本的概念，这使我们能够通过不平等表征所有规则。然后，我们将演绎问题减少到MILP问题，并通过Gurobi优化器解决。作为应用程序，我们分析了两个流密切雪2.0和Enocoro-128v2的安全性，以猜测和确定攻击。对于Snow 2.0，令人惊讶的是，在个人MacBook Air中获得9个已知变量的最佳解决方案所需的时间不足（2015年初，Double Intel Core i5 1.6GHz，4GB DDR3）。对于Enocoro-128V2，我们在3分钟内获得了18个已知变量的最佳解决方案。更重要的是，我们提出了两项改进，以减少变量和不平等的数量，从而大大降低了MILP问题的规模。
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.
