Measuring the Effectiveness of SAT-Based Guess-and-Determine Attacks in Algebraic Cryptanalysis

This paper studies the problem of algebraic cryptanalysis where state-of-the-art SAT solvers are used to invert some cryptographic function. We define a new metric of the hardness of CNF formulas that encode the corresponding cryptanalysis problems. The introduced metric is similar to the well-known tree-like metrics used in the theory of propositional proofs. However, unlike the latter, the new metric can be effectively estimated in application to specific cryptographic functions. The corresponding approach combines the Monte Carlo method and metaheuristic black-box optimization algorithms. The proposed algorithms require a large amount of computational resources, and for their experimental evaluation we used a supercomputer. In the experiments, we applied the proposed metrics to construct estimations of guess-and-determine attacks on the compression function of the well-known MD4 cryptographic hash algorithm.