论文标题
通过Cube and-Conquer颠倒加密哈希功能
Inverting Cryptographic Hash Functions via Cube-and-Conquer
论文作者
论文摘要
MD4和MD5是1990年代初提出的基本加密哈希功能。 MD4由48个步骤组成，并产生一个128位哈希，给出了任意有限大小的信息。 MD5是MD4的更安全的64步扩展。 MD4和MD5都容易受到实际碰撞攻击的攻击，但是倒转它们仍然不现实，即找到给定的消息。在2007年，MD4的39步版本通过还原和应用CDCL求解器以及所谓的Dobbertin的约束来倒置。至于MD5，在2012年，其28步版本是通过CDCL求解器以指定的哈希倒置的，而无需添加任何额外的约束。在这项研究中，将立方体固定（CDCL和LookAhead的组合）应用于倒入MD4和MD5的逐步减少版本。为此，提出了两种算法。第一个通过逐渐修改多伯丁的约束来为MD4产生反问题。第二种算法尝试具有不同截止阈值的立方体和串扰阶段，以找到具有征服阶段最小运行时估计值的插入阶段。该算法以两种模式运行：（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.
