基于SAT、SMT、MILP和CP的差分密码分析对比研究

# 基于SAT、SMT、MILP和CP的差分密码分析对比研究 ## 1. 差分密码分析基础 差分密码分析是一种统计密码分析技术，由Biham和Shamir于1990年首次提出，对许多密码原语（如分组密码、流密码或哈希函数）非常有效。该技术研究两个具有差异 $\Delta x$（通常使用异或操作）的输入，通过迭代操作传播到输出差异 $\Delta y$ 的情况。 ### 1.1 差分概率 对于向量布尔函数，给定输入/输出差异对的差分概率是指在所有具有该输入差异的可能输入对中，该输入/输出差异对出现的概率，用 $dpf(\Delta x \to \Delta y)$ 表示。由于分组密码输入对数量巨大，直接计算所有输入对的输出差异并构建差异分布表（DDT）是不可行的。 ### 1.2 差分轨迹 分组密码通常是迭代函数，由多个简单的轮函数 $f_i$ 组成。一个 $r$ 轮差分轨迹是一系列差异：$\Delta_0 \xrightarrow{f_0} \Delta_1 \xrightarrow{f_1} \cdots \to \Delta_{r - 1} \xrightarrow{f_{r - 1}} \Delta_r$，而差分是输入/输出差异对。整个复合原语的差分 $\Delta x \xrightarrow{f_0 \circ \cdots \circ f_{r - 1}} \Delta y$ 的概率等于所有以 $\Delta_0 = \Delta x$ 和 $\Delta_r = \Delta y$ 为起点和终点的差分特征的概率之和，而差分特征的概率通常计算为链中每个中间差分概率的乘积。 ## 2. 实验设置 ### 2.1 实验任务 本次实验主要考察以下三个任务： 1. **任务1**：搜索最优差分轨迹（包括简单和困难实例）。 2. **任务2**：枚举所有最优轨迹。 3. **任务3**：估计差分的概率。 ### 2.2 实验环境 所有测试均在以下配置的服务器上运行，且任何时候使用的线程数不超过一半： - CPU：2 x Intel(R) Xeon(R) Gold 6258R - 核心/线程数：2 × 28 核心/2 × 56 线程 - 基础/最大CPU频率：2.7 GHz / 4.0 GHz - 缓存：38.5 Mb - 内存：768GB @2933 MHz - 操作系统：Ubuntu 18.04.5 LTS ### 2.3 实验密码算法 考虑了多种密码算法，包括分组密码、置换和哈希函数，具体如下： - **分组密码**：Simon和Speck、Threefish、LEA、DES、Midori、PRESENT、TEA、XTEA。 - **置换**：Gift、Gimli、Keccak、Ascon、ChaCha、Xoodoo。 - **哈希函数**：SHA1、SHA - 224、SHA - 256、SHA - 384、SHA - 512、Blake、Blake2、MD5。 ## 3. 求解器选择 为了进行实验，针对不同的形式化方法选择了以下求解器： ### 3.1 SAT求解器 - CaDiCal (1.5.3) - CryptoMiniSat (5.11.4) - Glucose Syrup (4.1) - Kissat (3.0.0) - MathSAT (5.6.9) - Minisat (2.2.1) - Yices2 (2.6.4) 所有SAT求解器均使用默认参数和选项运行。 ### 3.2 SMT求解器 - MathSAT (5.6.9) - Yices2 (2.6.4) - Z3 (4.8.12) 同样，所有SMT求解器使用默认参数和选项，由于SMT模型需要SMT - LIB标准中的QF UF逻辑，因此排除了Boolector和STP。 ### 3.3 MILP求解器 - GLPK - Gurobi 原本考虑了SCIP，但由于MILP模型使用SageMath MILP模块提供的求解器接口编写，该接口不包括SCIP，因此未使用。 ### 3.4 CP求解器 - Chuffed - Gecode - OR - tools - Choco 模型使用MiniZinc语言编写，该语言与这些求解器进行接口。 #