基于自适应重启与反例引导抽象精化的密码哈希函数求逆求解器
密码学与安全
2016-08-17 v1
摘要
SAT 求解器正越来越多地用于哈希函数和对称加密方案的密码分析。受此趋势启发，我们提出 MapleCrypt，一个基于 SAT 求解器的密码分析工具，用于求逆哈希函数。我们将固定目标的哈希函数求逆问题归约为布尔逻辑的可满足性问题，并使用 MapleCrypt 为这些目标构造原像。MapleCrypt 有两个关键特性，即基于多臂赌博机的自适应重启（MABR）策略和反例引导的抽象精化（CEGAR）技术。MABR 技术利用强化学习在求解器运行过程中自适应地选择不同的重启策略。CEGAR 技术将输入哈希函数的某些步骤抽象掉，代之以恒等函数，并验证 MapleCrypt 构造的解是否确实哈希到先前固定的目标。如果确定产生的解是虚假的，则精化抽象，直到产生对输入哈希目标的正确求逆。我们证明，所得系统在求逆 SHA-1 哈希函数方面比最先进的求逆工具更快。
引用
@article{arxiv.1608.04720,
title = {Adaptive Restart and CEGAR-based Solver for Inverting Cryptographic Hash Functions},
author = {Saeed Nejati and Jia Hui Liang and Vijay Ganesh and Catherine Gebotys and Krzysztof Czarnecki},
journal= {arXiv preprint arXiv:1608.04720},
year = {2016}
}