Encoding Cryptographic Functions to SAT Using Transalg System

TL;DR

This paper introduces Transalg, a system for encoding cryptographic functions into SAT problems, enabling the use of SAT solvers for cryptanalysis, demonstrated through successful inversion of MD5 collisions and A5/1 keystream instances.

Contribution

The paper presents Transalg, a novel software system for constructing SAT encodings of cryptographic functions, facilitating effective cryptanalysis using SAT solvers.

Findings

Successfully inverted MD5 collision instances using SAT encodings.

Solved multiple cryptanalysis problems of A5/1 keystream generator.

Demonstrated Transalg's advantages over similar systems.

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. 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.