Using Volunteer Computing for Mounting SAT-based Cryptographic Attacks

TL;DR

This paper introduces SAT@home, a volunteer computing project that applies SAT solving techniques to cryptanalysis, demonstrated through attacking the A5/1 keystream generator using distributed computational resources.

Contribution

The paper presents a novel approach combining volunteer computing with SAT-based cryptanalysis, including a new partitioning technique for solving cryptographic inversion problems.

Findings

Successful cryptanalysis of A5/1 keystream using volunteer computing

Development of a partitioning method based on Monte Carlo and optimization techniques

Demonstration of SAT solving as a practical tool for cryptographic analysis

Abstract

In this paper we describe the volunteer computing project SAT@home, developed and maintained by us. This project is aimed at solving hard instances of the Boolean satisfiability problem (SAT). We believe that this project can be a useful tool for computational study of inversion problems of some cryptographic functions. In particular we describe a series of experiments performed in SAT@home on the cryptanalysis of the widely known keystream generator A5/1. In all experiments we analyzed one known burst (114 bits) of keystream produced by A5/1. Before the cryptanalysis itself there is a stage on which the partitioning of the original problem to a family of subproblems is carried out. Each of subproblems should be easy enough so that it could be solved in relatively small amount of time by volunteer's PC. We construct such partitioning using the special technique based on the Monte Carlo method and discrete optimization algorithms for special predictive functions. Besides this in the paper we describe the technique for reducing inversion problems of cryptographic functions to SAT.