Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions
| Autor: | Catherine H. Gebotys, Jia Hui Liang, Vijay Ganesh, Saeed Nejati, Krzysztof Czarnecki |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
business.industry
Computer science Hash function 02 engineering and technology Solver 020202 computer hardware & architecture law.invention Symmetric-key algorithm law 0202 electrical engineering electronic engineering information engineering Cryptographic hash function Identity function 020201 artificial intelligence & image processing business Cryptanalysis Boolean satisfiability problem Algorithm Abstraction (linguistics) |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319723075 VSTTE |
| DOI: | 10.1007/978-3-319-72308-2_8 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|