クリズのBlog

Appearance

自动化密码分析工具 ​

一、背景与目标 ​

  • 差分密码分析（Differential Cryptanalysis, DC 和 线性密码分析（Linear Cryptanalysis, LC） 是两种经典攻击方法。
  • 核心任务：寻找高概率的差分路径（differential trail） 或 高相关性的线性路径（linear trail）。
  • 手动搜索困难 → 需要自动化工具辅助。

二、主流自动化建模方法 ​

1. MILP（混合整数线性规划）方法 ​

  • 基本思想：将密码组件（如S盒、线性层）的行为用线性不等式 + 整数变量建模，交由求解器（如 Gurobi、CPLEX）优化。
  • 适用问题：
    • 最小活跃S盒数量（#Active S-boxes）
    • 最优差分/线性路径搜索
    • 不可能差分、零相关线性等区分器构造
关键技术点： ​

  • AES 建模示例：

    • 变量：S[r,i,j] ∈ {0,1} 表示第 r 轮 (i,j) 位置的 S 盒是否活跃。
    • MixColumns 层利用分支数（branch number = 5）：输入+输出活跃字节 ≥ 5。
    • 目标函数：最小化所有 S[r,i,j] 之和。
    • 结果：4轮 AES 至少 25 个活跃 S 盒（验证宽轨迹策略）。

  • S盒的位级建模（用于比特导向密码，如 PRESENT、SIMON）：

    • 方法一：凸包法（Convex Hull
      • 将所有合法的 (输入差分, 输出差分) 对视为 ℝ⁸ 中的点。
      • 计算其凸包 → 得到一组线性不等式。
      • 缺点：不等式数量庞大（如 410 个），需贪心约简（如保留 25 个关键不等式）。
    • 方法二：逻辑法（Logical Computation）
      • 对每个不可能差分 (a → b)，构造一个不等式排除它。
      • 利用权重技巧：若 a = [0,1,1,0,...]，则定义 q_i = 1 if a_i=0 else -1，构造 ∑ q_i·x_i ≥ 1 - HW(a)。
      • 更直观，易于实现。

  • XOR 建模：

    • c = a ⊕ b 可用 4 个不等式表示：
      a + b - c ≥ 0
a - b + c ≥ 0
-a + b + c ≥ 0
-a - b - c ≥ -2

2. SAT/SMT（布尔可满足性）方法 ​

  • 基本思想：将密码结构转化为布尔公式（CNF 合取范式），用 SAT 求解器（如 CryptoMiniSAT）判断是否存在满足条件的输入。
  • S盒建模：
    • 对每个不可能差分 (in_diff, out_diff)，添加一个子句（clause） 排除该组合。
    • 例如：若 0110 ↛ 0100，则添加子句：
      x0 ∨ ¬x1 ∨ ¬x2 ∨ x3 ∨ y0 ∨ y1 ∨ ¬y2 ∨ y3
    • 可进一步用 QM 或 Espresso 算法 对 CNF 进行最小化（但受限于变量数 ≤16）。
  • XOR 建模：
    • c = a ⊕ b 的 CNF 为 4 个子句：
      (a ∨ b ∨ ¬c)
(a ∨ ¬b ∨ c)
(¬a ∨ b ∨ c)
(¬a ∨ ¬b ∨ ¬c)
  • 优势：对位操作天然友好；现代 SAT 求解器极高效。
  • 局限：难以直接处理“计数”（如“最多4个活跃S盒”），需用基数约束（cardinality constraints） 转换，代价较高。

三、MILP vs SAT 对比 ​

特性MILPSAT
擅长整数优化、计数约束位级逻辑、大规模布尔推理
变量类型整数/实数（常用 binary）布尔变量
求解器商业为主（Gurobi, CPLEX）开源为主（MiniSAT, CryptoMiniSAT）
S盒建模不等式系统CNF 子句
适用场景结构规整（如 AES）、需最小化目标比特导向密码（如 SIMON, PRESENT）

💡 实践中常结合两者：用 SAT 找路径，用 MILP 验证或优化。

四、其他应用 ​

MILP/SAT 还可用于：

  • 不可能差分分析
  • 零相关线性分析
  • 积分区分器（Division Property）
  • Boomerang 攻击
  • 中间相遇攻击（MitM）
  • Cube 攻击

五、局限性 ​

  • MILP：对复杂位操作建模繁琐；变量过多时求解慢。
  • SAT：难以表达“数值优化”；CNF 规模可能爆炸。
  • 两者都依赖精确建模，错误建模会导致结果无效。

✏️ 复习题与答案 ​

问题 1：为什么在 AES 的 MILP 模型中，MixColumns 层要用不等式 5·M[r,j] ≤ Σ输入活跃 + Σ输出活跃 ≤ 8·M[r,j]？ ​

答：

  • M[r,j] 是辅助二元变量，表示第 r 轮第 j 列是否“活跃”。
  • AES 的 MixColumns 具有分支数 5，即：若输入非零，则输入+输出的活跃字节数 ≥ 5。
  • 当该列为活跃（M=1）时，不等式变为 5 ≤ 活跃字节数 ≤ 8（合理范围）。
  • 当该列不活跃（M=0）时，强制输入和输出全为 0。
  • 这样既保证了密码学性质，又通过 M 变量控制逻辑开关，便于求解器处理。

问题 2：在 SAT 方法中，如何用一个子句排除 S 盒的不可能差分 0110 → 0100？ ​

答：

  • 输入差分比特：x0=0, x1=1, x2=1, x3=0
  • 输出差分比特：y0=0, y1=1, y2=0, y3=0
  • 要排除该组合，需确保：只要输入输出等于该值，子句为假；否则为真。
  • 构造子句：对每一位，若原值为 1，则取反；若为 0，则保留。
  • 得到子句：
    x0 ∨ ¬x1 ∨ ¬x2 ∨ x3 ∨ y0 ∨ ¬y1 ∨ y2 ∨ y3
  • 当且仅当 (x,y) = (0110,0100) 时，所有文字为假，子句为假 → 被排除。

问题 3：MILP 和 SAT 在建模 S 盒时的核心区别是什么？ ​

答：

  • MILP 将 S 盒的差分行为建模为一组线性不等式（如凸包或逻辑推导所得），变量为整数（通常是 0/1），目标是最小化/最大化某个线性函数。
  • SAT 将 S 盒建模为一组布尔子句（CNF），每个子句对应一个被禁止的输入-输出差分对，目标是判断是否存在满足所有子句的赋值。
  • 简言之：MILP 用“不等式约束 + 优化”，SAT 用“逻辑约束 + 可满足性判定”。

问题 4：为什么在分析比特导向密码（如 PRESENT）时，不能简单地把 S 盒当作“恒等映射”来建模活跃度？ ​

答：

  • 在 AES 等字节导向密码中，S 盒是双射且非线性扩散强，但活跃度传播可近似为“输入活跃 ⇨ 输出活跃”（即视为恒等）。
  • 但在 PRESENT 等4-bit S 盒的比特导向密码中：
    • S 盒可能将单比特差分扩散为多比特，也可能将多比特差分压缩为单比特。
    • 甚至存在不可能差分（如某些输入差分无法产生特定输出差分）。
  • 若简单视为恒等，会高估或低估实际差分概率，导致搜索出的路径无效。
  • 因此必须精确建模 S 盒的差分分布表（DDT），无论是用 MILP 不等式还是 SAT 子句。

CopyRight@ 2025 Klizz