Application of satisfiability problem solvers for assessing the strength of hash algorithms

This article presents a methodology for assessing the strength of cryptographic algorithms and provides experimental data obtained from studying the cryptographic strength of the developed hash function HBC-256 using modern satisfiability problem (SAT) solvers. Various SAT solvers implementing the conflict-driven clause learning (CDCL) algorithm, based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, were used to conduct the cryptanalysis of the HBC-256 hash function. The most effective was the parallel SAT solver Parkissat, and thus it was used for more in-depth research. A series of experiments were conducted to determine how resistant the HBC-256 hashing algorithm is to preimage attacks for one, two, three, and four rounds. For this purpose, four sets of files were prepared using special propositional encoding tools, each set including 30 files in the standard of center for discrete mathematics and theoretical computer sciences (DIMACS) format. These files contain Boolean formulas in conjunctive normal form (CNF), used as input for modern SAT solvers. To obtain more accurate time measurements, the same experiment was repeated multiple times, after which the average time was determined. The results of this study show that SAT solvers encounter significant difficulties when attempting to solve the preimage search problem for the full-round version of the HBC-256 hash function, even when only 30 bits of the original message are unknown.