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

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 & Need­ ham, 1996; G 10, 1996; OECD, 1998].

Yet security depends heavily on the strength of crypto­ graphic algorithms: security protocols which have been for­ mally 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, 1998].

*Supported by CNR fellowship 201-15-9. This work has been partly supported by AS!, CNR and MURST grants. I would like to thank L. Carlucci Aiello, P. Liberatore, and L. Marraro for useful comments and discussions.

Search, although in different settings, has also been a prob­ lem at the heart of AI research for many years. Recently propositional search has received attention for a number of factors [Selman et al., 1997]:

First 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 be­ gan to develop and solve propositional encodings of interesting, real-world problems [ ... ] Between 1991 and 1996 the size of hard satisfiability prob­ lems grew from ones involving less than 100 vari­ ables 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 possi­ ble. In [Marraro & Massacci, 1999] it has been show that, by combining clever reverse engineering, advanced CAD minimization, and propositional simplification, it is possi­ ble to encode in propositional logic the properties of the U.S. Data Encryption Standard, DES for short, [NIST, 1997; Schneier, 1994]. An encoding whose size is within reach of current AI search techniques: the encoding of a crypto­ graphic search problem (finding a model is equivalent to find­ ing a key) for the commercial version of DES requires slightly more than 10,000 variables and 6 times many clauses.

Although DES is currently under review, it is still the most widely used cryptographic algorithm within banks, financial institutions, and governments. It is the algorithm on which cryptanalysts tested the final success of their techniques (see [Schneier, 1994] or Sect. 2 for further references). Even par­ tial successes with AI techniques can be relevant.

In this paper we claim that this problem should be one of the reference SAT-benchmarks. In particular, it gives the possibility of generating as many random instances as one wants and still each instance is as "real-world" as any instance that can be met in commercial cryptographic applications. It provides a neat answer to the last challenge for proposi­ tional reasoning and search proposed by Selman, Kautz and McAIIester [ 1997] at IJCAI-97.

To check the potential effectiveness of AI techniques on this problem, two state-of-the-art SAT solvers have been tested for cryptographic key search using the propositional encoding. The choices are Walk-SAT, a local search algo­ rithm proposed in [Selman et al., 1994] as an improvement of GSAT, and Rei-SAT, a combination of the traditional Davis­ Putnam Algorithm with back-jumping and learning proposed in [Bayardo & Schrag, 1997] to solve real-world problems.

In the experiments on the Data Encryption Standard, one shouldn't expect to be immediately competitive with twenty years of advanced cryptanalysis techniques, especially be­ cause AI Labs are not equally well funded to afford a spe­ cialized hardware machine of 250.000 USD or the exclusive use of a network of workstations for 50 days which have been used to break DES in the last years. Still, general purpose search algorithm using off-the-shelf hardware (Spares and Pentium II) can crack limited versions of DES without be­ ing told any problem-dependent information. Ad-hoc cryp~o­ graphic techniques are still better since the first success With the limited version of DES we can solve was obtained in 1982 [Andleman & Reeds, 1982] and modern cryptographic ap­ proaches [Biham & Shamir, 1991; Matsui, 1994a] obtain the same results with better scaling properties. Still , the result is promising and points out at weaknesses of AI search algo­ rithms that we need tackle to solve hard problems.

In the next section (§2) we introduce some basic prelim­ inaries on cryptography and the Data Encryption Standard. Then we discuss the features of the encoding (§3). This is followed by the experimental analysis with Walk-SAT (§4) and Rei-SAT (§5). Few lessons for SAT solvers we can learn (§6) and new challenges (§7) conclude the paper.

2 Cryptography and DES

To make the paper self-contained for the non-security expert we sketch some preliminaries about cryptography and DES (for an introduction see [Schneier, 1994]).

Following [Schneier, 1994], we denote vector of bits by P (the plaintext), C (the ciphertext), and K (the secret key). At an abstract level , a cryptographic algorithm is simply a function C = EK (P) that transforms a sequence of bits (the plaintext) into another sequence of bits (the ciphertext) with certain (desirable) properties by using some additional (pos­ sibly secret) bits K. To decrypt we use another function that maps back C into P using K (or its inverse).

The important property of the encryption algorithm is that security of the algorithm must reside in the (secret) key. If one does not know K, it must be difficult to recover P from C, even if the algorithm has been public for years. In the ideal case, the only way to recover the plaintext must be by brute force "generate-and-test" : try out all possible keys and see which yields an acceptable plaintext. The need to hinder brute force attacks has therefore generated hot debates on the minimum size of a key [Schneier, 1994].

Exhaustive search is not so impossible as it seems if one can use (and pay for) specialized hardware: last year a ma­ chine costing 250.000 USD broke the Data Encryption Stan­ dard finding a 56 bits key in 56 hours [DES Search, 1998a].

Search can be cut down if the cryptanalyst knows a suf-

'

'

ficient number of blocks of plaintext with the corresponding ciphertext (known plaintext attack). This is a reasonable hy­ pothesis: almost all messages and files have fixed parts. Us­ ing a network of 12 workstation and 2 47 (randomly gener­ ated) plaintexts, Matsui [ 1994a] broke DES in 50 days.

As the reader might now want to know how DES works, we start by saying that DES is a block cipher, which encipher blocks (sequences) of 64 bits into blocks of 64 bits using a key of 56 bits 1 · DES and almost all symmetric ciphers are built following an architecture which is due to Feistel and his group [Feistel et al., 1975]. After some initial preprocessing, the following operations are executed:

1. break the plaintext in two halves,
2. combine one half with the key using a clever function,
3. XOR the combination with the other half
4. swap the two parts.

These 4 operations constitutes a round and are repeated a suit­ able number of times. Figure 1 exemplifies the idea.

DES has 16 rounds which are almost identical except for the way in which the key is fed into the f function (Fig. 1): for each round a different subset of the 56 key bits is selected and combined with the input of the previous round. The strength of the cipher depends on the number of rounds and on f. Its design is, to quote Ron Rivest, "part art, part science".

As we have mentioned already, the basic way to break DES is by exhaustive search but there are other techniques.

Dlfterential cryptanalysis was introduced by Biham and Shamir [ 1991]. It assumes that the cryptanalyst can choose ciphertext and plaintext pairs presenting particular fixed dif­ ferences. Then, it analyzes the evolution of these differences through the rounds of DES. Using the differences resulting from ciphertexts, different probabilities are assigned to dif­ ferent keys. By analyzing a large number of ciphertext and plaintext pairs (2 47 for the commercial version), a key will emerge as the most probable. This attack is only practical for less than 12 rounds. After that, it requires too many resources.

1 The key is usually expressed as a 64 bits number, in which every eighth bit is a parity bit ignored by the algorithm.

Matsui's linear cryptanalysis [Matsui, 1994a; 1994b] works better. This method uses linear approximations (xor) to describe the behavior of the round function f (Fig. 1). By xoring together some plaintext bits with some ciphertext bits, one can get a bit that is the xor of some key bits. This is a lin­ ear approximation of a round that is true with a certain proba­ bility. Again, by analyzing a large number of plain/ciphertext pairs (2 43 are needed for DES at 16 rounds), it is possible to guess the value of some key bits with 80% success rate. A re­ finement of this method approximates the internal 14-round and then guesses the results of the first and last round. It can find 26 keybits and uses exhaustive search for the rest.

A key aspect of cryptanalytic attacks (beside brute force) is that they are probabilistic. No deterministic method is known.

3 DES as a SAT Problem

Recently, an encoding of the U.S. Data Encryption Standard in propositional logic has been proposed in [Marraro & Mas­ sacci, 1999]. Before discussing how the encoding can be used to generate random problems, we sketch its functioning:

• each bit of the ciphertext, the plaintext, and the key is encoded as a propositional variable;
• the operations corresponding to the round function f (Fig. 1) are transformed into boolean formulae and min­ imized off-line with CAD tools;
• then the encoding algorithm "runs" DES at the meta­ level, and generates formulae corresponding to each DES operation on the way;
• since the straightforward application of this method would generate a huge formula, clever optimizations are used so that some operations are encoded as formulae and some operations are computed.

For instance, operations corresponding to permutations of bits are not encoded as formulae; rather the propositional variables describing the inputs are permuted. Further details can be found in [Marraro & Massacci, 1999].

The outcome 2 of the algorithm is a formula t'(P, K, C) which represent the logical relations between the key bits K, the plaintext bits P and the ciphertext bits C.

In a traditional plaintext attack we know the value of some plaintext and ciphertext bits so, if we replace the variables by the corresponding truth value, we have a formula whose structure is shown in Fig. 2. The l(i are the key bits while the other variables Mf, Sf, Xf are introduced to denote in­ termediate results and make the formula simpler. We use the superscripts r to denote the results produced at the r-th round and the subscript i to the denote the i-th bit produced at corre­ sponding intermediate stage (i ranges from 1 to 64). Loosely speaking, and looking at Fig. 1, we may say that each X[ represents an output of the r-th round and thus an input of the r + 1-th round of the algorithm. The value lastr is the number of rounds of DES for which the encoding has been done. The actual formulae have more definitions to ease the subsequent (polynomial) translation into CNF.

2 The algorithm in [Marraro & Massacci, 1999] takes less than I sec (3rounds) up to 25 seconds (16 rounds) to generate the encoding. Memory requires a peak of 135M for the full 16 rounds.

Figure 2: The Encoding for a known-plaintext attack

Table 1, taken from [Marraro & Massacci, 1999], shows some quantitative data for the encoding of a single pair con­ stituted by a known block of plaintext and a block of cipher text, for an increasing number of rounds (R).

For random formulae, the ratio of cjv is an indicator of the hardness of the formula. In this case, it is not so. For instance, using the data of Table 1 for 3 rounds or more, we can see that if we use one block or an "infinite" number of blocks, the value of cjv changes by less than 4%. This would seem to imply that adding more blocks should not make the problem neither much easier nor much harder. As we shall see, the experimental results contradict this hypothesis.

In the introduction, it has been claimed that this encod­ ing can be used to combine the contrasting needs of using "real-world" problems (possibly with lot of structure) and of generating a huge number of instances which can only be (pseudo)randomly generated. It might solve the dilemma pointed out in [Bayardo & Schrag, 1997]:

Care must be taken when experimenting with real world instances because the number of instances available for experimentation is often limited

whereas [Crawford & Auton, 1996] noted that

[ ... ] random problems are readily available in any given size and virtually inexhaustible numbers. For example, ... [their experiments] required sev­ eral million problems and it is hard to imagine col­ lecting that many problems any other way.

How do we generate a random SAT problem based on cryptography? At first we generate a random key VK and a plaintext block vp (just vectors of 0/1). Then we use the cryptographic algorithm itself to get vc=EvK (vp ). Finally we substitute in t' (P, K, C) the corresponding boolean val­ ues vp and vc that we have so far generated. Then the pair (vK, t'(vp, K, vc)) is a solved instance of the SAT problem. Notice that t'(vp, K, vc) might contain other variables than K but the latter are the only independent variables. If we haven blocks of plaintext (and the corresponding ciphertext) we can constrain the search further by conjoining the corre­ sponding formulae /\7= 1 t'(v~, K, v~).

So we have encoded cryptographic key search, a known plaintext attack to DES, as a SAT problem. Since ciphers are designed to be hard to break, this will provide us with the hard solved instances asked for in [Cook and Mitchel, 1997]. We can generate generic instances by randomly generating both the plaintext and the ciphertext.

The main point here is that by changing the plaintext and the key we can generate an endless stream 3 of different solved instances either with the same solution or with different solu­ tions. At 16 rounds, it would be exactly identical to an actual plaintext and ciphertext used by a bank, financial institution or government department.

4 Walk-SAT on DES

The first tested algorithm is a local search one: Walk-SAT [Selman et al., 1994]. It is only briefly recalled:

• the algorithm starts from a random assignment;
• then it flips the value of some propositional variables (usually one) trying to increase the value of an objective function (here the number of satisfied clauses);
• when a local minimum is reached, the algorithm restart the search with another random assignment.

Variants of this basic approach include the possibility of mak­ ing random moves from time to time and of continuing the search after a local minimum by using a tabu-list 4 . For more details see [Selman et al., 1994; 1997].

Experiments were run on a Pentium II running Linux (with 64MB) and a Sun Spare running Solaris (with 64M) with qualitatively and quantitatively similar results. To generate an instance we simply follow the recipe above: generate ran­ domly a key (discarding weak keys [Schneier, 1994]) and then some hundred blocks of plaintext. For each plaintext block we generate the corresponding ciphertext and then sub­ stitute the value of the pair in the formula. An instance is finally created by conjoining the formulae corresponding to the desired number of plain/ciphertext pairs (or blocks).

The initial settings of Walk-SAT were the recommend standard: hill-climbing with some random perturbations. The performance improved by using a random flip every 16 moves and the final result is reported in Table 2. R denotes the num­ ber of rounds on which DES has been limited and B the num­ ber of blocks which have been conjoined to produce the in­ stance (to get the size of an instance, multiply the values of Table 1 for the number of blocks). Sec. is the average running time and Kbits tells on average how many bits of the solution found by Walk-SAT coincided with the known solution. For unsuccessful attempts we also report the lowest number of unsatisfied clauses found.

3 For DES we have 2 56 x 2 64 instances if we consider the encryp­ tion of binary data. If we restrict ourselves to ASCII plaintexts, the number of different plaintexts only shifts from 2 64 to 2 56 ·

4 A tabu-list is a list of variables which have just been flipped and which cannot be immediately re-flipped

Walk-SAT can crack DES up to 2 rounds, and compares favorably with the results of SATO and TABLEAU reported in [Marraro & Massacci, 1999]. At three rounds Walk-SAT cannot crack any instance, even with a number of flips hun­ dreds times the number of clauses and a few hundreds tries. Moreover, adding more constraints (blocks) makes the search harder and not easier.

Why doesn't Walk-SAT solve the problem well?

The first problem has been already pointed out in [Selman et al., 1997]: the difficulty of local search algorithms to run around dependent variables. Recall that here almost all vari­ ables are dependent. The dagsat approach proposed in [Kautz et al., 1997] might prove to be more successful.

The second problem is the presence of wide "rugged" plateaus at the bottom of the search space: the number of unsatisfied clauses goes quickly down from thousands to few tens per block and stays there, with Walk-SAT flipping (in vain) a lot of dependent variables and moving from a local minima to the next. The lowest number of bad clauses was decreased by re-engineering Walk-SAT as follows:

• the first time a local minimum is reached, its value is stored as a reference value and the search continues;
• after the search visited n local minima with value higher than the reference value, all keybits were randomly flipped (with a probability ~ all variables were flipped);
• each time a lower minimum was reached, n was reset and that minimum considered the new reference value;

The idea was to escape the plateaus by exploiting the domain knowledge that the keybits were the only independent vari­ ables. In this way, the search converges to a much lower value of bad clauses (usually from 40-100 bad clauses per block to less than 1 0), but we are still stuck there.

5 Rei-SAT on DES

The second algorithm is a systematic one: Rei-SAT from [Bayardo & Schrag, 1997]. It is a variant of the Davis-Putnam algorithm, enhanced with conflict directed back-jumping and learning. It works as follows:

• unit propagation is applied to the clause set;
• if no contradiction is found a new literal is selected and added either positively or negatively to the clause set;
• if a contradiction is found then the algorithm backtracks to the literal that caused the contradiction;
• the clause responsible for the contradiction is resolved with a clause representing the temporary assignment; the resolvent is thus learned as a reason to avoid the corre­ sponding assignment;
• the procedure is iterated until all literals have been as­ signed (SAT) or no backtrack is possible (UNSAT).

For more details see [Bayardo & Schrag, 1997].

The instance generation method, the architecture, and oper­ ating systems were the same used for Walk-SAT. Also in this case, the experiment started with the recommend standard: a small learning factor (4), using relevance-based learning.

Up to 2 rounds, Rei-SAT cracks DES only slightly faster than SATO and TABLEAU (see [Marraro & Massacci, 1999]) or Walk-SAT. However, it is the r ly algorithm which cracks three round of DES in less than ten minutes. Its performance is reported in Table 3. The success rate is omitted since either all instances could be solved or none could(-).

Other settings were tried: no learning at all and learning factors larger than 4. The analysis shows that learning is essential if we have few constraints but it might be skipped if enough constraints are around (Table 3). An intuitive ex­ planation could be that with few blocks the algorithm might split on dependent variables and then discover that this was not necessary. With many constraints, standard heuristics se­ lect almost only independent variables and therefore learning contribution to performance is diminished.

Note that the performance of the algorithm improves with the number of blocks composing the instance. Adding more constraints makes the search for the only (?) existing solu­ tion easier. This behavior is consistent with standard crypto­ graphic techniques [Biham & Shamir, 1991; Matsui, 1994a] where having more data improves the chances of success.

Given this promising results, the algorithm has been en­ gineered to accept larger formulae with more variables and tried on the full 16-round DES, also using 1, 2, and 4 blocks. The algorithm didn't return within 12 hours.

A small re-engineering of the algorithm was carried to ex­ ploit in a limited manner the knowledge of the domain. After a first selection of potential branching variables, a threshold is used in the original algorithm to reduce their number. The modified algorithm didn't check the threshold if the selected variable was a keybit. In this way the algorithm gives pref­ erences to dependent variable with very good properties or independent variables with medium properties. However, the running time of the algorithm didn't improved substantially.

6 Lessons for SAT Solvers

It is a promising result that SAT solvers can crack a limited version of DES without using any problem-dependent heuris­ tics but this is not enough. We want to solve the full DES.

The first temptation is then to dismiss the SAT solvers themselves: this problem has a non-clausal structure, so it has to be expected that CNF provers perform badly; the right tool should have been BDDs [Bryant, 1986]. Surprisingly, an extensive experimentation reported in [Ascione, 1999] shows that the BDDs cannot solve key search problems any better than SAT-based approaches.

The second conclusion might be that the problem is too constrained: at three rounds there is almost only one solu­ tion. This makes the problem harder for local search, but should make it easier for complete algorithms. Indeed, the very characteristics of DES with its avalanche effect (all key­ bits should affect all ciphertext bits, and a flip in the plain­ text should affect all ciphertext bits, etc.) should make this problem easy: if the value of few key bits is wrongly chosen, a cascade of unit propagations should immediately generate an inconsistency. This would implies that formulae encoding more rounds (and more defined variables) should be easier and not harder. Since this is not the case, it seems that with more rounds unit propagation is somehow hindered.

Finding an explanation (and a workaround) for this diffi­ culty is important because the structure of the encoding is common in many hard real problems: the natural formula­ tion of a problem is usually structured in layers, makes use of abbreviations and definitions, and often contains modulo2 arithmetics (xors). For instance see the parity bit problem mentioned in [Selman et al., 1997] and the IFIP benchmark for hardware verification.

If we look again at the structure of the encoding, we may notice that each round is separated by the next round by a level of xors and that most constraints are in form of xors: a large subpart of the problem is an affine problem, which should be polynomially solvable by Schaefer's theorem. It is precisely this affine subproblem that make the problem hard for current AI techniques. Look again at table 1: the problem becomes difficult as soon as xors start to appear.

In contrast, cryptographic techniques exploits this affine subproblem and even approximate the whole problem into an affine problem [Matsui, 1994a]. Therefore, to crack DES or similar real-word problem a SAT solver needs the ability to solve affine subproblems.

7 Conclusions and Future Challenges

In this paper we have seen an application of propositional reasoning and search to a key s.ecurity problem of industrial relevance. We have also discussed how this approach can op­ timally provide "real-world" problems where many instances can be randomly generated.

Thus we believe that the whole approach on encoding cryp­ tographic key search as propositional search can be a good an­ swer to the final challenge proposed in [Selman et al., 1997]:

Develop a generator for problem instances that have computational properties that are more simi­ lar to real world instances.

Moreover, the preliminary tests on using SAT-solvers to crack the Data Encryption Standard are promising, although SAT-solvers must be improved to meet the full challenge pro­ vided by this benchmark. Thus, a good conclusion of this pa­ per may just be the indication of the future challenges. They are listed in order of feasibility.

The first challenge is to find a key for the commercial 16 rounds Data Encryption Standard in less than 56 hours using off-the-shelf h/w and s/w but specialized search heuristics. This might be the simplest and immediately rewarding chal­ lenge, assuming that the 10,000 USD prize of RSA Security for breaking its DES challenges will be there in the year 2000.

Then we may wish to design SAT-solvers that work with every Feistel-type cipher with data independent rounds like DES. If we were able to cope with affine subproblems this would not be a big extension. Since the operations are data independent, a certain amount of preprocessing for the inter­ nal rounds could be done off-line.

The third challenge is to find efficient encodings into SAT of data-dependent Feistel-type ciphers like RC5 [Schneier, 1994 ]. A straightforward encoding is always possible: just translate the cipher into a circuit and this into propositional logic. Unfortunately this is already unworkable for DES.

Last but not least, we may wish to find efficient encod­ ings into propositional (or any) logic of public-key algorithms such as RSA. This challenge, firstly proposed in [Cook and Mitchel, 1997], might prove to be the hardest since number theory is fairly remote from propositional logic.

As for all real problems, there might also be a darker side: the final measure of success might well be the "privi lege" ( !?) of successful SAT algorithms being denied export licenses as dangerous weapons.