SHA-256 Collision Attack with Programmatic SAT

密码哈希函数在确保数据安全方面起着至关重要的作用，可以从可变长度的输入生成固定长度的哈希值。由于经过20多年的深入审查后仍然具有强大的韧性，哈希函数SHA-256在数据安全方面是值得信赖的。其中一个关键特性是抗碰撞性，也就是说，找到两个具有相同哈希值的不同输入是不可行的。目前，最好的SHA-256碰撞攻击使用差分密码分析在简化版本的SHA-256中找到碰撞，这些版本被简化为较少的步骤，使得找到碰撞成为可能。 在本文中，我们使用可满足性（SAT）求解器作为工具来搜索步骤减少的SHA-256碰撞，并使用计算机代数系统（CAS）动态指导求解器，以便检测不一致性并推断出求解器无法自行检测到的信息。我们的混合SAT + CAS求解器明显优于纯SAT方法，使我们能够在步骤减少的SHA-256中找到更多步骤的碰撞。使用SAT + CAS，我们发现了一个使用修改的初始化向量的38步SHA-256碰撞，这是由Mendel、Nad和Schl\"affer的高度复杂的搜索工具首次发现的。相反，纯SAT方法只能找到不超过28步的碰撞。然而，我们的工作仅使用了SAT求解器CaDiCaL及其编程接口IPASIR-UP。

本论文旨在使用混合SAT和CAS求解器，在动态引导下搜索简化版本的SHA-256哈希函数的碰撞。研究人员试图通过这种方法来验证SHA-256的安全性是否仍然可靠。

本论文的关键思路是使用混合SAT和CAS求解器来搜索简化版本的SHA-256哈希函数的碰撞。与之前的研究不同的是，研究人员使用了动态引导和计算机代数系统来指导SAT求解器，从而提高了搜索效率。

论文使用了混合SAT和CAS求解器来搜索简化版本的SHA-256哈希函数的碰撞，并在38个步骤内找到了碰撞。论文还提出了动态引导和计算机代数系统的使用，以提高搜索效率。研究人员使用了开源的SAT求解器CaDiCaL和其程序接口IPASIR-UP。这项研究对于验证SHA-256的安全性具有重要意义。

在最近的相关研究中，Mendel、Nad和Schl"affer使用了高度复杂的搜索工具，发现了SHA-256的修改初始化向量的38个步骤的碰撞。然而，他们的方法需要大量的计算资源。另外，之前的研究也使用了SAT求解器来搜索SHA-256的碰撞，但是这些方法只能找到少于28个步骤的碰撞。