基于混合整数线性规划模型的...GENT_S盒紧凑约束分析_石一鹏.pdf

2023-05-10计算机应用,Journal of Computer Applications2023,43(5):1504-1510ISSN 1001-9081CODEN JYIIDUhttp：/基于混合整数线性规划模型的SPONGENT S盒紧凑约束分析石一鹏1，刘杰1*，祖锦源1，张涛1，张国群2（1.西北工业大学 软件学院，西安 710129；2.上海机电工程研究所，上海 201109）（通信作者电子邮箱lucky_）摘要：应用基于混合整数线性规划（MILP）模型的S盒紧凑约束计算方法，可以较好地解决SPONGENT在差分密码分析过程中差分路径搜索效率低下的问题；为寻找S盒的最优描述，提出一种紧凑性验证算法从约束条件存在必要性的角度验证S盒的不等式约束的紧凑性问题。首先，引入MILP模型分析SPONGENT S盒的不等式约束，得到了由23个不等式组成的约束；然后，提出一种用于评价约束不等式存在必要性的指标，并基于该指标提出了一种验证约束不等式组紧凑程度的紧凑性验证算法；最后，使用所提算法验证所求得的SPONGENT S盒约束的紧凑性。计算分析表明，23个不等式都具有唯一可以排除的不可能差分模式，即每个不等式都有存在的必要性；同时，对于同一案例，与利用贪心算法原理筛选的不等式相比，数量减少了20%。因此，所得到的SPONGENT的S盒不等式约束是紧凑的，且所提紧凑性验证算法的效果要优于对比的贪心算法。关键词：差分密码分析；混合整数线性规划；代换置换网络；SPONGENT；S盒中图分类号：TP309.7 文献标志码：ACompact constraint analysis of SPONGENT S-box based on mixed integer linear programming modelSHI Yipeng1，LIU Jie1*，ZU Jinyuan1，ZHANG Tao1，ZHANG Guoqun2（1.School of Software，Northwestern Polytechnical University，Xian Shaanxi 710129，China；2.Shanghai Institute of Mechanical and Electrical Engineering，Shanghai 201109，China）Abstract:Applying the compact constraint calculation method of S-box based on Mixed Integer Linear Programming（MILP）model can solve the low efficiency of differential path search of SPONGENT in differential cryptanalysis.To find the best description of S box，a compactness verification algorithm was proposed to verify the inequality constraints in S-box from the perspective of the necessity of the existence of constraints.Firstly，the MILP model was introduced to analyze the inequality constraints of SPONGENT S-box，and the constraint composed of 23 inequalities was obtained.Then，an index for evaluating the existence necessity of constraint inequality was proposed，and a compactness verification algorithm for verifying the compactness of group of constraint inequalities was proposed based on this index.Finally，the compactness of the obtained SPONGENT S-box constraint was verified by using the proposed algorithm.Calculation analysis show that the 23 inequalities have a unique impossible difference mode that can be excluded，that is，each inequality has the necessity of existence.Furthermore，for the same case，the number of inequalities was reduced by 20%compared to that screened by using the greedy algorithm principle.Therefore，the obtained inequality constraint of S-box in SPONGENT is compact，and the proposed compactness verification algorithm outperforms the greedy algorithm.Key words:differential cryptanalysis;Mixed Integer Linear Programming(MILP);Substitution-Permutation Network(SPN);SPONGENT;S-box0 引言 SPONGENT1-2是一种基于海绵结构的轻量级哈希函数，它的作用是针对可变长度有限位的输入，通过吸收、压缩等步骤输出一个固定位数的哈希值。在SPONGENT中，使用了类 似 PRESENT3的 基 于 代 换 置 换 网 络（Substitution-Permutation Network，SPN）结构的轮函数，该轮函数的输入是经过有限步简单处理的原始输入信息，输出是最终生成的哈希值。因此，轮函数是SPONGENT中生成哈希值的关键结构，对SPONGENT的差分密码分析，最重要的就是针对轮函数分析差分密码。差分密码分析是针对现代分组密码最有效、最著名的攻击方法之一，目前已经应用到很多密码的攻击中，因此抵抗文章编号：1001-9081（2023）05-1504-07DOI：10.11772/j.issn.1001-9081.2022040496收稿日期：2022-04-13；修回日期：2022-05-26；录用日期：2022-06-06。基金项目：上海航天科技创新基金资助项目（SAST2021-054）；太仓市基础研究计划面上项目（TC2021JC32）；中央高校基本科研业务费专项资金资助项目（D5000210638）。作者简介：石一鹏（2001），男，山西朔州人，主要研究方向：密码学、软件工程；刘杰（1985），男，河南南阳人，副教授，博士，CCF会员，主要研究方向：密码学、网络安全；祖锦源（2001），男，安徽合肥人，主要研究方向：密码学、信息安全；张涛（1976），男，陕西扶风人，副教授，博士，主要研究方向：智能机器人、人工智能、强化学习、软件测试；张国群（1978），男，江苏高邮人，高级工程师，硕士，主要研究方向：软件测试、软件工程化。第 5 期石一鹏等：基于混合整数线性规划模型的SPONGENT S盒紧凑约束分析差分攻击的能力也逐渐成为评估加密算法安全性能的基本要求。Ankele 等4针对 Sparx-64/128 分析了 15 和 16 轮的差分特征；ElSheikh 等5针对 CRAFT 算法分析了差分密码；Ji等6针对 GIFT-64 和 GIFT-128 展开了密钥相关的差分路径搜索；杨继林等7针对类 CLEFIA 动态密码结构分析了差分特征。同时，很多基于差分密码分析的新的密码分析方法也逐渐诞生，并广泛应用于多种密码算法的安全性分析中，如Wei 等8对 TWINE 算 法 展 开 了 不 可 能 差 分 密 码 分 析；Moghaddam 等9对 Midori、SKINNY 和 CRAFT 算法展开了截断差分分析；Hutahaean等10对小型PRESENT算法展开了飞去来器分析（boomerang attack）；陈少真等11对GOST2算法展开了密钥相关攻击等。差分密码分析的基本思想是通过研究密码输入差分和输出差分之间的关系猜测密钥，为了提高攻击成功的概率，需要寻找一条高概率的差分路径；然而密码在经过数轮迭代之后产生的差分可能十分复杂，分析处理时可能面临十分庞大的数据量。Mouha 等12提出将混合整数线性规划（Mixed Integer Linear Programming，MILP）模型应用于差分路径的自动搜索，为寻找高概率的差分路径提供了一种全新的思路，通过这种方法可以有效地找到活动 S盒数量的下限。但最初提出的模型忽略了S盒自身的差分特性，不能够用于面向位进行处理的加密算法，如 PRESENT3、LS-Design（Linear-Sbox-Design）13、GIFT14等。Sun等15使用描述S盒可能和不可能差分模式的方法，将Mouha等12提出的模型扩展到了面向位的密码算法的差分分析中；但是该S盒描述方法不能保证得出描述S盒的最优方式。Sasaki等16在文献 15 的基础上改进了MILP模型，提出了一种新的约简算法，获得了理论上的最优描述，大幅提高了差分路径搜索的效率。此后MILP模型在差分密码分析中有了更多的应用。如，Zhu 等17基于MILP 模 型 对 GIFT-64 展 开 了 12 轮 差 分 特 征 的 研 究；Bagherzadeh 等18基于 MILP 模型对 LEA 和 HIGHT 分析了差分密码；Kumar等19基于 MILP模型对 WARP分析了 18轮和19轮的差分特征。基于以上的分析，针对 SPONGENT 的轮函数应用 MILP模型进行差分路径搜索时，可以较好地解决SPONGENT差分路径搜索效率低下的问题。由此，将SPONGENT差分路径搜索问题转变为针对它的轮函数进行MILP建模的问题；而对于具有典型SPN结构的轮函数，建立MILP模型，最重要的步骤就是寻找S盒的最优描述。所谓“最优”，就是在不违背S盒所规定差分模式的条件下最大限度地减少冗余不等式的数量，即寻找一种“紧凑约束”。本文基于约简算法16分析了SPONGENT的S盒的紧凑约束。此外，无法忽略一个事实即使约简算法16在应用过程中展现了很好的实际效果，但是目前仍没有一种严谨的方法证明所得到约束结果的紧凑性。因此，本文提出了一种可能的方法，从约束条件存在必要性的角度验证所得到约束的紧凑性。本文的主要工作为：1）使用不等式对 SPONGENT 中 S 盒所有差分模式的最小凸集描述，得到287个不等式，应用约简算法16在287个不等式中筛选，首次得到了一组由23个不等式组成的约束。2）提出了一种评价约束条件必要程度的指标，并给出了基于该指标的约束紧凑性验证算法，用于对所得到的不等式约束验证紧凑性。针对所得到的 SPONGENT S 盒的约束应用该算法，结果表明，所得到的约束中，每一个不等式都是不可替代的，即23个不等式组成的约束对于SPONGENT的S盒是紧凑的。1 SPONGENT 1.1SPONGENT的版本参数SPONGENT是一个基于海绵结构的哈希函数家族，根据不同的散列输出值的位数（size）、capacity和 rate，SPONGENT可以被分为 13个版本，不同的版本对应不同的加密轮数和安全等级。表 1 以 SPONGENT-size/capacity/rate 的参数化形式标识不同的版本，并给出了每一个版本对应的和运算轮数（round）。其中：state 是参与 SPN 结构轮函数运算部分的位数；rate 是 state 中参与异或运算的位数，也是输入信息分块处理的单位；capacity是state中不参与异或运算部分的位数，3个参数满足state=rate+capacity。由表1可知，SPONGENT共有5种长度的散列值输出，由SPONGENT-size 表 示，分 别 为 SPONGENT-88、SPONGENT-128、SPONGENT-160、SPONGENT-224和SPONGENT-256。1.2SONGENT的计算过程对于输入的消息，SPONGENT进行以下3个阶段的操作计算输出：1）初始化阶段：将输入信息的位数扩展成为rate的整数倍，再将它分割为若干个rate位的分块。2）吸收阶段：将初始化阶段得到的若干个分块逐步与state的前rate位异或运算。3）压缩阶段：通过 SPN 结构的轮函数逐步计算得到输出值。1.3SONGENT中的轮函数在SPONGENT所用的轮函数中主要进行以下运算：1）state与轮常数及其反序值进行异或运算，根据state的位数不同，轮常数相应的初值不同。2）state通过 S盒完成字节代换，每一次代换的字节由 4表1SPONGENT版本参数Tab.1SPONGENT version parameters版本名称（SPONGENT-size/capacity/rate）SPONGENT-88/80/8SPONGENT-88/176/88SPONGENT-128/128/8SPONGENT-128/256/128SPONGENT-160/160/16SPONGENT-160/160/80SPONGENT-160/320/160SPONGENT-224/224/16SPONGENT-224/224/112SPONGENT-224/448/224SPONGENT-256/256/16SPONGENT-256/256/128SPONGENT-256/512/256state88264136384176240480240336672272384768round4513570195901202401201703401401953851505第 43 卷计算机应用位组成，使用b表示state的位数，每一轮需要进行b/4个平行运算。表2为S盒规格的16进制表示，x经过代换变为S(x)。3）state进行P盒置换运算，这里的P盒与PRESENT所用P盒的置换规则类似，都是一种宽轨迹策略的运算。第 i位的值被置换到第P（i）位，运算规则为：P(i)=i()b/4 mod b-1，i 0，1，b-2b-1，i=b-1（1）本文重点分析S盒的紧凑约束，对于轮函数的运算过程不作更多讨论。在得到 S盒的紧凑约束之后可以针对轮函数的结构建立更加高效的MILP模型，从而进行更高效的差分密码分析。2 MILP在最优差分路径搜索中的应用 MILP 应用于差分路径搜索之前，已经在很多领域发挥过重要的作用，它的含义可分为“混合整数”以及“线性规划”两部分。“线性规划”即表明这是一种使用变量约束和不等式约束对目标函数优化的数学方法；“混合整数”则强调其中的一些变量被限制为整数值，而其他变量可以是二进制值或连续值。对于最优差分路径的搜索，可以使用相应的变量约束和不等式约束描述可能的差分路径，并将差分路径的概率作为目标函数，该MILP模型的解即对应最优的差分路径。2.1文献 12 分析框架Mouha 等12提出将 MILP 应用到差分路径分析时，给出了针对SPN结构3种常见操作的不等式分析。2.1.1异或操作不等式分析使用Xin1、Xin2表示异或运算的输入差分，Xout表示相应的输出差分，3个参数之间的关系可以表示为：Xin1Xin2=Xout（2）其中表示异或运算。可以发现，当且仅当Xin1与Xin2值都为 0 时，Xout的值为 0，否则 3 个参数之间至少有两个值不为0。使用一个虚拟变量d 0，1辅助表示这种关系：Xin1+Xin2+Xout 2d；Xin1，Xin2，Xout d（3）2.1.2线性操作不等式分析使用xLin、xLout分别表示线性运算的输入和输出的差分向量。设l为xLin与xLout中的分量个数，则|xLin=xLinlxLin2xLin1xLout=xLoutlxLout2xLout1（4）使用w(x)表示一个向量x的汉明重量，差分分支数BD满足以下公式：BD=minxLin 0w(xLin)+w(xLout)（5）由于线性操作不会改变差分的数值，只会使差分扩散，因此xLin与xLout的汉明重量相等，当有BD个差分分支时，xLin与xLout的 汉 明 重 量 之 和 至 少 为BD。使 用 一 个 虚 拟 变 量dL0，1辅助表示这种关系：j=1l()xLin j+xLout j BDdL；xLin j，xLout j dL（6）2.1.3S盒操作不等式分析使用xSin、xSout分别表示一个规格为 的S盒的输入和输出差分向量，BS表示它们的差分分支数。则|xSin=xSinxSin2xSin1xSout=xSoutxSout2xSout1（7）BS=minxSin 0w(xSin)+w(xSout)（8）对于双射的S盒，当且仅当输入差分为0时，输出差分也为0。即满足以下公式：|j=1xSout j-j=1xSin j 0 j=1xSin j-j=1xSout j 0（9）当有BS个差分分支时，xSin j与xSout j的汉明重量之和至少为BS。使用一个虚拟变量dS0，1辅助表示这种关系：j=1xSin j+j=1xSout j BSdS；xSin j，xSout j dS（10）2.2收紧MILP可行域的方法利用文献 12 的方法针对SPN加密结构建立MILP模型之后，就可以针对不等式约束求解，最优的差分路径就是不等式解空间中的一个解。然而，针对面向位的密码算法，在庞大的解空间中寻找最优的差分路径并不比应用MILP之前更容易；并且，在这个解空间中很多差分路径是不可能出现的。因此需要寻找到一种收紧MILP可行域的方法，尽可能多地剔除不可能出现的差分路径，以缩小最优差分路径的搜索范围。通过添加不等式约束条件排除不可能的差分模式，就可以有效排除很多不可能差分路径，这样的不等式约束被称为截断不等式。Sun等15提出了两种生成截断不等式的方法：针对统计规律逻辑建模，以及差分模式最小凸集的 H-表示。由于受到统计规律的限制，针对统计规律逻辑建模的方式并不适用于大多数加密结构，因此以下主要介绍差分模式最小凸集的H-表示。定义1 将S盒所有可能的差分模式描述为一个离散点集，这个点集的最小凸集可以表示为若干不等式的公共解，那么称这一组不等式为 S盒所有可能差分模式最小凸集的H-表示。例如，S盒的输入差分为x=1001时，可能的输出差分为y=1001或y=1100，输入差分为x=1011时，可能的输出差分为y=1011或y=1110。使用（x3，x2，x1，x0，y3，y2，y1，y0）表示一个差分模式，那么所有可能的差分模式组成的点集为 （1，0，0，1，1，0，0，1），（1，0，0，1，1，1，0，0），（1，0，1，1，1，0，1，1），表2S盒规格的16进制表示Tab.2Hexadecimal representation of S-box specificationx01234567S(x)EDB0214Fx89ABCDEFS(x)7A859C361506第 5 期石一鹏等：基于混合整数线性规划模型的SPONGENT S盒紧凑约束分析（1，0，1，1，1，1，1，0），最小凸集的H-表示为：|-y0+1 0y0 0-y1+1 0y1 0S盒所有可能差分模式最小凸集的 H-表示中含有大量有效的截断不等式。2.3获取紧凑约束的方法随着可能差分模式的增多，最小凸集 H-表示的不等式会越来越多，例如 PRESENT 中 S 盒所有可能差分模式最小凸集的H-表示为327个不等式。这样庞大的不等式组合极其冗杂，导致MILP在有限时间内难以完成求解。然而，由于不可能的差分模式是有限的，排除所有不可能的差分模式并不需要如此多的不等式，只需要选择可以排除所有不可能差分模式的截断不等式组合就可以达到收紧可行域的目的。因此可以在不影响原有约束有效性的同时尽可能地减少不等式的数量，以便不等式求解，即所谓得到紧凑约束的过程。为了尽可能地减少不等式数量，Sun等15利用贪心算法的思想筛选不等式：依次选择可以排除更多不可能差分模式的不等式，直到所有的不可能差分都被所选择的截断不等式排除。使用该贪心算法可以得到一个较优解，但无法保证所得到的不等式数量是最少的；并且对于可以排除相等数量不可能差分模式的截断不等式，并没有明确给出选择的优先级。基于这种情况，Sasaki等16提出了一种新的约简算法，应用MILP选择最优不等式组合，它的基本步骤为：首先计算每个不可能的差分模式可以被哪些不等式排除，得到一个关于不可能差分模式和截断不等式之间的指导二维表，如表 3 所示，单元值为1表示它对应的不可能差分模式可以被对应的截断不等式排除；然后设定约束条件为每一个不可能差分模式至少被一个不等式所排除，同时设定每一个不等式最多可以选择一次；最后设定目标函数为最少的不等式数量，进行MILP求解。3 SPONGENT S盒的约束分析 为了寻找S盒的紧凑约束，本章使用Sasaki等16提出的约简算法展开具体分析，主要步骤包括：计算所有可能的差分模式、求解截断不等式和缩减不等式数量。3.1计算所有可能的差分模式求解 SPONGENT 中 S 盒所有可能的差分模式，得到输入输出差分表，如表4所示。例如，输入差分x=0001时，可能的差分输出有：y=0011，y=0101，y=1011，y=1101，则可能的差分模式包括（0，0，0，1，0，0，1，1），（0，0，0，1，0，1，0，1），（0，0，0，1，1，0，1，1），（0，0，0，1，1，1，0，1）。3.2求解截断不等式根据表4可以得到97个可能的差分模式，对应97个点，使用 SageMath中的函数 inequality_generator（）计算得到它的凸集的H-表示，共含有287个不等式：|-x3+1 0-x2+1 0-x1+1 0-x0+1 0-y3+1 0-x2-x1-x0-y3-y2-y0+5 0-3x3+x2-2x1-3x0-3y3-2y2+y1-y0+11 0-x3-2x2-x1-2x0-y3+y2-2y1-y0+8 0对所有的不等式按照顺序从0开始编号，以便下一步计算，最 后 一 个 不 等 式 的 编 号 为 286。使 用 变 量Ij 0，1(j 0，1，286)表示每一个不等式。3.3缩减不等式数量计算所有不可能的差分模式，共有256-97=159个，并对所有的不可能差分模式从0开始编号，最后一个不可能差分模式编号为158。然后应用约简算法16，得到了类似表3的159287的二维表，如可以排除第20个不可能差分模式（1，1，1，0，1，0，0，0）的不等式有I23，I28，I41，I193，I223和I242：|I23：-x3-x2-x1+x0-y2-y1+2 0I28：-x3-x2-x1+x0+2y3+3y2+3y1+2y0 0I41：-2x3-x2-x1+2x0-y3+2y2+2y1-y0+4 0I193：-x2-x1+x0+y3+2y2+2y1+2y0 0I223：-x2-x+x0+y2+y1+y0+1 0I242：x3-x2-x1+x0+2y2+2y1+2y0 0令Ij=1表示选择保留这个不等式，Ij=0表示不保留该不等式，则由第20个不可能差分模式可以得到约束条件为：I23+I28+I41+I193+I223+I242 1表3指导二维表样例Tab.3Example of 2D guidance table不可能差分模式I1I2I3IM不等式Q11101Q20100Q31001QN0110表4输入输出差分表Tab.4Input-output difference table输入差分0000000100100011010001010110011110001001101010111100110111101111输出差分00000011，0101，1011，11010101，0110，1010，1101，1110，11110010，0101，0110，1101，1110，11110011，0110，1011，1100，1110，11110011，0100，0110，1011，1110，11110001，0010，0100，1001，1010，11000001，0010，0100，1001，1010，11000011，0101，0111，1001，1011，11010010，0100，1000，1010，1100，11100001，0011，0110，0111，1000，1010，1100，11010001，0010，0100，0101，0110，0111，1000，10110001，0101，0110，0111，1000，1010，1011，11000001，0010，0011，0100，0110，0111，1000，11010010，0011，0100，0101，1010，1011，1100，11010111，1000，1001，11101507第 43 卷计算机应用对全部不可能差分模式进行以上步骤，可以得到关于Ij的159个不等式约束，求解得min()j=0286Ij=23。对应值为1的不等式为：|I9：-3x3-x2+x1+x0-3y3-3y2-2y1-y0+10 0I12：-x2-x1+x0-y2-y1+3 0I18：-3x3+x2-x1+x0-3y3-2y2-3y1-y0+10 0I21：-x3+x1-x0-y3+y2-y0+3 0I41：-2x3-x2-x1+2x0-y3+2y2+2y1-y0+4 0I48：2x3-2x2+x1+2y2+y1+y0 0I70：x3+x2-2x1-x0+y3+y2-y1-2y0+4 0I83：2x3+x2-2x1+y2+2y1+y0 0I89：x3+2x2+2x1-2x0+y3-3y2-3y1-y0+6 0I97：3x3+x2+x1-2x0-y3+y2+y1+2y0 0I101：-x2+x1-x0-y3-y2+y1+y0+3 0I116：-x3-x2+x1+x0+y3+y2-y1+2 0I132：-x3+3x2+3x1-x0+2y3+2y2+2y1-y0 0I155：x3-2x2+x1-x0+y3-y2+y1-2y0+4 0I180：2x3-2x2-2x1-y2-y1-y0+5 0I182：3x3+2x2-x1+2x0+2y3+2y2-y1-y0 0I194：3x3+6x2+6x1+3x0-2y3-2y2-2y1+y0 0I211：2x3-x2+x1+x0+y3-y2+y1-y0+1 0I224：-x3+x2-x1+x0+y3-y2+y1+2 0I240：-2x3-2x2-2x1-2x0+3y3+y2+y1+y0+5 0I250：-3x3+x2+x1+2x0+2y3+y2+y1+2y0 0I270：-2x3-x2-x1-2x0-y3+2y2-2y1+y0+7 0I285：-3x3+x2-2x1-3x0-3y3-2y2+y1-y0+11 0上述不等式组即为所求S盒的约束。4 紧凑性验证 4.1紧凑性验证算法4.1.1约束不等式集合的紧凑性在S盒所有可能差分模式最小凸集的H-表示中，每一个截断不等式可以排除的不可能差分模式会有重合的部分，如表3中，不等式1和3都能排除不可能差分模式1，不等式1、2和N都能排除不可能差分模式2。这种重合的情况在最终所求得的不等式约束集合中同样存在，而这恰恰是发现不等式约束集合可能存在冗余的一个重要突破口。为了更好地表示这种冗余的情况，本文使用一个具体的案例说明。如表5所示，使用Qi表示待选择的截断不等式，使用Ij表示需要被排除的不可能差分模式，当单元格值为1时，表示它对应的不可能差分模式可以被对应的截断不等式排除，表5中Q1到Q8所能排除的不等式数量为降序排列。针对表5中的数据应用贪心算法15筛选不等式，依次选取可以排除不可能差分模式最多的截断不等式，直到所有的不可能差分模式都被排除，得到的筛选结果为Q1、Q2、Q3、Q4、Q5。不难发现，Q1排除的不可能差分模式都可以被Q2、Q3、Q4、Q5组成的其他不等式组排除，不等式Q1对整个不等式约束集合就是冗余的。删去Q1对于不等式约束集合排除不可能差分模式的能力没有任何影响，但是却可以减轻运算的负担，提高差分路径搜索的效率。使用 MILP 模型进行 S 盒约束不等式求解的目标，是希望使用尽可能少的不等式描述S盒所容许的差分模式，并且排除所有不可能的差分模式。由于求解关注的重点之一是不等式的数量，因此一切可能导致不等式约束集合存在冗余的情况都应当被排除，这对于差分路径搜索复杂度的提升具有重要的意义。无论使用哪一种算法求解不等式约束集合，都应当保证最终的求解结果自身是紧凑的。为此，需要针对不等式约束集合验证紧凑性。遗憾的是，目前尚未有一种方法能够针对不等式约束集合的紧凑性验证，为此，本文提出一种可行的方法。4.1.2紧凑性验证算法为了验证不等式约束集合的紧凑性，本文首先定义了一个评价约束条件必要程度的指标“必要度”，使用参数Necessity 0，1，表示，定义如下：定义2 对于一个约束条件，在整个约束条件集合中由该条件唯一排除的不可能差分模式的数量定义为该约束条件的必要度。当一个不等式的必要度为0时，表示该不等式对于约束组合是非必要存在的。此时，原不等式约束集合就是不紧凑的，一个紧凑的不等式约束集合至少不能包含该不等式。基于约束不等式的必要度，本文提出了一种验证约束条件集合紧凑性的算法，如算法1所示。算法1 验证约束条件集合紧凑性的算法。输入 不等式约束集合H，不可能差分模式集合Q，不等式约束的必要度散列表NH，每一个不可能差分模式对应的截断不等式散列表DQ；输出 约束条件的紧凑性Cmpt True，False。1）Initialize（NH）；/*初始化，每一个不等式的必要度初值为0*/2）Initialize（DQ）；/*初始化，每个不可能差分模式对应一个空集*/3）Cmpt=True；/*初始化*/4）for（i 0 to|Q）do；5）for（j 0 to|H）do；6）if H j can exclude Qi do；7）add H j in DQQi；8）end for9）end for10）for（i 0 to|Q）do；11）if|DQQi=1 do；表5冗余不等式约束案例Tab.5Case of redundant inequality constraints不可能差分模式I1I2I3I4I5I6I7I8I9I10I11不等式Q111011001010Q201110010010Q310001001110Q410100100100Q501100000001Q610000100100Q700000001001Q8000000110001508第 5 期石一鹏等：基于混合整数线性规划模型的SPONGENT S盒紧凑约束分析12）NH DQQi0+=1；13）end for14）for（j 0 to|H）do；15）if NH H j=0 do；16）Cmpt=False；17）end for4.1.3算法的正确性及应用算法 1是基于“必要度”的概念设计的。对于一个不等式约束集合，算法 1能够计算每一个不等式的必要度，当不等式约束集合中存在必要度为0的不等式时，则判定该不等式约束集合是不紧凑的；反之，若所有不等式的必要度都不为0，则判定该不等式约束集合是紧凑的。由于“必要度”代表一个不等式能够唯一排除的不可能差分模式的数量，当不等式约束集合中存在必要度为0的不等式时，表明该不等式所排除的每一个不可能差分模式都能被其他不等式所排除，去除这个不等式对于不等式约束集合整体排除不可能差分模式的能力没有影响，因此当前的不等式约束集合存在冗余不等式，是不紧凑的；同样，若每一个不等式的必要度都非0，则表明每一个不等式都至少有一个不可能差分模式是其他所有的不等式都不能排除的，若去除其中某个不等式，新的不等式约束集合就无法排除对应的不可能差分模式，因此当前不等式约束中的每一个不等式都有存在的必要，当前的不等式约束集合是紧凑的。由此可以证明，算法1能够准确判定一个不等式约束集合的紧凑性。对于表5中所示案例，使用Sun等的贪心算法15得到的约束不等式集合与使用本文算法 1优化得到的约束不等式集合如表6所示。使用贪心算法15得到的约束不等式集合为 Q1，Q2，Q3，Q4，Q5。使用算法1得到其中各个不等式的必要度分别为：0、1、0、1、1。此时可以得知，Q1和Q3对于不等式约束集合而言是冗余的。去除Q1，得到新的不等式约束为Q2、Q3、Q4、Q5，此时各个不等式的必要度分别为 2、2、1、1，即新的不等式约束集合是紧凑的。由此可知，算法1对于鉴别约束不等式集合的紧凑性以及指导约束集合优化具有实际的有效性。值得注意的是，对于一个不等式约束集合而言，其中各个不等式的必要度会相互影响，去除或替换某一个不等式，其他不等式的必要度很可能也会发生变化。如表6所示，去除Q1之后，Q3的必要度由 0变化为 2，这启示研究者在不等式集合中发现多个必要度为0的不等式时，不可以直接将它们全部去除，而是应该每去除一个不等式重新评估一次必要度，采用回溯的方式找到去除不等式最多的方案。表6的案例说明，算法1对于约束不等式可能存在的冗余情况具有很好的鉴别作用，对于不等式约束的改进和优化也具有很好的指导意义。对于应用 Sun等15提出的贪心算法进行差分分析相关研究遇到的问题18，或许可以使用算法 1 解决；而对于 Sasaki 等16改进之后的约简算法而言，使用算法1可以验证其所得到结果的正确性。由于Sasaki等16的约简算法是基于线性规划的，并且以不等式数量的最小值作为规划目标，其所得的不等式约束集合中每一个不等式的必要度一定不为 0。假设存在一个必要度为 0的不等式，它一定会在线性规划过程中因为“不等式数量最小化”这个优化目标而被排除，否则可以判定算法的实现过程出现了错误。综上，算法1对于Sun等15提出的贪心算法具有很好的优化效果，当出现必要度为0的不等式时，可以根据算法1指导不等式约束集合的优化；对于Sasaki等16改进之后的约简算法则具有很好的检验作用，当出现必要度为 0 的不等式时，证明算法的实现过程存在错误，从而及时矫正。4.1.4算法的时间复杂度对于拥有m个不等式、n个不可能差分模式的不等式约束，使用验证算法紧凑性验证，首先需要计算每一个不等式的必要度，这一过程的时间复杂度为O（mn）；之后需要检查是否存在必要度为0的不等式，这一过程的最坏时间复杂度为O（m）。综上，本文验证算法的时间复杂度为O（mn）。4.2约束紧凑性验证4.1节中说明，使用 Sasaki等16改进之后的约简算法得到的约束不等式集合应当是紧凑的，若得到的不等式集合不是紧凑的，则说明算法实现过程中出现了错误。因此针对3.3节中得到的约束应用算法 1，得到每一个不等式约束的必要度如表 7所示。由表 7可知，3.3节中所得的每一个不等式约束必要度都不为0，即每一个不等式都有存在的必要性，算法实现过程是正确的，所得的约束不等式集合是SPONGENT S盒的一个紧凑约束。5 结语 随着 MILP在差分密码分析中的地位日渐升高，寻找建立高效不等式约束的方式也变得更加重要。本文使用MILP模型针对SPONGENT中S盒的紧凑约束展开了分析，得到了