分组密码攻击模型的构建和自动化密码分析

发布时间：2020-03-26 06:33

【摘要】：随着物联网时代向万物互联时代的不断推动,互联网为生活方方面面带来便利的同时,网络安全问题也在新形势下面临新的挑战。作为保障网络安全的基石,密码在安全认证、加密保护和信息传递等方面发挥了十分重要的作用。与公钥密码体制相比,对称密码算法由于效率高、算法简单、适合加密大量数据的优点应用更为广泛。基于这一事实,对分组密码算法分析与设计的研究在新环境下显得尤为重要。本文围绕分组密码攻击模型的构建和自动化密码分析这一主题展开。首先,在攻击模型构建方面,我们提出了卡方多重/多维零相关线性分析模型,并将该模型用于一系列算法的多重和多维零相关分析中。其次,针对自动化密码分析,我们一方面着眼于攻击路线的自动化搜索问题,另一方面试图借助自动化思想解决密码学中的理论问题。在路线自动化搜索方面,我们给出了基于MILP方法对具有复杂线性层的算法和ARX类算法搜索比特级分离特性的模型,使用新方法对一系列算法关于积分分析的抵抗性进行了评估。构建了基于SAT方法ARX类算法比特级分离特性的自动化搜索工具和基于SMT方法自动化搜索字级分离特性的新工具,完善了分离特性自动化搜索框架。在自动化解决理论问题方面,讨论了差分分析中的差分聚集现象,对两个算法给出了更加精确的差分分析。最后,我们对SIMON算法的所有版本给出了零相关攻击结果。具体结果如下。给出了基于SAT方法自动化搜索并分析带S盒算法差分闭包的工具:为了填补SAT方法在搜索差分闭包方面的空白,我们给出了基于SAT问题的差分闭包自动化搜索工具。首先,我们给出对线性层和由多个小S盒构成的非线性层的刻画。随后,给出了目标函数的SAT模型,这使得我们可以实现在固定权重下差分特征的搜索。最后,给出了搜索差分闭包中多条路线的方法。这一自动化搜索方法在对LED64算法和Midori64算法的分析中发挥了十分重要的作用。对于LED64算法,我们提出了一种自动化搜索差分闭包正确对的方法。首先,我们导出满足差分路线正确对的约束条件,而后,将这些约束条件转化为SAT问题,保证SAT问题的解与路线的所有正确对一一对应。然后,使用求解器的多解搜索模式,搜索服从差分路线的所有正确对。基于这一方法,我们改进了 Mendel等人[86]给出的迭代和非迭代差分闭包概率的结果。基于这些针对差分闭包改进的结果,已有的对于LED64算法缩短轮的攻击都得到了不同程度的改进。对于Midori64算法,我们构建了一种自动化评估差分闭包弱密钥空间的模型。首先,我们导出一个密钥作为弱密钥所满足的必要条件,而后针对这些条件构建SAT模型,并调用求解器求解。基于这一方法,我们给出了 Midori64算法两个4轮差分闭包的实例,对这两个差分闭包,超过78%的密钥将使其变为不可能差分,换言之,它们的弱密钥比例非常低。如果该路线用于差分攻击,那么很可能错误的将正确密钥当作错误密钥,这就使得差分分析理论结果与实际情况产生偏差。与这一现象相对应,我们考虑差分闭包确定的那些“极弱的”密钥,在这些密钥下,差分攻击的成功率将大于理论结果。该问题与讨论差分闭包中同时成立的路线数量相关,我们发现这类问题可以转化为一类特殊的Max-PoSSo问题。对此,我们构建SAT模型以确定差分闭包中可兼容路线的最大数量。最后,我们给出了 Midori64算法一条差分闭包的实例,对于2-12的密钥,差分闭包的概率由期望值2-23.79提升到2-16。这一现象表明,在这些“极弱”密钥下,差分攻击将更有可能成功,或者说,我们可以以更低的代价实现差分攻击。这些例子提醒我们,对于密钥生成算法简单的轻量级算法,在进行差分分析时,需要格外注意区分器本身的有效性。构建卡方多重/多维零相关线性分析新模型,用该模型给出了TEA算法单密钥情境下的最优攻击:作为更加成熟的密码分析方法,多重和多维零相关线性分析克服了经典零相关攻击在数据复杂度方面的缺陷,使得零相关分析方法被广泛应用于系列对称密码攻击的同时,成为了很多算法的最优攻击方法。虽然多重和多维零相关模型在对众多密码算法的分析中显示出了优越性,但这两个模型对于零相关路线数量的限制条件仍然存在。为了消除这一约束条件,我们构建了卡方多重/多维零相关线性分析模型。由于在模型构建过程中取消了卡方分布的正态逼近过程,新模型在复杂度评估方面达到更高精度的同时,有效性不再依赖路线数量的假设。卡方模型的提出在零相关分析领域具有十分重要的意义:一方面,新模型拓宽了零相关模型的应用范围,具有普适性;另一方面,新的卡方多重模型允许我们在单路线环境下使用低于整个明文空间的数据量对密码算法进行分析,克服了传统零相关分析在这一方面的不足。我们将卡方多维攻击模型应用于CLEFIA-192算法的分析,在对已有攻击复杂度给出更精确评估的同时,使用更少的零相关路线对算法的多维零相关分析结果进行了改进。另外,我们使用新的卡方多重零相关分析模型对TEA算法和XTEA算法关于多重零相关分析的抵抗性重新进行了评估,给出的TEA算法的23轮攻击是该算法在单密钥环境下数据量低于整个明文空间的最好攻击结果。完善了基于MILP方法自动化搜索比特级分离特性的工具:作为传统积分性质的一种推广,分离特性由于能够更确切的刻画传统的ALL特性和BAL-ANCE特性之间的隐含性质,已经成为搜索积分区分器的一种强有力工具。而比特级分离特性由于能对算法的代数性质进行更精准的把控,通常可以导出比传统方法性质更好的区分器,然而直接调用该方法在复杂度方面的缺陷限制了其广泛应用。2016年的亚密会上,Xiang等人提出了基于MILP思想自动化搜索比特级分离特性的方法,这在一定程度上缓解了比特级分离特性对目标算法分组长度的约束,改进了一些以比特置换作为线性层的算法的积分区分器。然而,对那些以复杂线性变换作为扩散层的算法,这一方法的适用性还不得而知。以此为动机,我们首先将原有的复制模型和异或模型分别进行推广,使其适配于具有多输出分支的复制操作和具有多输入分支的异或操作。基于对线性变换本源表示的观测,我们使用两个推广的模型给出了构建复杂线性层MILP模型的一般方法。结合该方法,解决了基于MILP方法比特级分离特性的自动化搜索在具有非比特置换线性层算法上的适用性问题,拓宽了 MILP搜索方法的使用范围,使其在搜索积分区分器方面发挥更大的优势。考虑到ARX类算法在分组密码算法中的重要地位,我们构建了模加运算的MILP模型,使得基于MILP思想的比特级分离特性自动化搜索方法推广到ARX类算法。基于上述推广的模型,我们对一系列算法的积分区分器进行了搜索,对Midori64算法、LED64算法、Joltik-BC算法、Serpent 算法、Noekeon算法、HIGHT算法和LEA等算法的积分区分器给出了不同程度的改进。构建了基于SAT方法ARX类算法比特级分离特性的自动化搜索工具:注意到在ARX类算法差分/线性路线的自动化搜索中,基于SAT/SMT的方法在表现上优于那些基于MILP的方法,我们针对ARX类算法构建了基于SAT问题自动化搜索比特级分离特性的工具。首先,我们对三种基本运算(复制运算、与运算和异或运算)的比特级分离特性建模,将分离特性在运算中的传递规律转化为满足合取范式形式的逻辑表达式。随后,基于这三种基本操作,我们构建了刻画模加运算比特级分离特性的SAT模型。设置好初始分离特性和终止规则后,ARX算法比特级分离特性的搜索问题将转化为SAT问题,进而可调用求解器求解。为了快速定位目标算法的最优积分区分器,我们给出了一种高效的搜索算法,这一算法可以帮助我们缩减初始分离特性的搜索空间,快速定位导出最优积分区分器的初始分离特性的形式。基于这一方法,我们得到了SHACAL-2算法的17轮积分区分器,这使得该算法最优积分区分器轮数改进了 4轮。除此之外,对LEA算法、HIGHT算法和SPECK算法,新获取的积分区分器与用MILP方法得到的结果相比都有不同程度的改进。构建了基于SMT方法自动化搜索字级分离特性的新工具:一方面,考虑到自动化搜索在字级分离特性评估中的空白;另一方面,观察到对大状态/含复杂运算的算法在比特水平追踪分离特性的困难性,我们使用基于SMT的方法实现了字级分离特性的自动化搜索。首先,考虑对字级分离特性在一些基本运算中的传递规律建模,模型的构建采用排除法。而后,合理的设置初始分离特性和终止条件,以将字级分离特性的搜索问题转化为SMT问题,并调用开源求解器对问题进行求解。基于该方法,我们找到了 CLEFIA算法的10轮积分区分器,这些区分器比之前最好的区分器长一轮。对于哈希函数Whirlpool的内层置换,我们改进了 4轮和5轮区分器的数据复杂度。对Rijndael-192和Rijndael-256算法,我们给出了6轮积分区分器,这比之前最好结果多两轮。除此之外,使用新的积分区分器,我们将CLEFIA算法的积分攻击结果改进一轮。
【图文】：

而后，我们将所得的约束条件转化为满足合取范式形式的ＳＡＴ模型。最后，逡逑使用ＳＡＴ求解器的多解功能，求解差分闭包的正确对。逡逑关于正确对的约束条件如图２．２所示，记和Ａｙｉ为第ｉ轮ＳｕｂＣｅｌｌｓ运逡逑算的输入和输出差分，ｆ和Ｖ分别表示第ｉ轮ＳｕｂＣｅｌｌｓ运算的输入值和输出逡逑值，，表示第＊轮使用的轮常数矩阵。逡逑由于步函数中不含有关于密钥的操作，在这里等式（２．５）应调整为逡逑Ｍａｆｊｔ１邋■邋ｘｉ＋１邋＝逦？邋ｙ｛邋？邋ｃｌ＋１）邋＝邋Ｍａｔ＾Ｔ１邋■邋Ｐ邋■邋ｙｌ邋＠邋Ｍａｔ＾ｔ１邋？邋ｃ！＋１邋＝邋Ｖｅｃ＾１，逡逑其中尸＝邋ＭＣ。ＳＲ。因此，给定的差分路线仅对＃的值构成约束。换言之，式逡逑－２７邋－逡逑

中剩余的行向量Ｍｚ（ｉ）均为Ｍ0，邋Ｍｘ，．．．，的线性组合，那么相应的变量逡逑Ｍ／ｊ）ｉ可以表示成变量；ｒ0，化，．．．，的异或。为了更直观的理解这一过程，逡逑请参考图２．４。由于我们使用了主密钥的线性组合，那么ｘａｌｈｌ丨…丨的一个逡逑确定值相当于对整个密钥空间加入了纟个线性约束条件，因此ｚｏｌｌｎｌｌ邋？邋？邋■邋｜｜ｍ逡逑的一个解对应了主密钥ＭＭ…Ｍｍ的１冗丨／２￡种可能的取值。如果我们最终逡逑对变量孙ＩＮ丨丨…丨丨Ａｄ可以得到＆个解，那么一个密钥落入集合／ｃ邋一邋Ｉ］１邋Ｖ；？逡逑ｉ＝Ｑ逡逑的概率应为ｔ／２￡。逡逑弱密钥比例低于５０％的４轮差分闭包我们将上述基于ＳＡＴ问题的搜索技巧逡逑应用于Ｍｉｄｏｒｉ６４的一些４轮差分闭包的分析。下面给出两个例子。对于第一逡逑个差分闭包，其弱密钥比例低于２１．３６％。对于第二个差分闭包，其期望条件概逡逑率在理论上保证了其在差分分析中的有效性，但其弱密钥比例低于３．９４％，这逡逑也说明对于９６．０６％的密钥，该差分闭包将变为不可能差分。这些反例具有非常逡逑重要的意义，因为在进行差分分析时，我们很少考虑区分器本身成立的概率，而逡逑差分闭包的概率关于密钥的分布影响了攻击的有效性。如果一个差分闭包在固逡逑定密钥下差分概率为零的概率非常高，当我们将其用于攻击时，那么很可能错逡逑误的将正确密钥当作错误密钥
【学位授予单位】：山东大学
【学位级别】：博士
【学位授予年份】：2019
【分类号】：TN918.1


本文编号：2601091