Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems

TL;DR

This paper introduces a new method and software tool for translating discrete functions into SAT problems, facilitating cryptanalysis and enabling state-of-the-art attacks on cryptographic functions.

Contribution

The paper presents a novel translation technology and the Transalg tool, specifically designed for cryptanalysis, with theoretical justification and practical applications demonstrating its effectiveness.

Findings

Transalg successfully reduces cryptanalysis problems to SAT.

Applied attacks using Transalg achieve state-of-the-art results.

Experimental data shows high efficiency with top SAT solvers.

Abstract

In the present paper, we propose a technology for translating algorithmic descriptions of discrete functions to SAT. The proposed technology is aimed at applications in algebraic cryptanalysis. We describe how cryptanalysis problems are reduced to SAT in such a way that it should be perceived as natural by the cryptographic community. In~the theoretical part of the paper we justify the main principles of general reduction to SAT for discrete functions from a class containing the majority of functions employed in cryptography. Then, we describe the Transalg software tool developed based on these principles with SAT-based cryptanalysis specifics in mind. We demonstrate the results of applications of Transalg to construction of a number of attacks on various cryptographic functions. Some of the corresponding attacks are state of the art. We compare the functional capabilities of the proposed tool with that of other domain-specific software tools which can be used to reduce cryptanalysis problems to SAT, and also with the CBMC system widely employed in symbolic verification. The paper also presents vast experimental data, obtained using the SAT solvers that took first places at the SAT competitions in the recent several years.