Using Walk-SAT and Rel-SAT for Cryptographic Key Search

Sep 14, 2026

Uploaded by Jake

Computer security relies on the strength of cryptographic algorithms, making cryptographic key search a central challenge for governments and large organizations. This work promotes cryptographic key search as a benchmark for propositional reasoning and search, leveraging encodings that capture both real-world and random problem characteristics. Two state-of-the-art AI search methods, Walk-SAT and Rel-SAT, are evaluated on a propositional encoding of the Data Encryption Standard (DES), with results analyzed to guide improvements to SAT solvers. Future challenges are outlined.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages6

Reading Time15 min

AccessFree to download

Introduction

Encoding cryptographic key search as SAT

Walk-SAT and Rel-SAT for DES

Experimental evaluation and implications

Using Walk-SAT an d Rel-SAT for Cryptographic Key Search Fabio Massacci * Dip. di Informatica e Sistemistica Univ. di Roma I "La Sapienza"via Salaria 113,1-00198 Roma , Italy email: [massa cci@dis . uni roma l . it](massa cci@dis . uni roma l . it)[ ](massa cci@dis . uni roma l . it)url: [h t t p : / /www. di s . uni roma l . it /](h t t p : / /www. di s . uni roma l . it /) ~massa cc i Abstract Computer security depends heavily on the strength of cryptographic algorithms. Thus , cryptographic key search is often THE search problem for many governments and corporations. In the recent years , Al search techniques have achieved notable successes in solving "real world "problems. Following a recent result which showed that the properties of the U.S. Data Encryption Standard can be encoded in propositional logic , this paper advocates the use of cryptographic key search as a benchmark for propositional reasoning and search. Benchmarks based on the encoding of cryptographic algorithms optimally share the features of "real world " and random problems. In this paper, two state-of-the-art Al search algorithms , Walk-SAT by Kautz & Selman and RelSAT by Bayard o & Schrag , have been tested on the encoding of the Data Encryption Standard , to see whether they are up the task , and we discuss what lesson can be learned from the analysis on this benchmark to improve SAT solvers. New challenges in this field conclude the paper. 1 Introduction Securing one's data and communication from unauthorized access in large open networks such as the Internet is of the main issues for computer science today [Anderson & Needham , 1996 ; G10 , 1996 ; OECD , 19981. Yet security depends heavily on the strength of cryptographic algorithms: security protocols which have been formall y proved correct may be broken by the choice of a bad cipher Ryan & Schneider, 1998) . Thus , cryptographic key search is often the search problem for many government and large corporations ; and the ability of law enforcement officers to perform key search becomes the main concern behind the licensing of encryption technology [OECD , 19981. * Supported by CNR fellowship 201-15-9. This work has been partly supported by AS1 , CNR and MURST grants. 1 would like to thank L. Carlucci Aiello , F. Liberatore, and L. Marraro for useful comments and discussions. 290 CHALLENGE PAPERS Search , although in different settings , has also been a problem at the heart of Al research for many years. Recently propositional search has received attention for a number offactors [Selma n et al., 19971 : Eirst new algorithms were discovered .. . based on stochastic local search as well as systematic search [ | . Second , improvements in machine speed , memory size and implementations extended the range of the algorithms. Third , researchers began to develop and solve propositional encodings of interesting , real-world problems [ ] Between 1991 and 1996 the size of hard satisfiability problems grew from ones involving less than 100 variables to ones involving over 10,000 variables. Following a seminal proposal from [Cook and Mitchel , 1997], an application comes to one's mind: can we encode cryptographic key search as a SAT-problem so that AI search techniques can solve it'! A recent result in automated reasoning makes this possible. In [Marraro & Massacci , 19991 it has been show that , by combining clever reverse engineering , advanced CAD minimization , and propositional simplification , it is possible to encode in propositional logic the properties of the U.S. Data Encryption Standard , DES for short ,[NIST , 1997 ; Schneicr, 1994] . An encoding whose size is within reach of current Al search techniques: the encoding of a cryptographic search problem (finding a model is equivalent to finding a key) for the commercial version of DES requires slightly more than 10,000 variable s and 6 times many clauses. Although DES is currently under review , it is still the mos

FAQs

Why is cryptographic key search important in computer security?

Cryptographic key search is often the main search problem because breaking communication security depends on the cipher’s strength.

How does the paper use propositional logic to model cryptographic key search?

It encodes properties of the Data Encryption Standard so that finding a model corresponds to finding a key, turning key search into a SAT problem.

Which AI search algorithms are tested, and on what target?

The paper tests Walk-SAT and Rel-SAT on the propositional encoding of the Data Encryption Standard (DES).

Sep 14, 2026

Uploaded by Jake

Using Walk-SAT and Rel-SAT for Cryptographic Key Search_Page 1

Open in WPS to view all 6 pages