通过 Cube-and-Conquer 逆密码哈希函数
Inverting Cryptographic Hash Functions via Cube-and-Conquer
AI总结：
提出两种 Cube-and-Conquer 辅助算法，逐步修改 Dobbertin 约束并优化立方截断阈值，首次逆求 40–43 步 MD4，并对四个哈希逆求 28 步 MD5。
摘要：
MD4 和 MD5 是 20 世纪 90 年代初提出的基础密码哈希函数。MD4 由 48 步组成，给定任意有限长度的消息，会产生 128 位哈希。MD5 是 MD4 的更安全的 64 步扩展。MD4 和 MD5 都易受实际碰撞攻击，但逆求它们（即给定哈希寻找消息）仍然不现实。2007 年，通过归约为 SAT 并应用 CDCL 求解器以及所谓的 Dobbertin 约束，40 步版本的 MD4 被逆求。至于 MD5，2012 年其 28 步版本通过 CDCL 求解器针对一个指定哈希被逆求，且没有添加任何额外约束。本研究将 Cube-and-Conquer（CDCL 与前瞻的组合）应用于逆求步数缩减版本的 MD4 和 MD5。为此，提出了两种算法。第一种通过逐步修改 Dobbertin 约束来生成 MD4 的逆问题。第二种算法尝试使用不同截断阈值的 Cube-and-Conquer 的立方阶段，以寻找征服阶段运行时间估计最小的阈值。该算法以两种模式运行：（i）估计给定命题布尔公式的难度；（ii）对给定可满足命题布尔公式进行不完备 SAT 求解。第一种算法专注于逆求步数缩减的 MD4，而第二种算法不局限于特定领域，因此适用于多种类别的困难 SAT 实例。本研究通过第一种算法和第二种算法的估计模式，首次逆求了 40、41、42 和 43 步 MD4。此外，通过第二种算法的不完备 SAT 求解模式，针对四个哈希逆求了 28 步 MD5。其中三个哈希是首次完成。
英文摘要：
MD4 and MD5 are fundamental cryptographic hash functions proposed in the early 1990s. MD4 consists of 48 steps and produces a 128-bit hash given a message of arbitrary finite size. MD5 is a more secure 64-step extension of MD4. Both MD4 and MD5 are vulnerable to practical collision attacks, yet it is still not realistic to invert them, i.e., to find a message given a hash. In 2007, the 39-step version of MD4 was inverted by reducing to SAT and applying a CDCL solver along with the so-called Dobbertin's constraints. As for MD5, in 2012 its 28-step version was inverted via a CDCL solver for one specified hash without adding any extra constraints. In this study, Cube-and-Conquer (a combination of CDCL and lookahead) is applied to invert step-reduced versions of MD4 and MD5. For this purpose, two algorithms are proposed. The first one generates inverse problems for MD4 by gradually modifying the Dobbertin's constraints. The second algorithm tries the cubing phase of Cube-and-Conquer with different cutoff thresholds to find the one with the minimum runtime estimate of the conquer phase. This algorithm operates in two modes: (i) estimating the hardness of a given propositional Boolean formula; (ii) incomplete SAT solving of a given satisfiable propositional Boolean formula. While the first algorithm is focused on inverting step-reduced MD4, the second one is not area-specific and is therefore applicable to a variety of classes of hard SAT instances. In this study, 40-, 41-, 42-, and 43-step MD4 are inverted for the first time via the first algorithm and the estimating mode of the second algorithm. Also, 28-step MD5 is inverted for four hashes via the incomplete SAT solving mode of the second algorithm. For three hashes out of them, it is done for the first time.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
