论文部分内容阅读
在万物互联时代,随着物联网设备的普及,相关的网络安全问题也面临着更加严峻的挑战。密码作为保障网络安全的基石,在信息传递、加密保护、安全认证等方面发挥了十分重要的作用。原有的传统对称密码算法主要针对桌面/服务器等资源丰富的应用环境,以安全性最大化为设计目标。而在资源受限的应用场景之中,对称密码算法的设计趋于轻量化,要求对算法的软硬件实现性能与安全性进行权衡。所以近年来轻量级对称密码算法的设计与实现逐渐成为研究热点之一。本质上,轻量级对称密码设计与实现的核心是对算法组件的研究,只有从组件的设计上进行原始创新,才能解决现有信息系统对密码算法提出的新挑战。在很多轻量级对称密码算法中,S盒是唯一的非线性组件,主要起到了混淆的作用。轻量级S盒的设计分为两个关键的层面:安全性强度和软硬件实现性能。从安全性的角度,针对不同的应用场景,需要更精细化地控制S盒的多个密码学性质,以达到不同的安全性强度要求。从软硬件实现的角度,虽然有很多商业软件可以针对通用场景下的电路进行优化,但轻量级对称密码算法中主要使用4比特和5比特的小尺寸S盒,所以针对这种S盒需要专门的硬件实现电路优化方案。基于此我们展开了研究,具体成果如下:构建了基于可满足性问题（SAT/SMT）的自动化搜索S盒的模型:在传统对称密码S盒的设计中,设计者更关注差分均匀度和线性度这两个性质,以评估算法抵抗差分、线性攻击的能力。而在轻量级S盒中,其他密码学性质,例如差分均匀度和线性度的频率、差分分布表和线性逼近表中BIBO（Bad Input and Bad Output）模式的数量能更精确地度量算法抵抗差分、线性攻击的能力。已有的S盒设计方法在考虑多个安全性性质的时候,需要分步进行筛选,导致搜索效率低且粒度粗,从而遗漏一些S盒。为了能精确控制和统筹考虑多个安全性性质,我们构建了基于SAT问题的S盒自动化搜索模型。根据我们的研究,绝大部分安全性性质都可以由S盒的差分分布表、线性逼近表直接体现。基于此,我们提出了新的设计思路:先构建满足要求的差分分布表和线性逼近表,再逆向地重构出对应的S盒。·首先,我们将S盒与其差分分布表、线性逼近表之间的关系转化为可满足性问题中的布尔等式。当给定差分分布表或线性逼近表的时候,可以利用SAT求解器重构出对应的S盒。我们以PRESENT算法和KECCAK算法中S盒对应的DDT为例,在较短时间内分别重构出了全部256个4比特S盒和1024个5比特S盒。·然后,我们将对于差分分布表和线性逼近表的安全性性质要求,转化为约束条件。再同样以布尔等式的形式描述并添加进模型中。最后,利用重构S盒的方法,找到满足要求的S盒。与之前的方法相比,我们可以更精细化地考虑多个密码学性质。对4比特的S盒,以PRESENT/GIFT/RECTANGLE算法中S盒为例,我们分别搜索出了 3723/947/620个具有相同性质的S盒。此外,我们以略微提升差分均匀度为代价,使差分分布表和线性逼近表中BIBO模式的个数降低,最终获得了 834个新的S盒。对5比特S盒,以KECCAK和ASCON算法中S盒为例,我们分别搜索到了 31/28个具有相同性质的S盒。更进一步,我们搜索到了 17个具有更低差分均匀度的新S盒。当得到一个安全性性质好的S盒,可以通过等价变换得到一族具有相同性质的S盒,所以S盒等价分类的理论研究也十分具有意义。在2019年的Designs,Codes and Cryptography期刊上,Boura等人提出了关于S盒DDT等价类的猜想:若给定一个任意两行均不相同的DDT,则与之对应的S盒均满足平凡的DDT等价形式。我们创造性地提出了一个关于S盒DDT等价关系的命题和两个推论,并将验证范围从244缩小到了 259,从而验证了 Boura等人的猜想在4比特S盒上的正确性。提出了基于可满足性问题的搜索给定S盒最小面积硬件实现的模型:硬件面积是轻量级S盒实现中的重要指标之一。然而,在此之前没有一种有效的方法能搜索S盒最小面积的硬件实现。现有的硬件实现优化方法可以分为两类,一类是启发式的搜索方法,旨在找到一个令人满意但不一定最优的实现,适用于较大的S盒;另一类是基于SAT问题的搜索方法,只能搜索给定S盒使用最少标准单元门的硬件实现。然而不同的标准单元门具有不同的面积,标准单元门最少的硬件实现,其面积不一定最小。我们将多输入的复杂标准单元门以新的编码方式进行描述,并以面积为目标函数进行给定S盒的硬件实现搜索。为了提升搜索的速度,我们提出了并行算法和用于确定标准单元门数量上下界的预计算算法。我们将模型分别应用在了PICCOLO、SKINNY、RECTANGLE和LBLOCK算法中的4比特S盒上。在相同的技术库和标准单元门下,与之前的结果相比,RECTANGLE算法的S盒的硬件实现面积降低为18.00GE。同时证明了目前PICCOLO、SKINNY、LBLOCK中S盒的硬件实现面积是最优的。得益于加速技术的使用,我们模型同样适用于KECCAK算法和ASCON算法中5比特S盒硬件实现的搜索。