Encoding Cryptographic Functions to SAT Using Transalg System
In this paper we propose the technology for constructing propositional encodings of discrete functions. It is aimed at solving inversion problems of considered functions using state-of-the-art SAT solvers. We implemented this technology in the form of the software system called Transalg, and used it to construct SAT encodings for a number of cryptanalysis problems. By applying SAT solvers to these encodings we managed to invert several cryptographic functions. In particular, we used the SAT encodings produced by Transalg to construct the family of two-block MD5 collisions in which the first 10 bytes are zeros. Also we used Transalg encoding for the widely known A5/1 keystream generator to solve several dozen of its cryptanalysis instances in a distributed computing environment. In the paper we compare in detail the functionality of Transalg with that of similar software systems.
Code (1)
Tasks
CryptanalysisDistributed ComputingSimilar Papers 제목 키워드 기반
Transalg: a Tool for Translating Procedural Descriptions of Discrete Functions to SAT
In this paper we present the Transalg system, designed to produce SAT encodings for discrete functions, written as programs in a specific language. Translation of such programs to SAT is based on propositional encoding m…
TranslationTranslation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems
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 cryptanaly…
CryptanalysisTranslationA Systematic Study on the Design of Odd-Sized Highly Nonlinear Boolean Functions via Evolutionary Algorithms
This paper focuses on the problem of evolving Boolean functions of odd sizes with high nonlinearity, a property of cryptographic relevance. Despite its simple formulation, this problem turns out to be remarkably difficul…
Evolutionary AlgorithmsDegree is Important: On Evolving Homogeneous Boolean Functions
Boolean functions with good cryptographic properties like high nonlinearity and algebraic degree play an important in the security of stream and block ciphers. Such functions may be designed, for instance, by algebraic c…
Evolutionary AlgorithmsExploring the Cryptographic Limits of Transformer Networks
In recent work it has been shown that colluding AI agents can use steganographic methods to exchange malicious information. Whether a transformer can implement steganographic methods depends on what cryptographic functio…