通过 Cube-and-Conquer 逆推密码学哈希函数

MD4 和 MD5 是 1990 年代初提出的基础密码学哈希函数。MD4 由 48 步组成，对任意有限长度消息产生 128 位哈希。MD5 是 MD4 更安全的 64 步扩展。MD4 和 MD5 均易受实际碰撞攻击，但逆推它们（即给定哈希求消息）仍不现实。2007 年，MD4 的 39 步版本通过归约到 SAT 并应用 CDCL 求解器及所谓的 Dobbertin 约束而被逆推。对于 MD5，2012 年其 28 步版本在未添加任何额外约束的情况下通过 CDCL 求解器针对一个指定哈希被逆推。在本研究中，应用 Cube-and-Conquer（CDCL 与 lookahead 的结合）来逆推降步版本的 MD4 和 MD5。为此提出两种算法。第一种通过逐步修改 Dobbertin 约束来生成 MD4 的逆问题。第二种算法以不同截断阈值尝试 Cube-and-Conquer 的 cubing 阶段，以找到 conquer 阶段运行时间估计最小的那个。该算法以两种模式运行：(i) 估计给定命题布尔公式的硬度；(ii) 对给定可满足命题布尔公式的不完全 SAT 求解。第一种算法专注于逆推降步 MD4，而第二种算法不限定领域，因此适用于多种难 SAT 实例类。本研究中，40、41、42 和 43 步 MD4 首次通过第一种算法及第二种算法的估计模式被逆推。此外，28 步 MD5 通过第二种算法的不完全 SAT 求解模式针对四个哈希被逆推。其中三个哈希为首次实现。