基于SAT 的差分和线性活跃S 盒搜索方法*

苗旭东，董新锋，韩 羽，穆道光，张文政

（1.中国电子科技集团公司第三十研究所，四川 成都 610041；2.保密通信重点实验室，四川 成都 610041）

0 引 言

差分和线性分析是分组密码的两种最基本的安全性分析评估方法，对于分组较大（64 比特以上）且S 盒尺寸较大（4 比特以上）的密码算法而言，一般通过搜索活跃S 盒的个数来评估密码算法抵抗差分和线性分析的能力，目前通常采用基于分支定界[1]和混合整数线性规划[2]（Mixed Integer Linear Programming，MILP）的自动化搜索方法。基于分支定界的密码分析技术的提出时间较早，建模相对复杂，而基于MILP和 布 尔 可 满 足 性 问 题[3]（Boolean Satisfiability Problem，SAT）的密码分析技术是近年来提出的方法，建模相对简单。两种方法都属于约束规划问题，算法分析人员只需考虑如何将密码分析问题转换为两种约束规划问题，不需要考虑如何求解计算的问题。MILP 和SAT 具有自动化集成度高、求解器计算能力强、密码分析效果好的特点，已成为目前行业较为通用的两种密码自动化分析技术。

2013 年，Mouha 等 人[3]首 次 提 出 了 基 于SAT 的最优差分特征分析技术，并成功得到了ARX 结构算法Salsa20 的3 轮最优差分特征，由于SAT 求解器的计算能力强，SAT 语句（合取范式）的表达能力强，基于SAT 的密码分析技术很快被应用到密码算法的多种安全性分析技术中[4-6]。截至目前，基于SAT 的密码自动化分析方法主要包括：比特级的最优差分和线性特征分析、比特级和字节级的积分可分性分析等，还没有基于SAT 的差分和线性活跃S 盒分析方法。基于此，本文对如何将差分和线性活跃S盒搜索问题转化为SAT 问题进行研究，目的是使SAT 成为密码算法安全性分析和评估的一种更为通用的方法。

1 密码基本部件建模

由于公开文献中没有对基于SAT 的差分和线性活跃S 盒分析技术的研究，唯一可借鉴的是基于MILP 的差分和线性活跃S 盒分析技术，两种分析技术中关键的一步是将密码基本部件的差分和线性传播行为用相应的语句刻画。基于SAT 的密码分析技术需要将密码分析问题转换为SAT 模型，本质上是将密码基本部件的差分和线性传播行为用合取范式（与、或、非3种操作）表示，由于差分和线性活跃S 盒分析是一种字节级的建模方法，本文首次提出了字节级分支、异或、最大距离可分码（Maximum Distance Separable Codes，MDS）合取范式刻画，并介绍了具体的刻画方法。

1.1 字节级分支操作

字节级分支操作如图1 所示，其中，x 为代表输入差分或掩码，y 和z 为分成两支的输出差分或掩码。

分支操作的差分传播模式为(x →y, z)，所有可能的传播模式的真值表点有：

分支操作的线性掩码传播模式为(x →y, z)，所有可能的传播模式的真值表点有：

用合取范式表达线性掩码传播的真值表点为：

1.2 字节级异或操作

字节级异或操作如图2 所示，x 和y 代表输入差分或掩码，z 为经过异或后的输出差分或掩码。

由于差分和线性分析存在对偶特征，字节异或的差分传播行为和字节分支的线性传播行为是相同的，因此，字节异或的差分传播行为的合取范式为：

同上，字节异或的线性传播行为和字节分支的差分传播行为是相同的，因此，字节异或的线性传播行为的合取范式为：

1.3 MDS 矩阵

MDS 矩阵常用于SPN、Feistel 结构密码算法的线性扩散层中，例如，AES 域构造的线性扩散层和Dblock 基于循环移位的线性扩散层均可按字节为单位当作4×4 的MDS，如图3 所示。

假设MDS矩阵的输入差分或掩码为a,b,c,d，经过MDS 后的输出差分或掩码为e,f,g,h，(a,b,c,d,e,f,g,h)变量的值取0 或1，分别代表相应字节的差分或掩码值为0 或非0，由于MDS 矩阵的差分和线性分支数均为5，在活跃S 盒分析中，仅利用了该性质，不会考虑MDS 的具体实施细节。因此，利用差分和线性活跃S 盒分析方法时，对MDS 的刻画是相同的，本文仅考虑分支数为5 的刻画方法，如下文所述。

考虑所有的输入输出可能模式，即当输入非零时，输入输出至少有5 个字节非零，共种情况；当输入为零时，输出为零，仅1 种情况。因此，可能的传播模式共94 种，而不可能的传播模式有256-94=162 种，采用逻辑刻画[6]的方法需要162 个逻辑表达式。利用逻辑表达式优化技术，将所有94 种可能的传播模式的真值表点输入到Logic Friday 软件中，再执行Product of Sum 操作，将真值表点转换为SAT 语言的合取范式，共162 条。表达式过多会影响SAT 求解器的求解效率，还需做进一步的优化。利用Logic Friday 软件集成的Quine-McCluskey 和Espresso 算法求解出一个最少数量的合取范式，最终仅用70 个表达式表示，具体如下：

本节仅考查了线性扩散层为MDS 矩阵时的一种通用建模方法，当面对几乎MDS 矩阵、0/1线性扩散矩阵等其他线性扩散层时，均可采用该方法建立模型。

2 搜索策略设置

本文介绍了密码基本部件的建模方法，在分析一个具体的密码算法时，首先，根据密码算法中部件的先后顺序建立相应的SAT 模型；其次，根据不同的分析方法，对初始条件、目标值进行设置；最后，调用一个求解算法，对SAT 模型进行求解，才能得出最终的分析结果。

2.1 初始条件设置

假设分组密码的分组长度为m，输入差分或掩码为x0,x1,…,xm-1，为避免SAT 问题出现平凡的全零解，须设置输入差分或掩码非零，合取范式为：

2.2 目标条件设置

假设待分析算法中S 盒的个数为n，统计活跃S 盒的变量为x0,x1,…,xm-1，要判定活跃S 盒的个数总和是否达到一个指定值k，即判定SAT 问题是否有可满足解，用线性不等式表示：

由于合取范式不支持线性不等式表示，须将线性不等式转换为合取范式，采用序列编码方法[7]，将该问题转化为合取范式，序列编码电路如图4 所示。

将以上电路转换为合取范式表示为[7-8]：

式中：si,j为辅助计数变量，取值均为0 或1。

将该约束条件写入SAT 模型即可判断指定活跃S 盒个数是否有可满足解。

2.3 搜索算法

按照本文中密码基本部件的建模方法和约束条件设置方法，建立了密码算法活跃S 盒搜索的SAT 模型，交给SAT 求解，并利用以下算法求解活跃S 盒的个数，基本方法为先给SAT模型设置一个较小的目标值，使模型没有满足解，再逐渐增大目标值，当SAT 模型有满足解时，该目标值即为活跃S 盒的个数。算法1：基于SAT 的活跃S 盒搜索算法输入：SAT 模型，活跃S 盒个数初始值k输出：最小活跃S 盒个数k

1 将活跃S 盒个数k 设定为一个最小值0；

2 将SAT 模型交给CaDiCaL 求解

3 若得到不满足解

则k=k+1，并返回步骤2

4 若得到满足解

返回k 的值

3 实际应用效果

为了验证本文提出的搜索活跃S 盒方法的实际应用效果，对经典SPN 结构的AES 算法和Feistel 结构的Dblock 系列算法的活跃S 盒个数进行搜索，由于两个算法的差分和线性活跃S盒相同，统一用活跃S 盒表示。实施效果如表1、表2 所示。

表1 AES 活跃S 盒个数

表2 Dblock-128 活跃S 盒个数

从表1 和表2 可以看出，利用SAT 技术对组长度为128 比特的密码算法活跃S 盒进行搜索时，所需时间较短，通常在几分钟内就可以给出搜索结果。但从表1 也可以看出搜索AES算法8 轮活跃S 盒的时间偏长，原因在于7 轮到8 轮的活跃S 盒个数差值较大，搜索算法需要判断16 次才能给出一个满足的解。

从表3 可以看出，利用SAT 技术对分组长度大于128 比特的密码算法活跃S 盒进行搜索时，所需时间较长，表3 中“时间”为未采用任何加速方法的搜索结果，搜索时间相对较长，为了提高搜索效率，本文借鉴文献[8]中的加速方法，将Matsui 的分支定界搜索策略融入SAT模型中，起到加速作用，表3 中“加速时间”一列为加速后的搜索时间，可以看到，在搜索长轮数的模型时加速效果显著。

对于Dblock-256 而言，由于分组长度较大，模型更加复杂，搜索时间过长，利用本文提出的方法结合加速策略仅搜索到17 轮，如表4 所示。

表3 Dblock-192 活跃S 盒个数

表4 Dblock-256 活跃S 盒个数

从整体搜索效果来看，在借助分支定界的加速策略条件下，基于SAT 的活跃S 盒搜索方法基本满足活跃S 盒搜索需求。可以搜索出分组较大达到安全性轮数的活跃S 盒个数。

4 结 语

本文提出了一种新的基于SAT 的差分和线性活跃S 盒搜索方法，可以用较少的合取范式子句刻画字节级分支、异或、MDS 的差分和线性传播行为，给出了详细的建模和搜索方法，并利用该方法成功搜索出AES、Dblock 系列算法的活跃S 盒个数，实际使用效果较好。将基于SAT的密码分析技术从比特级扩展到字节级，使得SAT 成为一种更加通用的密码分析方法。但面对分组更大（分组长度大于256 比特）的密码算法活跃S 盒时，该方法也很难计算出完整轮的活跃S 盒，因此，在后续的研究中将着重优化模型和提升本方法的搜索效率。