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

1、精选优质文档-倾情为你奉上分组密码攻击模型的构建和自动化密码分析随着物联网时代向万物互联时代的不断推动,互联网为生活方方面面带来便利的同时,网络安全问题也在新形势下面临新的挑战。作为保障网络安全的基石,密码在安全认证、加密保护和信息传递等方面发挥了十分重要的作用。与公钥密码体制相比,对称密码算法由于效率高、算法简单、适合加密大量数据的优点应用更为广泛。基于这一事实,对分组密码算法分析与设计的研究在新环境下显得尤为重要。本文围绕分组密码攻击模型的构建和自动化密码分析这一主题展开。首先,在攻击模型构建方面,我们提出了卡方多重/多维零相关线性分析模型,并将该模型用于一系列算法的多重和多维零相关分析中

2、。其次,针对自动化密码分析,我们一方面着眼于攻击路线的自动化搜索问题,另一方面试图借助自动化思想解决密码学中的理论问题。在路线自动化搜索方面,我们给出了基于MILP方法对具有复杂线性层的算法和ARX类算法搜索比特级分离特性的模型,使用新方法对一系列算法关于积分分析的抵抗性进行了评估。构建了基于SAT方法ARX类算法比特级分离特性的自动化搜索工具和基于SMT方法自动化搜索字级分离特性的新工具,完善了分离特性自动化搜索框架。在自动化解决理论问题方面,讨论了差分分析中的差分聚集现象,对两个算法给出了更加精确的差分分析。最后,我们对SIMON算法的所有版本给出了零相关攻击结果。具体结果如下。给出了基于

3、SAT方法自动化搜索并分析带S盒算法差分闭包的工具:为了填补SAT方法在搜索差分闭包方面的空白,我们给出了基于SAT问题的差分闭包自动化搜索工具。首先,我们给出对线性层和由多个小S盒构成的非线性层的刻画。随后,给出了目标函数的SAT模型,这使得我们可以实现在固定权重下差分特征的搜索。最后,给出了搜索差分闭包中多条路线的方法。这一自动化搜索方法在对LED64算法和Midori64算法的分析中发挥了十分重要的作用。对于LED64算法,我们提出了一种自动化搜索差分闭包正确对的方法。首先,我们导出满足差分路线正确对的约束条件,而后,将这些约束条件转化为SAT问题,保证SAT问题的解与路线的所有正确对一

4、一对应。然后,使用求解器的多解搜索模式,搜索服从差分路线的所有正确对。基于这一方法,我们改进了 Mendel等人86给出的迭代和非迭代差分闭包概率的结果。基于这些针对差分闭包改进的结果,已有的对于LED64算法缩短轮的攻击都得到了不同程度的改进。对于Midori64算法,我们构建了一种自动化评估差分闭包弱密钥空间的模型。首先,我们导出一个密钥作为弱密钥所满足的必要条件,而后针对这些条件构建SAT模型,并调用求解器求解。基于这一方法,我们给出了 Midori64算法两个4轮差分闭包的实例,对这两个差分闭包,超过78%的密钥将使其变为不可能差分,换言之,它们的弱密钥比例非常低。如果该路线用于差分攻

5、击,那么很可能错误的将正确密钥当作错误密钥,这就使得差分分析理论结果与实际情况产生偏差。与这一现象相对应,我们考虑差分闭包确定的那些“极弱的”密钥,在这些密钥下,差分攻击的成功率将大于理论结果。该问题与讨论差分闭包中同时成立的路线数量相关,我们发现这类问题可以转化为一类特殊的Max-PoSSo问题。对此,我们构建SAT模型以确定差分闭包中可兼容路线的最大数量。最后,我们给出了 Midori64算法一条差分闭包的实例,对于2-12的密钥,差分闭包的概率由期望值2-23.79提升到2-16。这一现象表明,在这些“极弱”密钥下,差分攻击将更有可能成功,或者说,我们可以以更低的代价实现差分攻击。这些例

6、子提醒我们,对于密钥生成算法简单的轻量级算法,在进行差分分析时,需要格外注意区分器本身的有效性。构建卡方多重/多维零相关线性分析新模型,用该模型给出了TEA算法单密钥情境下的最优攻击:作为更加成熟的密码分析方法,多重和多维零相关线性分析克服了经典零相关攻击在数据复杂度方面的缺陷,使得零相关分析方法被广泛应用于系列对称密码攻击的同时,成为了很多算法的最优攻击方法。虽然多重和多维零相关模型在对众多密码算法的分析中显示出了优越性,但这两个模型对于零相关路线数量的限制条件仍然存在。为了消除这一约束条件,我们构建了卡方多重/多维零相关线性分析模型。由于在模型构建过程中取消了卡方分布的正态逼近过程,新模型

7、在复杂度评估方面达到更高精度的同时,有效性不再依赖路线数量的假设。卡方模型的提出在零相关分析领域具有十分重要的意义:一方面,新模型拓宽了零相关模型的应用范围,具有普适性;另一方面,新的卡方多重模型允许我们在单路线环境下使用低于整个明文空间的数据量对密码算法进行分析,克服了传统零相关分析在这一方面的不足。我们将卡方多维攻击模型应用于CLEFIA-192算法的分析,在对已有攻击复杂度给出更精确评估的同时,使用更少的零相关路线对算法的多维零相关分析结果进行了改进。另外,我们使用新的卡方多重零相关分析模型对TEA算法和XTEA算法关于多重零相关分析的抵抗性重新进行了评估,给出的TEA算法的23轮攻击是

8、该算法在单密钥环境下数据量低于整个明文空间的最好攻击结果。完善了基于MILP方法自动化搜索比特级分离特性的工具:作为传统积分性质的一种推广,分离特性由于能够更确切的刻画传统的ALL特性和BAL-ANCE特性之间的隐含性质,已经成为搜索积分区分器的一种强有力工具。而比特级分离特性由于能对算法的代数性质进行更精准的把控,通常可以导出比传统方法性质更好的区分器,然而直接调用该方法在复杂度方面的缺陷限制了其广泛应用。2016年的亚密会上,Xiang等人提出了基于MILP思想自动化搜索比特级分离特性的方法,这在一定程度上缓解了比特级分离特性对目标算法分组长度的约束,改进了一些以比特置换作为线性层的算法的

9、积分区分器。然而,对那些以复杂线性变换作为扩散层的算法,这一方法的适用性还不得而知。以此为动机,我们首先将原有的复制模型和异或模型分别进行推广,使其适配于具有多输出分支的复制操作和具有多输入分支的异或操作。基于对线性变换本源表示的观测,我们使用两个推广的模型给出了构建复杂线性层MILP模型的一般方法。结合该方法,解决了基于MILP方法比特级分离特性的自动化搜索在具有非比特置换线性层算法上的适用性问题,拓宽了 MILP搜索方法的使用范围,使其在搜索积分区分器方面发挥更大的优势。考虑到ARX类算法在分组密码算法中的重要地位,我们构建了模加运算的MILP模型,使得基于MILP思想的比特级分离特性自动

10、化搜索方法推广到ARX类算法。基于上述推广的模型,我们对一系列算法的积分区分器进行了搜索,对Midori64算法、LED64算法、Joltik-BC算法、Serpent 算法、Noekeon算法、HIGHT算法和LEA等算法的积分区分器给出了不同程度的改进。构建了基于SAT方法ARX类算法比特级分离特性的自动化搜索工具:注意到在ARX类算法差分/线性路线的自动化搜索中,基于SAT/SMT的方法在表现上优于那些基于MILP的方法,我们针对ARX类算法构建了基于SAT问题自动化搜索比特级分离特性的工具。首先,我们对三种基本运算(复制运算、与运算和异或运算)的比特级分离特性建模,将分离特性在运算中的

11、传递规律转化为满足合取范式形式的逻辑表达式。随后,基于这三种基本操作,我们构建了刻画模加运算比特级分离特性的SAT模型。设置好初始分离特性和终止规则后,ARX算法比特级分离特性的搜索问题将转化为SAT问题,进而可调用求解器求解。为了快速定位目标算法的最优积分区分器,我们给出了一种高效的搜索算法,这一算法可以帮助我们缩减初始分离特性的搜索空间,快速定位导出最优积分区分器的初始分离特性的形式。基于这一方法,我们得到了SHACAL-2算法的17轮积分区分器,这使得该算法最优积分区分器轮数改进了 4轮。除此之外,对LEA算法、HIGHT算法和SPECK算法,新获取的积分区分器与用MILP方法得到的结果相比都有不同程度的改进。构建了基于SMT方法自动化搜索字级分离特性的新工具:一方面,考虑到自动化搜索在字级分离特性评估中的空白;另一方面,观察到对大状态/含复杂运算的算法在比特水平追踪分离特性的困难性,我们使用基于SMT的方法实现了字级分离特性的自动化搜索。首先,考虑对字级分离特性在一些基本运算中的传递规律建模,模型的构建采用排除法。而后,合理的设置初始分离特性和终止条件,以将字级分离特性的搜索问题转化为SMT问题,并调用开源求解器对问题进行求解。基于该方法