salle A. Turing CE4
6 March 2012 - 15h00
Symbolic Methods for the Automatic Search of Attacks Against Some Block Ciphers
by Charles Bouillaguet from ENS
Abstract: The block cipher cryptanalyst usually faces the following problem: she may interact with a black box containing the block cipher instantiated with a secret random key, and her goal is, in most cases, to retrieve this secret key using less time than exhaustive search and asking less encryptions/decryptions to the black box than the whole codebook.
Several researchers had previously observed that the Advanced Encryption Standard (AES), the most widespread block cipher, had a relatively simple algebraic description over the field with 256 elements, because of its byte-oriented design. However, this property has not been harnessed by cryptanalysts to this day. In particular the (tempting) approach consisting in writing down the equations describing the AES, and trying to solve them directly using off-the-shelf tools such as SAT-solvers, has systematically failed to provide any result.
In this talk, I will present the results we obtained using a slightly different method. We have designed tools that take as input a system of AES-like equations, and that search for an efficient ad hoc solving procedure. The result of these tools is the source code of a solver that can only solve the input system, but which can in some cases be efficient (its complexity can be predicted accurately). This solver can then be compiled and run to find the actual solutions.
Our tools, which reason from the equations describing the AES (or similar looking symmetric primitives) are intrinsically symbolic, and they are inspired by standard tools from the field of automated deduction, such as the DPLL algorithm for SAT, the Knuth-Bendix completion algorithm, or the resolution algorithm for first-order logic.
These tools found, nearly automatically, the best known Low-Data-Complexity attacks on reduced versions of the AES, and the best known attack on the full versions of AES-derived primitives, such as the Message Authentication code Pelican-MAC, and the stream cipher LEX.
Slides of the Presentation.
