SAT-based preimage attacks on SHA-1
SAT-based preimage attacks on SHA-1
复制标题
针对 SHA-1 的基于 SAT 的原像攻击
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Vegard Nossum
中科院分区：
文献类型：
--
作者：
Vegard Nossum
散列函数是重要的密码原语，它将任意长的消息映射到固定长度的消息摘要，以这样的方式：（1）很容易计算给定消息的消息摘要，而（2）反转散列过程（例如找到映射到特定消息摘要的消息）是困难的。对散列函数的一种攻击是一种算法，它仍然设法反转散列过程。散列函数用于例如认证、数字签名和密钥交换。在许多实际应用场景中使用的流行散列函数是安全散列算法（SHA-1）。在这篇论文中，我们调查了目前的艺术状态，在进行原像攻击对SHA-1使用SAT求解器，我们试图找出是否有任何改进的空间，无论是在编码或解决过程。我们运行了一系列的实验，使用SAT解算器上的编码降低难度版本的SHA-1。每个实验测试编码或求解过程的一个方面，例如确定是否存在最佳重启间隔或确定哪种分支启发式导致最佳平均求解时间。我们工作的一个重要部分是使用统计上合理的方法，即考虑样本大小和变化的假设检验。我们最重要的结果是一个新的32位模加法编码，它大大减少了SAT求解器找到解决方案所需的时间相比，以前已知的编码。其他结果包括这样一个事实，即通过将消息的位固定到某个点来减少搜索空间的绝对大小实际上会导致SAT求解器更难求解的实例。我们还确定了一些轻微的改进，所使用的参数的求解器MiniSat的算法，例如，相反的断言在文献中，我们发现，使用较长的重新启动间隔提高了求解器的运行时间。
Hash functions are important cryptographic primitives which map arbitrarily long messages to fixed-length message digests in such a way that: (1) it is easy to compute the message digest given a message, while (2) inverting the hashing process (e.g. finding a message that maps to a specific message digest) is hard. One attack against a hash function is an algorithm that nevertheless manages to invert the hashing process. Hash functions are used in e.g. authentication, digital signatures, and key exchange. A popular hash function used in many practical application scenarios is the Secure Hash Algorithm (SHA-1). In this thesis we investigate the current state of the art in carrying out preimage attacks against SHA-1 using SAT solvers, and we attempt to find out if there is any room for improvement in either the encoding or the solving processes. We run a series of experiments using SAT solvers on encodings of reduceddifficulty versions of SHA-1. Each experiment tests one aspect of the encoding or solving process, such as e.g. determining whether there exists an optimal restart interval or determining which branching heuristic leads to the best average solving time. An important part of our work is to use statistically sound methods, i.e. hypothesis tests which take sample size and variation into account. Our most important result is a new encoding of 32-bit modular addition which significantly reduces the time it takes the SAT solver to find a solution compared to previously known encodings. Other results include the fact that reducing the absolute size of the search space by fixing bits of the message up to a certain point actually results in an instance that is harder for the SAT solver to solve. We have also identified some slight improvements to the parameters used by the heuristics of the solver MiniSat; for example, contrary to assertions made in the literature, we find that using longer restart intervals improves the running time of the solver.
影响因子：
1.9
作者：
Zhou, XH;Gao, SJ;Hui, SL
通讯作者：
Hui, SL