Algebraic and Logic Solving Methods for Cryptanalysis
|
Abstract 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. In addition to that 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. Also in the present paper we compare the functionality of TRANSALG with that of similar software systems. 本文提出了构造离散函数的命题编码技术。它旨在用最先进的SAT求解器解决考虑函数的反演问题。我们以TRANSALG软件系统的形式实现了这项技术，并使用它来构造SAT编码来解决一些密码分析问题。通过将SAT求解器应用于这些编码，我们成功地反演了几个加密函数。特别地，我们使用TRANSALG产生的SAT编码来构造两个块的MD5碰撞族，其中前10个字节为零。除此之外，我们还为广为人知的A5/1密钥流生成器使用了TRANSALG编码来解决分布式计算环境中的几十个密码分析实例。此外，本文还将TRANSALG的功能与类似的软件系统进行了比较。 |
|
|
|
|
转换为SAT的软件transalg的网址： https://gitlab.com/transalg/transalg |
|
