Extending SAT Solvers to Cryptographic Problems

2009 | Mate Soos, Karsten Nohl, Claude Castelluccia – University of Virginia

Cryptography ensures the confidentiality and authenticity of information but often relies on unproven assumptions. SAT solvers are a powerful tool to test the hardness of certain problems and have successfully been used to test hardness assumptions. This paper extends a SAT solver to efficiently work on cryptographic problems. The paper further illustrates how SAT solvers process cryptographic functions using automatically generated visualizations, introduces techniques for simplifying the solving process by modifying cipher representations, and demonstrates the feasibility of the approach by solving three stream ciphers.

To optimize a SAT solver for cryptographic problems, we extended the solver’s input language to support the XOR operation that is common in cryptography. To better understand the inner workings of the adapted solver and to identify bottlenecks, we visualize its execution. Finally, to improve the solving time significantly, we remove these bottlenecks by altering the function representation and by pre-parsing the resulting system of equations.

The main contribution of this paper is a new approach to solving cryptographic problems by adapting both the problem description and the solver synchronously instead of tweaking just one of them. Using these techniques, we were able to solve a well-researched stream cipher 26 times faster than was previously possible.

—————————————————-

Applications of SAT Solvers to Cryptanalysis of Hash Functions

August 2006 | Ilya Mironov, Lintao Zhang

Several standard cryptographic hash functions were broken in 2005. Some essential building blocks of these attacks lend themselves well to automation by encoding them as CNF formulas, which are within reach of modern SAT solvers. In this paper we demonstrate effectiveness of this approach. In particular, we are able to generate full collisions for MD4 and MD5 given only the differential path and applying a (minimally modified) off-the-shelf SAT solver. To the best of our knowledge, this is the first example of a SAT-solver-aided cryptanalysis of a non-trivial cryptographic primitive. We expect SAT solvers to find new applications as a validation and testing tool of practicing cryptanalysts.

—————————————————-

Money is Memory

1999 | Fabio Massacci, Published in: IJCAI’99 Proceedings of the 16th international joint conference on Artifical intelligence – Volume 1, Pages 290-295

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, AI 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 AI search algorithms, Walk-SAT by Kautz & Selman and Rel-SAT by Bayardo & 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.

—————————————————-

Money is Memory

October 1996 | Federal Reserve Bank of Minneapolis – Narayana R. Kocherlakota

This paper examines the sts of feasible allocations in a large class of economic environments in which commitment is impossible. The main proposition proves that any allocation that is feasible in an anvironment, the converse may or may not be true. Hence, from a technological point of view, money is equivalent to a primative form of memory.

—————————————————-

New Directions in Cryptography

November 1976 | Whitfield Diffie and Martin E. Hellman

Two kinds of contemporary developments in cryptography are examined. Widening applications of teleprocessing have given rise to a need for new types of cryptographic systems, which minimize the need for secure key distribution channels and supply the equivalent of a written signature. This paper suggests ways to solve these currently open problems. It also discusses how the theories of communication and computation are beginning to provide the tools to solve cryptographic problems of long standing.

—————————————————-

Back to University Archives