Alexander Semenov ; Ilya Otpuschennikov ; Irina Gribanova ; Oleg Zaikin ; Stepan Kochemazov - 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 ProblemsArticle

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

    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
    Accepted on: January 22, 2020
    Submitted on: May 23, 2018
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Artificial Intelligence,Computer Science - Cryptography and Security

    Consultation statistics

    This page has been seen 1350 times.
    This article's PDF has been downloaded 1226 times.