Semenov, Alexander and Otpuschennikov, Ilya and Gribanova, Irina and Zaikin, Oleg and Kochemazov, Stepan - Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems

lmcs:4525 - Logical Methods in Computer Science, March 2, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:29)2020
Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems

Authors: Semenov, Alexander and Otpuschennikov, Ilya and Gribanova, Irina and Zaikin, Oleg and Kochemazov, Stepan

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.


Volume: Volume 16, Issue 1
Published on: March 2, 2020
Submitted on: May 23, 2018
Keywords: Computer Science - Logic in Computer Science,Computer Science - Artificial Intelligence,Computer Science - Cryptography and Security


Share

Consultation statistics

This page has been seen 227 times.
This article's PDF has been downloaded 346 times.