Encoding Hash Functions as a SAT Problem
Encoding Hash Functions as a SAT Problem
复制标题
将哈希函数编码为 SAT 问题
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
M. Krajecki
中科院分区：
文献类型：
--
作者：
F. Legendre;Gilles Dequen;M. Krajecki
可饱和性问题是数理逻辑和计算理论中的一个核心问题。在过去的几年里，进步已经导致它成为一个伟大的和有竞争力的方法，以实际解决广泛的工业和学术问题。因此，当前的SAT求解能力允许命题形式主义成为解决密码学问题的有趣替代方案，特别是引入了一个称为逻辑密码分析的新领域[15]。本文论述了原始应用的SAT问题编码著名的MD？而SHA？散列函数算法中的一个通用DIMACS公式。由于加密哈希函数是现代密码学的核心元素，我们选择对这些函数的逆进行专门的攻击来验证我们的建模。这种攻击的行为就像一个逆向工程的过程中，由于国家的最先进的SAT求解器实现削弱的第二原像MD？而SHA？因此，我们提出了我们的建模和改进的最佳实用的攻击步骤减少MD4，MD5和SHA？反转，分别高达39，28和23个中断步骤。最后，我们的结果进行了简要的分析，可以给一个想法的逻辑密码分析和散列函数。
The SATisfiability Problem is a core problem in mathematical logic and computing theory. In the last years, progresses have led it to be a great and competitive approach to practically solve a wide range of industrial and academic problems. Thus, the current SAT solving capacity allows the propositional formalism to be an interesting alternative to tackle cryptographic problems, and particularly introduced a new field called logical cryptanalysis [15]. This paper deals with an original application of the SAT problem to encode the well-known MD? and SHA? hash functions algorithm in a generic DIMACS formula. As cryptographic hash functions are central elements in modern cryptography we choose to validate our modelisation with a dedicated attack on the inversion of these functions. This attack behaves like a reverse-engineering process, thanks to a state of the art SAT solver achieving a weakening of the second preimage of MD? and SHA?. As a result, we present our modelisation and an improvement of the current limit of best practical attacks on step-reduced MD4, MD5 and SHA? inversions, respectively up to 39, 28 and 23 broken steps. Finally, a brief analyse of our results allows to give an idea about logical cryptanalysis and hash functions.