第 9 章：区分器的自动化搜索
前几章的区分器都是手工构造的：差分路线一轮一轮地推，积分特性一个组件一个组件地传。对 AES 这样的小规模例子还行，但真实算法一轮就可以拆成成百上千个基本操作，手工搜索既慢又容易漏。近年来大量工作把区分器搜索转化为求解器问题，常见的有：
- 混合整数线性规划 (Mixed Integer Linear Programming, MILP)；
- 可满足性模理论 (Satisfiability Modulo Theories, SMT) 与 布尔可满足性 (SAT)；
- 约束规划 (Constraint Programming, CP)。
不同的技术各有特点，但都要做同一件事：对非线性组件和线性组件的传播性质进行刻画。刻画的精确程度决定了区分器搜索模型的精确程度。本章先讲 MILP，再讲 SAT。
§ 01MILP 自动化求解工具
1.1 MILP 简介
MILP 顾名思义：目标函数是线性的，所有约束也是线性的，决策变量可以取整数。
例 1.1
两个整数 \(x,y\) 满足 \(x+2y>5\) 和 \(x-y>1\)，求 \(x+y\) 的最小值。
解
把它输入 MILP 求解器：设两个整数变量 \(x,y\)，加两个约束 \(x+2y\ge6\)、\(x-y\ge2\)（整数严格不等式改成非严格），目标 \(\min(x+y)\)。手算：由 \(x\ge y+2\) 和 \(x\ge6-2y\)，\(x+y\ge\max(2y+2,\ 6-y)\)。\(y=1\) 时下界为 \(\max(4,5)=5\)，\(y=2\) 时为 \(\max(6,4)=6\)，\(y=0\) 时为 \(6\)。所以最小值为 \(5\)，在 \((x,y)=(4,1)\) 处取到。
密码分析中的变量大多是布尔量，只取 \(0,1\)。MILP 里用整数变量表示它们，再用一组线性不等式把可行的取值组合“围”出来——能且仅能让满足传播规则的取值满足不等式。下面所有建模都是在做这件事。
1.2 差分区分器的搜索
Mouha 等与 Wu、Wang 率先把计算最小差分活跃 S 盒个数转化为 MILP 问题：对目标算法构建差分模型，用开源或商业求解器求解，得到最少差分活跃 S 盒数。这一方法后来被用来搜索特定模式的差分特征和线性逼近，加入特定的表示方法后又被用来计算比特级分组密码的最小活跃 S 盒数。
孙思维等精准刻画了 S 盒的差分传播特性，首次给出精确的 S 盒差分传播 MILP 模型（同样适用于线性分析），主要适用于包含比特级异或、S 盒（小于 8 比特）和比特级线性置换的算法。之后对 MILP 模型的改进都基于此，下面着重介绍这个模型。
分支 (COPY)。 差分满足 \(a=b=c\)，\(a\) 为输入差分，\(b,c\) 为两个输出差分。
异或 (XOR)。 对比特级异或 \(a\oplus b=c\)（\(a,b\) 为输入差分，\(c\) 为输出差分），引入辅助布尔变量 \(d_\oplus\)，
习题 1.2
证明不等式组 (1) 恰好刻画了异或的差分传播。
解
单比特异或所有可能的差分传播为 \((a,b,c)\in\{(0,0,0),(0,1,1),(1,0,1),(1,1,0)\}\)。
- \(a+b+c\le2\) 排除了 \((1,1,1)\)；
- 若 \(a,b,c\) 中恰有一个为 \(1\)：前三式迫使 \(d_\oplus=1\)，第四式要求 \(1\ge2\)，矛盾，所以 \((1,0,0)\)、\((0,1,0)\)、\((0,0,1)\) 都被排除；
- \((0,0,0)\) 取 \(d_\oplus=0\) 可行；恰有两个为 \(1\) 时取 \(d_\oplus=1\)，\(2\ge2\) 可行。
（我用程序枚举 \((a,b,c,d_\oplus)\) 核对过，可行的 \((a,b,c)\) 恰为上述四组。）\(d_\oplus\) 的意义是“这个异或是否活跃”。
S 盒。 关键工具是凸包。
定义 1.3凸包
有限点集 \(P\subseteq\mathbb R^n\) 的凸包 \(\mathrm{conv}(P)\) 是 \(\mathbb R^n\) 中包含 \(P\) 的最小凸集。
命题 1.4凸包的 \(H\) 表示
对任意有限点集 \(P\subseteq\mathbb R^n\)，存在一组线性不等式 \(H_{\mathrm{conv}}(P)\)，
其解空间恰为 \(\mathrm{conv}(P)\)，\(\lambda_{i,j}\) 为固定实数。称为凸包的 \(H\) 表示 (H-representation)。
对一个 \(w\times v\) 的 S 盒，输入差分为 \((x_0,\cdots,x_{w-1})\)，输出差分为 \((y_0,\cdots,y_{v-1})\)，把 \((x_0,\cdots,x_{w-1},y_0,\cdots,y_{v-1})\) 看作 \(\{0,1\}^{w+v}\subseteq\mathbb R^{w+v}\) 中的点。所有可能的差分传播模式构成一个点集 \(P\)。\(\{0,1\}^{w+v}\) 的点都是 \([0,1]^{w+v}\) 的顶点，所以 \(\mathrm{conv}(P)\) 中的 \(0/1\) 点恰好就是 \(P\) 本身。求出 \(P\) 的 \(H\) 表示，就得到了精确刻画 S 盒差分传播的不等式组。
但这样得到的不等式往往数量庞大，全部加入模型会让求解变得很慢。孙思维等提出用贪心算法筛选：其实不需要整个凸包，只需要一组不等式能把所有不可能的传播模式排除即可。
定理 1.5算法（贪心筛选不等式）
输入：S 盒凸包的 \(H\) 表示 \(\mathcal H\)，S 盒不可能差分传播模式的集合 \(\mathcal X\)。输出：筛选出的不等式集合 \(O\)。
- \(\mathcal X^*\leftarrow\mathcal X\)，\(\mathcal H^*\leftarrow\mathcal H\)，\(O\leftarrow\varnothing\)；
- 循环：
- \(\mathcal L\leftarrow\mathcal H^*\) 中能删掉 \(\mathcal X^*\) 中最多不可能模式的那个不等式；
- \(\mathcal X^*\leftarrow\) 经 \(\mathcal L\) 筛选后 \(\mathcal X^*\) 中剩下的模式；
- \(\mathcal H^*\leftarrow\mathcal H^*\setminus\{\mathcal L\}\)，\(O\leftarrow O\cup\{\mathcal L\}\)；
- 若 \(\mathcal X^*=\varnothing\)，返回 \(O\)。
目标函数。 搜索一定轮数的差分路线时，希望路线包含的活跃 S 盒尽量少，所以目标函数与活跃 S 盒（或概率）相关。对双射 S 盒，非零输入差分必然导致非零输出差分。引入标志变量 \(A_t\) 表示 S 盒是否活跃，要保证 \(A_t=1\) 当且仅当 \((x_0,\cdots,x_{w-1})\) 非零：
为保证非零输入差分必然产生非零输出差分（以及反过来），还要
最后把目标函数设为 \(\min\sum A_t\)，就能搜索 MILP 模型中最小活跃 S 盒数对应的差分路线。
例 1.6LBlock 的 S 盒 \(S_0\)
LBlock 的一个 S 盒为
| \(x\) | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| \(S_0(x)\) | 14 | 9 | 15 | 0 | 13 | 4 | 10 | 11 | 1 | 2 | 8 | 3 | 7 | 6 | 12 | 5 |
先作出差分分布表，得到所有可能和不可能的差分传播模式，用 SageMath 计算可能模式对应凸包的 \(H\) 表示，共 205 个线性不等式；再用贪心算法筛选，得到 28 个不等式，例如
（\(x\) 在这里指 8 维向量 \((x_0,\cdots,x_3,y_0,\cdots,y_3)\)。）
注
我用程序算了 \(S_0\) 的差分分布表：非零输入差分的行里，非零项只有 \(2\) 和 \(4\) 两种取值（分别 72 个和 24 个），可能的差分模式共 \(97\) 个（含 \(0\to0\)），不可能的 \(159\) 个。贪心算法要排除的就是这 159 个点。205 和 28 这两个数依赖于凸包软件与贪心的具体实现，我没有复算。
习题 1.7
上面的模型只区分了“可能”与“不可能”。但差分分布表中不同的传播概率不同，如何把这种不均匀性刻画进 MILP 模型，得到更准确的区分器？
解
给每个 S 盒引入记录概率指数的变量。以 LBlock 的 \(S_0\) 为例，差分分布表中非零项只有 \(N_s(\delta_{\mathrm{in}},\delta_{\mathrm{out}})\in\{2,4\}\)（再加上 \(0\to0\) 的 \(16\)），对应概率的负对数 \(-\log_2\frac{N_s}{2^4}\in\{0,2,3\}\)。用两个布尔变量 \(dp_0,dp_1\) 编码这个指数，例如 \(3dp_0+2dp_1\)：\((0,0)\mapsto0\)，\((0,1)\mapsto2\)，\((1,0)\mapsto3\)。
把 S 盒的点改为 \((w+v+u)\) 维向量 \((x_0,\cdots,x_{w-1},y_0,\cdots,y_{v-1},dp_0,\cdots,dp_{u-1})\in\{0,1\}^{w+v+u}\)，所有“可能传播 + 对应概率指数”的组合构成点集，计算它的凸包 \(H\) 表示并用贪心筛选，就得到同时刻画传播与概率的不等式组。目标函数从 \(\sum A_t\) 改为 \(\sum\mathrm{DP}_t\)，\(\mathrm{DP}_t=3dp_{t,0}+2dp_{t,1}\) 是第 \(t\) 个 S 盒的概率指数。这样求得的是概率最高的差分特征，而不仅是活跃 S 盒最少的。
1.3 线性区分器的搜索
线性分析和差分分析是最基础的密码分析方法，第一步也是最重要的一步就是找高概率的差分特征或线性逼近。孙思维等的精确 S 盒模型同样适用于线性分析，只需按掩码传播的特点修改组件模型。
异或。 掩码满足 \(a=b=c\)，\(a,b\) 为两个输入掩码，\(c\) 为输出掩码。
分支。 输入掩码 \(a\)，输出掩码 \(b,c\)，引入辅助变量 \(d_\Gamma\)，
S 盒。 与差分相同，用 \(A_t\) 记录活跃状态，输入掩码为 \((x_0,\cdots,x_{w-1})\)，约束同 (2)。
可见掩码传播与差分传播呈现对偶的性质：差分的分支模型类比于掩码的异或模型，差分的异或模型类比于掩码的分支模型。这种对偶正是第八章中不可能差分与零相关线性壳等价的根源。
最优相关度模型。 类比差分，用 \(c_0,\cdots,c_{u-1}\) 表示掩码传播相关度的指数，S 盒凸包的点改为 \((x_0,\cdots,x_{w-1},y_0,\cdots,y_{v-1},c_0,\cdots,c_{u-1})\in\{0,1\}^{w+v+u}\)，目标函数从 \(\sum A_t\) 改为 \(\sum\mathrm{Cor}_t\)。
1.4 不可能差分/零相关线性路线的搜索
不可能差分/零相关线性路线是一条不可能存在的差分/线性路线，所以搜索的思路是：判断 MILP 模型是否存在矛盾。固定输入输出差分，把模型交给求解器：若无可行解，就找到了一条不可能差分路线。
定理 1.8算法（通用不可能差分搜索算法）
输入：所选定的输入差分集合 \(\Delta_{\mathrm{in}}\)，输出差分集合 \(\Delta_{\mathrm{out}}\)。输出：不可能差分路线集合 \(O\)。
- \(O\leftarrow\varnothing\)；
- 对每个 \(\alpha\in\Delta_{\mathrm{in}}\)，\(\beta\in\Delta_{\mathrm{out}}\)：
- \(\mathcal M\leftarrow\) 根据 \((\alpha,\beta)\) 生成的算法差分 MILP 模型；
- 若 \(\mathcal M\) 无解，\(O\leftarrow O\cup\{(\alpha,\beta)\}\)。
零相关线性路线类似，把差分模型换成线性模型。
注
\(\Delta_{\mathrm{in}}\)、\(\Delta_{\mathrm{out}}\) 可以根据算法的特点选取或遍历。通常选择输入差分只有一个块活跃、其他块不活跃，输出差分也只有一个块活跃，这样最容易拉长不可能差分区分器的轮数。以 AES-128 为例，遍历输入输出单块活跃的所有情况，需要 \(16\times16=256\) 个不同输入输出差分的 MILP 模型。
要注意：这里的 S 盒如果只用“可能/不可能”模式刻画，搜到的是具体 S 盒下的不可能差分；如果只刻画活跃性（非零进、非零出），搜到的就是第八章意义下“结构”的不可能差分。
习题 1.9
搜索 CipherFour 最长轮数的不可能差分/零相关线性路线，给出输入输出差分/掩码，并手动验证路线的矛盾。
思路
CipherFour（见算法附录）是 16 比特 SPN，线性层是对合的比特置换。
- 建模：每轮 4 个 S 盒，每个 S 盒用其差分分布表可能模式的凸包不等式刻画，比特置换只是变量重命名，不需要约束；
- 遍历：输入差分取“一个半字节非零、其余为零”的 \(4\times15=60\) 种，输出差分同样 60 种，共 3600 个模型，对 \(r=1,2,3,\cdots\) 逐轮增加，直到所有模型都有解为止；
- 手动验证：对找到的最长 \((\alpha,\beta)\)，从 \(\alpha\) 向前传播、从 \(\beta\) 向后传播，各用概率 1 的规则（零差分 S 盒输出为零，比特置换确定），在中间某一轮看到某个比特/半字节一边必为零、另一边必非零，就是矛盾。
由第八章的结论，CipherFour 的线性层满足 \(P^{\mathrm T}P=I\)，零相关线性路线的搜索结果在结构意义下与不可能差分相同。这道题我没有实际跑出结果，最长轮数留待自己用求解器验证。
1.5 分离特性的搜索
第五章介绍了比特级分离特性的传播规则，以及它经过 COPY、XOR、AND 的规律。但实际算法的轮函数可以拆成成百上千个基本操作，一轮的分离特性传播路线就可能多达上万条，多轮更是计算不过来。这时就要借助求解器：用线性不等式刻画传播规律，输入 MILP 求解器自动搜索分离特性的传播路线（称为分离路线 (division trail)），从而判断是否存在积分区分器。
起始约束。 以两子集比特级分离特性为例，若输入多重集 \(X\) 具有 \(\mathcal D^{1^n}_{\mathbb K}\)，\(\mathbb K=\{(0,1,1,\cdots,1)\}\)，在 MILP 中用 \(n\) 个二进制变量 \(x_1,\cdots,x_n\) 表示，加约束 \(x_1=0\)，\(x_2=\cdots=x_n=1\)。
COPY。 输入 \((m)\in\mathbb F_2\)，输出 \((m,m)\in\mathbb F_2^2\)。可能的分离路线有 \((0)\to(0,0)\)，\((1)\to(0,1)\)，\((1)\to(1,0)\)，刻画为 \(x=y_1+y_2\)（\(x,y_1,y_2\) 为二进制变量）。
XOR。 输入 \((m_1,m_2)\)，输出 \(m_1\oplus m_2\)。可能的路线有 \((0,0)\to(0)\)，\((0,1)\to(1)\)，\((1,0)\to(1)\)，刻画为 \(x_1+x_2=y\)。
AND。 输入 \((m_1,m_2)\)，输出 \(m_1\wedge m_2\)。可能的路线有 \((0,0)\to(0)\)，\((1,1)\to(1)\)，刻画为
注
我枚举了一下，这组 AND 不等式允许的 \((x_1,x_2,y)\) 是 \((0,0,0)\)、\((0,1,1)\)、\((1,0,1)\)、\((1,1,1)\)，比文字中说的两种多了 \((0,1)\to(1)\) 和 \((1,0)\to(1)\)。这不是错误：这两条路线也是合法的（只是冗余），这正是 Xiang 等最初给出的 AND 模型。后面 SAT 部分的 AND 子句只允许 \((0,0,0)\) 与 \((1,1,1)\)，两者搜到的结论相同。
结束约束。 设输出多重集具有 \(\mathcal D^{1^n}_{\mathbb K'}\)，用 \(n\) 个二进制变量 \(z_1,\cdots,z_n\) 表示 \(\mathbb K'\) 中向量的取值。要判断 \(\mathbb K'\) 是否包含所有单位向量：设目标函数 \(\min\{z_1+z_2+\cdots+z_n\}\)。若某个单位向量不能作为可行解（例如固定 \(z_1=1\)、其余为 \(0\) 时模型无解），就搜到了对应比特的零和积分区分器。
习题 1.10
用 MILP 求解器建模并搜索：当输入多重集 \(\mathbb X\) 具有 \(\mathcal D^{1^{32}}_{\mathbb K}\)，\(\mathbb K=\{(0,1,1,\cdots,1)\}\) 时，SIMON32 第 12 轮输出的第一比特是否存在积分区分器？
思路
SIMON32 一轮的轮函数为 \((L,R)\mapsto(R\oplus f(L)\oplus k,\ L)\)，\(f(L)=\big((L\lll1)\wedge(L\lll8)\big)\oplus(L\lll2)\)。拆成基本操作：\(L\) 的每个比特要被使用 4 次（输出到右半、\(\lll1\)、\(\lll8\)、\(\lll2\)），所以每个比特是一个 3 次 COPY；AND 对 16 比特逐位作用；再与 \(\lll2\) 和 \(R\) 作两次 XOR；密钥异或对两子集分离特性没有影响。按上面的不等式逐轮建模 12 轮，在输出端固定只有左半第一比特为 \(1\) 的单位向量，看模型是否无解。Todo–Morii 用比特级分离特性证明了 SIMON32 存在 14 轮积分区分器（输入 31 个活跃比特），所以 12 轮第一比特的结论应该是“存在”。具体答案见向泽军等 ASIACRYPT 2016 的论文。
§ 02SAT 自动化求解工具
SAT 是一个 NP 完全问题：判断一个由布尔变量和运算符构成的布尔表达式是否可满足。设置合适的限制，就能把搜索限制在较小的空间里，更容易求得解。用自动化工具 STP 可以把密码算法的约束转为可满足性问题去求解。
2.1 差分区分器的搜索
STP 的输入语言（CVC）可以直接对比特向量 (BITVECTOR) 建模，下面是刻画差分经过各种组件时的模型。
复制。 记 \((\alpha)\xrightarrow{\mathrm{COPY}}(\beta_0,\beta_1)\)，\(\alpha,\beta_0,\beta_1\) 都是 \(n\) 比特：
异或。 记 \((\alpha_0,\alpha_1)\xrightarrow{\mathrm{XOR}}(\beta)\)：
与。 比特级与运算可以看作一组 S 盒的级联，用 S 盒的规则刻画。
S 盒。 先刻画 S 盒的差分分布表：
刻画完整的差分分布表后，就可以刻画过 S 盒的所有可能传播：
\(\alpha=0\) 时必有 \(\beta=0\)，且 \(p=\mathrm{DDT}[\alpha\Vert\beta]=1\)。
矩阵乘。 先刻画矩阵 \(A\)，再用 \(\beta=A\cdot\alpha\) 计算差分：
\(A_i\) 表示 \(A\) 的第 \(i\) 列。
循环移位与移位。 用比特串的截取和拼接 @：
习题 2.1
如何借助 STP 刻画 CipherFour 的 S 盒（见算法附录）的差分分布表和概率传播？
解
CipherFour 的 S 盒是 \(4\times4\) 的，差分分布表有 \(16\times16\) 项。用一个以 8 比特 \(\alpha\Vert\beta\) 为下标、值为 \(-\log_2\) 概率（取整的权重）的数组刻画：
DDT : ARRAY BITVECTOR(8) OF BITVECTOR(4);
ASSERT(DDT[0bin00000000] = 0bin0000); % 0 -> 0 概率 1，权重 0
... % 对 256 项逐一 ASSERT
不可能的传播（DDT 值为 0）赋一个特殊值，例如 0bin1111，再对每个 S 盒加约束 ASSERT(NOT(p = 0bin1111)) 排除它们。可能的传播按 DDT 值 \(N\) 记权重 \(4-\log_2N\)：\(N=16\) 记 \(0\)，\(N=4\) 记 \(2\)，\(N=2\) 记 \(3\)。CipherFour 的 S 盒差分分布表中非零输入差分的最大项为 \(10\)（我用程序核对过），不是 2 的幂，这时可以把权重扩大若干倍再取整，或者改用 \(-\log_2\) 的定点表示。最后把所有 S 盒的权重加起来，用 ASSERT(BVLE(sum, w)) 限定总权重，从小到大增加 \(w\)，第一次可满足时就得到最优差分特征的概率 \(2^{-w}\)。
2.2 线性区分器的搜索
与差分类似，只是各组件刻画的是掩码传播。对偶性在这里体现得很清楚：
- 复制：\(\alpha=\mathrm{BVXOR}(\beta_0,\beta_1)\)；
- 异或：\(\beta=\alpha_0\)，\(\alpha_0=\alpha_1\)；
- 与：看作 S 盒处理；
- S 盒：用线性近似表 (LAT) 代替差分分布表，
LAT : ARRAY BITVECTOR(2n) OF BITVECTOR(n)，\(p=\mathrm{LAT}[\alpha\Vert\beta]\)。\(\alpha=0\) 时必有 \(\beta=0\)，且 \(p=1\)； -
矩阵乘：掩码按转置传播，\(\alpha=A^{\mathrm T}\cdot\beta\)：
\[ \mathrm{ASSERT}(\alpha=\mathrm{BVXOR}(A_1^{\mathrm T}\cdot\beta,\cdots,A_n^{\mathrm T}\cdot\beta)), \]\(A_i^{\mathrm T}\) 表示 \(A^{\mathrm T}\) 的第 \(i\) 行； - 循环移位、移位：与差分相同。
习题 2.2
如何借助 STP 刻画 CipherFour 的 S 盒的线性近似表和相关性的传播？
解
与上一题相同的思路，把数组的值换成相关度的权重。CipherFour 的 S 盒 LAT（以“满足个数 \(-8\)”计）非平凡项的绝对值为 \(2\)、\(4\)、\(6\)（我用程序核对过），对应相关度 \(\pm\frac14\)、\(\pm\frac12\)、\(\pm\frac34\)，权重 \(-\log_2|c|\) 为 \(2\)、\(1\)、\(0.415\)，非整数的同样要放大取整；\(0\to0\) 权重为 \(0\)；LAT 值为 \(0\) 的组合（相关度为 \(0\)）赋特殊值并排除。因为线性路线的相关度按堆积引理相乘，总权重仍是各 S 盒权重之和，同样逐步放宽上界找最优线性特征。注意符号不进入权重，单条路线的相关度绝对值才是我们关心的。
2.3 不可能差分/零相关线性路线的搜索
概率为 \(0\) 的差分路径即不可能差分路径。模型基于搜索差分路径的 SAT 模型，其中 S 盒模型要求转移概率 \(p>0\)。以 ARX 类算法为例，建模时以比特为单位，对模加和其他线性部件分别建立比特级可满足性模型，对路线首尾低汉明重量的输入和输出作部分遍历，寻找 \(R\) 轮不可能差分路线：在相应条件下求解器发现模型无解，就找到了一条不可能差分路线；有解说明该条件下有一条差分路线，继续遍历下一个条件。搜索算法与 §1.4 的算法完全相同，只是把 MILP 模型换成 SAT 模型。
零相关线性路线类似：寻找与密钥取值无关、相关度为 \(0\) 的线性壳 \(\alpha\to\beta\)，S 盒模型要求 \(p>0\)，若模型无解就找到了一条零相关线性路线。
习题 2.3
用 SAT 工具搜索 CipherFour 最长轮数的不可能差分路线，给出输入输出差分/掩码，并手动验证路线的矛盾。
提示
与 §1.4 的习题相同，只是工具换成 STP：每个 S 盒加 ASSERT(NOT(DDT[α@β] = 0bin0000))（即要求 \(p>0\)），比特置换用比特截取和拼接实现。STP 返回 Valid. 表示原问题（加了 QUERY(FALSE)）无解，即找到了不可能差分。
2.4 分离特性的搜索
用 SAT 求解器搜索分离特性的传播路线，从而判断是否存在积分区分器。
起始约束。 以两子集比特级分离特性为例，输入 \(\mathcal D^{1^n}_{\mathbb K}\)，\(\mathbb K=\{(0,1,1,\cdots,1)\}\)，用 \(n\) 个命题变量 \(x_1,\cdots,x_n\) 表示，写成 \(n\) 个布尔子句 \(\neg x_1\)，\(x_2\)，……，\(x_n\)。
各操作的刻画（每个子句是若干文字的析取，所有子句合取）：
| 操作 | 允许的路线 | SAT 子句 |
|---|---|---|
| COPY \((x)\to(y_1,y_2)\) | \((0)\to(0,0)\)，\((1)\to(0,1)\)，\((1)\to(1,0)\) | \(x\vee\neg y_1\)，\(x\vee\neg y_2\)，\(\neg x\vee y_1\vee y_2\)，\(\neg x\vee\neg y_1\vee\neg y_2\) |
| XOR \((x_1,x_2)\to(y)\) | \((0,0)\to(0)\)，\((0,1)\to(1)\)，\((1,0)\to(1)\) | \(y\vee\neg x_1\)，\(y\vee\neg x_2\)，\(\neg y\vee x_1\vee x_2\)，\(\neg y\vee\neg x_1\vee\neg x_2\) |
| AND \((x_1,x_2)\to(y)\) | \((0,0)\to(0)\)，\((1,1)\to(1)\) | \(y\vee\neg x_1\)，\(y\vee\neg x_2\)，\(\neg y\vee x_1\)，\(\neg y\vee x_2\) |
注
我枚举核对过：三组子句的可满足赋值恰好就是表中“允许的路线”。
密码算法的轮函数可以拆成若干个分支、异或、与操作的组合。对每个操作的输入输出设置命题变量，用布尔子句刻画它们的关系，就把输入多重集与输出多重集的分离特性在 SAT 求解器中联系起来：
结束约束。 若多重集具有分离特性 \(\mathcal D^{1^n}_{\mathbb K}\)，\(\mathbb K\) 不包括所有单位向量，就得到一个积分区分器；若包括所有单位向量，就没有找到积分区分器。
例 2.4
设输出多重集 \(\mathbb Y\) 具有 \(\mathcal D^{1^4}_{\mathbb K}\)，\(\mathbb K=\{(0,0,0,1),(0,0,1,0),(0,1,0,0),(1,0,0,0)\}\)，则对任意 \(\boldsymbol u\succeq\boldsymbol k_i\)，\(\boldsymbol k_i\in\mathbb K\)，\(\sum_{\boldsymbol x\in\mathbb Y}\pi_{\boldsymbol u}(\boldsymbol x)\) 都是不确定的，无法得到零和区分器。但若 \(\mathbb K'=\{(0,0,1,0),(0,1,0,0),(1,0,0,0)\}\) 中缺了 \((0,0,0,1)\)，则 \(\sum_{\boldsymbol x}\pi_{(0,0,0,1)}(\boldsymbol x)=0\)，就得到一个零和区分器。
所以在 SAT 求解器中，对第 \(r\) 轮输出的命题变量 \(z_1,\cdots,z_n\) 加约束：要判断输出第一比特上是否有零和区分器，就加一条子句 \(z_1\) 和若干条 \(\neg z_2,\cdots,\neg z_n\)（即要求 \(\mathbb K'\) 中含单位向量 \((1,0,\cdots,0)\)）。若 SAT 求解器输出无解，就证明了 \((1,0,\cdots,0)\notin\mathbb K'\)，即 \(\sum_{\boldsymbol x\in\mathbb X}\pi_{(1,0,\cdots,0)}(\boldsymbol x)=0\)。
注
教材此处把这条约束写成一条子句 \(z_1\cup\neg z_2\cup\neg z_3\cup\cdots\cup\neg z_n\)。按析取的含义，这条子句只要求“\(z_1\) 为真或某个 \(z_j\)（\(j\ge2\)）为假”，并不能把输出钉在单位向量 \((1,0,\cdots,0)\) 上。要达到文中的目的，应该写成 \(n\) 条单文字子句 \(z_1\)，\(\neg z_2\)，……，\(\neg z_n\) 的合取。上面按这个意思写。
习题 2.5
用 SAT 求解器建模并搜索：输入多重集 \(\mathbb X\) 具有 \(\mathcal D^{1^{32}}_{\mathbb K}\)，\(\mathbb K=\{(0,1,1,\cdots,1)\}\) 时，SIMON32 的第 12 轮输出的第一比特是否存在积分区分器？
提示
与 §1.5 的习题相同，把不等式换成上表的子句。用 CryptoMiniSat 或 STP 都可以；SAT 模型通常比 MILP 模型求解更快，这也是近年分离特性搜索多用 SAT 的原因。
2.5 \(\mathcal{DS}\) 中间相遇攻击的搜索
对称密码算法通过轮函数的迭代保证安全性，轮函数由若干组件函数有序组合而成。所以对 第六章的 \(\mathcal{DS}\) 中间相遇攻击，只需刻画出每个组件函数中需要施加的约束，就能构造整个算法的模型。具体地说：
- 对 \(\mathcal{DS}\) 中间相遇区分器，要刻画组件函数前向差分与后向确定性关系的传播；
- 对 \(\mathcal{DS}\) 中间相遇密钥恢复，还要在此基础上刻画组件函数的后向差分与前向确定性关系。
符号。 用 \(T\) 表示不同类型的模板变量，可以换成下文的 \(X,Y,Z\) 等。\(\mathrm{Vars}^{(i)}(T)=\{T_i[j]\mid0\le j<n_c\}\) 表示 \(\mathrm{state}_i\) 引入的一组 \(T\) 变量（\(n_c\) 为状态中字的个数）；\(\mathrm{Vars}_{(r)}(T)\) 表示第 \(r\) 轮的一组 \(T\) 变量，若每轮有 \(k\) 个 state，则 \(\mathrm{Vars}_{(r)}(T)=\{\mathrm{Vars}^{(kr)}(T),\cdots,\mathrm{Vars}^{(kr+k-1)}(T)\}\)。
区分器搜索模型
区分器中每个 \(\mathrm{state}_i\) 引入三类变量：
- \(X\) 型：刻画前向差分（\(X_i[j]=1\) 表示这个字的差分可能非零）；
- \(Y\) 型：刻画后向确定性关系（\(Y_i[j]=1\) 表示这个字的值要由尾部决定）；
- \(Z\) 型：刻画前向差分与后向确定性关系的交，\(Z_i[j]=1\) 表示这个字既活跃又被需要，它就是预计算中要遍历的变量。
前向差分的传播规则（与截断差分相同）：
- S 盒：\(X_{i+1}[j]=X_i[j]\)；
- 字级置换 \(P\)：\(X_{i+1}[j]=X_i[P[j]]\)；
- 列混合 MC：设 \(\{X_i[s_0],\cdots,X_i[s_{l-1}]\}\) 和 \(\{X_{i+1}[s_0],\cdots,X_{i+1}[s_{l-1}]\}\) 为 MC 一列的输入输出，\(X_{i+1}[s_a]=1\) 当且仅当 \(Q=\{X_i[s_j]\mid\mathrm{MC}[a][j]\ne0\}\) 中的元素不全为 \(0\)：
ASSERT(orTerm(Q) = X_{i+1}[s_a])，\(\mathrm{orTerm}(Q)\) 为 \(Q\) 中所有变量的或； - 分支：\(X_{i+1}[m]=X_i[j]\)，\(X_{i+1}[l]=X_i[j]\)；
- 异或：\(X_{i+1}[j]=X_i[m]\mid X_i[l]\)。
后向确定性关系的传播规则（从尾部往回推“需要知道哪些字”）：
- S 盒：\(Y_i[j]=Y_{i+1}[j]\)；
- 字级置换：\(Y_i[P[j]]=Y_{i+1}[j]\)；
- MC：\(Y_i[s_a]=1\) 当且仅当 \(Q=\{Y_{i+1}[s_j]\mid\mathrm{MC}^{\mathrm T}[a][j]\ne0\}\) 不全为 \(0\)，
ASSERT(orTerm(Q) = Y_i[s_a])； - 分支：\(Y_i[j]=Y_{i+1}[m]\mid Y_{i+1}[l]\)；
- 异或：\(Y_i[m]=Y_{i+1}[j]\)，\(Y_i[l]=Y_{i+1}[j]\)。
注意分支与异或在两个方向上又一次呈现对偶。
其他约束：
- 交：\(Z_i[j]=X_i[j]\ \&\ Y_i[j]\)；
-
必要约束：为得到非平凡解，头部的 \(X\) 型变量 \(\{X_0[0],\cdots,X_0[n_c-1]\}\) 不全为 \(0\)，尾部的 \(Y\) 型变量不全为 \(0\)；为保证区分器有效，S 盒输入位置的 \(Z\) 型变量的非零个数（即度数 \(d\)）要小于密钥字数 KW：
\[ \mathrm{ASSERT}(\mathrm{plusTerm}(\mathrm{ZVars})=\mathrm{degree}),\qquad\mathrm{ASSERT}(\mathrm{BVLT}(\mathrm{degree},\mathrm{KW})); \] -
额外约束：结合算法特性给出合适的约束，减少度数。
定理 2.6算法（\(\mathcal{DS}\) 中间相遇区分器搜索模型）
输入：密码算法 \(E\)，轮数 \(R\)，密钥字数 KW。输出：区分器的度数 \(d\)。
- 循环：
- 对 \(i=0,\cdots,R-1\)，声明 \(\mathrm{Vars}_{(i)}(X),\mathrm{Vars}_{(i)}(Y),\mathrm{Vars}_{(i)}(Z)\)，用规则 1–5 加前向差分约束，规则 6–10 加后向确定性约束，规则 11 加交的约束，规则 12、13 加必要和额外约束，全部写入 CVC 文件；
- 用 STP 运行 CVC 文件；
- 若无解，跳出循环；若有解，读出 degree 的值，令 \(\mathrm{KW}\leftarrow\) degree；
- 返回 \(d\leftarrow\mathrm{KW}\)。
每次有解就把上界收紧为当前解的度数，直到无解，得到度数最小的 \(\mathcal{DS}\) 中间相遇区分器，再根据 \(Z\) 型变量的取值把区分器提取出来。
密钥恢复模型
把加密分为 \(E=E_2\circ E_1\circ E_0\)，轮数分别为 \(r_0,r_1,r_2\)。
刻画区分器尾部 \(E_2\)。 每个 state 引入 \(W\) 型变量，刻画尾部的前向确定性关系：
- S 盒与字级置换的前向确定性关系与后向确定性关系的刻画相同；
- 分支的前向确定性关系与异或的后向确定性关系的刻画相同；
- 异或的前向确定性关系与分支的后向确定性关系的刻画相同；
- MC 的前向确定性关系与 MC 的前向差分刻画相同，只需把 MC 矩阵换成 \((\mathrm{MC}^{-1})^{\mathrm T}\)。
由此得到 \(E_2\) 中需要猜测值的位置，即 S 盒的 \(W\) 型输入变量中非零的位置。
刻画区分器头部 \(E_0\)。 每个 state 引入 \(M\) 型变量，刻画头部的后向差分：
- S 盒与字级置换的后向差分与前向差分的刻画相同；
- 分支的后向差分与异或的前向差分刻画相同；
- 异或的后向差分与分支的前向差分刻画相同；
- MC 的后向差分与前向差分的刻画相同，只需把 MC 换成 \(\mathrm{MC}^{-1}\)；
- \(Z\) 型变量线性层后向确定性关系：在 \(E_0\) 的 S 盒输入位置引入 \(Z\) 型变量，令其等于同位置的 \(M\) 型变量，再对每一轮按分支操作的后向确定性关系刻画。
由此得到 \(E_0\) 中需要猜测值的位置，即 S 盒的 \(Z\) 型输入变量中非零的位置。
提取需要猜测的密钥。
-
引入 SK 型变量 \(\mathrm{Vars(SK)}\)：在 \(E_0\) 处，SK 型变量等于异或密钥后的 \(Z\) 型变量；在 \(E_2\) 处，等于异或密钥前的 \(W\) 型变量。加约束
\[ \mathrm{ASSERT}(\mathrm{BVLT}(\mathrm{plusTerm}(\mathrm{Vars(SK)}),\mathrm{UpBound})), \]UpBound 是预先给定的、比密钥字数大的值。
定理 2.7算法（\(\mathcal{DS}\) 中间相遇攻击的自动化密钥恢复模型）
输入：\(E=E_2\circ E_1\circ E_0\)，轮数 \(r_0,r_1,r_2\)，区分器度数 \(d\)，密钥字数上界 UpBound。输出：需要猜测的密钥字数 Guess_Key。
- 对 \(E_0\) 的每一轮（\(i=0,\cdots,r_0-1\)）：声明 \(M\)、\(Z\) 型变量，用规则 18–20 加后向差分约束，规则 22 加后向确定性约束；
- 对 \(E_1\) 的每一轮（\(j=r_0,\cdots,r_0+r_1-1\)）：声明 \(X,Y,Z\) 型变量，用规则 1–13 刻画区分器，令 KW 的值为 \(d\)；
- 对 \(E_2\) 的每一轮（\(l=r_0+r_1,\cdots,r_0+r_1+r_2-1\)）：声明 \(W\) 型变量，用规则 14–17 加前向确定性约束；
- 声明 SK 型变量，用规则 23 加约束，设上界 UpBound；
- 用 STP 运行，根据结果中的 SK 型变量得到需要猜测的密钥；
- 用密钥桥接 (key bridging) 技术缩减猜测量，输出 Guess_Key。
如果缩减后需要猜测的密钥字数小于算法的密钥字数，就认为这个密钥恢复是有效的。
习题 2.8
用本节的模型重新审视第六章的 4 轮 Mini-AES 区分器 \(\mathcal X_0[0]\to\Delta\mathcal X_4[0]\)：哪些位置的 \(Z\) 型变量为 \(1\)？度数 \(d\) 是多少？
解
前向差分（\(X\) 型）：从 \(X_0[0]\) 一个活跃半字节出发，第 1 轮后第一列活跃，第 2 轮后全部活跃，之后一直全部活跃。后向确定性（\(Y\) 型）：从 \(X_4[0]\) 往回推，它依赖第 4 轮 MC 前同一列的 \(X_3^S\) 的两个半字节，即 \(X_3[0]\)、\(X_3[3]\)；再往回，\(X_3[0]\) 与 \(X_3[3]\) 合起来依赖 \(X_2\) 的全部 4 个半字节；\(X_2\) 的 4 个依赖 \(X_1\) 的全部。
\(Z=X\wedge Y\)，S 盒输入位置上为 \(1\) 的有：\(X_1\) 中前向活跃且后向需要的 \(X_1[0]\)、\(X_1[1]\)（2 个），\(X_2\) 的 4 个，\(X_3[0]\)、\(X_3[3]\)（2 个），共 8 个半字节，即 \(d=8\)。这正对应第六章中的 \(\mathcal V'=c_0\Vert c_1\Vert c_2\Vert c_3\Vert c_4\Vert c_5\Vert K_3[0]\Vert K_3[3]\)：\(c_0,c_1\) 是 \(X_1[0],X_1[1]\) 的“偏移”，\(c_2,\cdots,c_5\) 是 \(X_2\) 的 4 个，\(K_3[0],K_3[3]\) 是 \(X_3\) 的 2 个，共 \(8\times4=32\) 比特，与第六章的 \(2^{32}\) 一致。
参考：王美琴主编，《密码分析学》，科学出版社，2024，第 9 章。
完
评论