Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions
Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions
复制标题
用于反转加密哈希函数的自适应重启和基于 CEGAR 的求解器
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Vijay Ganesh
中科院分区：
文献类型：
--
作者：
Saeed Nejati;J. Liang;C. Gebotys;K. Czarnecki;Vijay Ganesh
SAT求解器越来越多地用于散列函数和对称加密方案的密码分析。受这种趋势的启发，我们提出了MapleCrypt，这是一个基于SAT求解器的密码分析工具，用于反转哈希函数。我们将固定目标的哈希函数求逆问题简化为布尔逻辑的可满足性问题，并使用MapleCrypt为这些目标构造原像。MapleCrypt有两个关键特性，即基于多臂强盗的自适应重启（MABR）策略和反例引导的抽象细化（CEGAR）技术。MABR技术使用强化学习在求解器运行期间自适应地在不同的重启策略之间进行选择。CEGAR技术抽象出输入哈希函数的某些步骤，用身份函数代替它们，并验证MapleCrypt构建的解决方案是否确实哈希到先前固定的目标。如果确定所产生的解是虚假的，则细化抽象，直到产生输入散列目标的正确逆。我们表明，由此产生的系统是更快的反相SHA-1哈希函数比国家的最先进的反相工具。
SAT solvers are increasingly being used for cryptanalysis of hash functions and symmetric encryption schemes. Inspired by this trend, we present MapleCrypt which is a SAT solver-based cryptanalysis tool for inverting hash functions. We reduce the hash function inversion problem for fixed targets into the satisfiability problem for Boolean logic, and use MapleCrypt to construct preimages for these targets. MapleCrypt has two key features, namely, a multi-armed bandit based adaptive restart (MABR) policy and a counterexample-guided abstraction refinement (CEGAR) technique. The MABR technique uses reinforcement learning to adaptively choose between different restart policies during the run of the solver. The CEGAR technique abstracts away certain steps of the input hash function, replacing them with the identity function, and verifies whether the solution constructed by MapleCrypt indeed hashes to the previously fixed targets. If it is determined that the solution produced is spurious, the abstraction is refined until a correct inversion to the input hash target is produced. We show that the resultant system is faster for inverting the SHA-1 hash function than state-of-the-art inversion tools.