Nicolas Courtois, a mathematician and senior lecturer in computer science at UCL, working with Daniel Hulme and Theodosis Mourouzis, has won the 2012 best paper award from the International Academy, Research, and Industry Association for their work on using SAT solvers to study various problems in algebra and circuit optimization. The research was funded by the European Commission under the FP7 project number 242497, “Resilient Infrastructure and Building Security (RIBS)” and by the UK Technology Strategy Board under project 9626-58525. The paper, Multiplicative Complexity and Solving Generalized Brent Equations with SAT Solvers, was presented at Computation Tools 2012, the third International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking, held in Nice, France in July.
SAT (short for “satisfiability”) solvers are algorithms used to analyse logical problems composed of multiple statements such as “A is true OR not-B is true or C is true” for the purpose of determining whether the whole system can be true – that is, whether all the statements it’s composed of can be satisfied. SAT solvers also are used to determine how to assign the variables to make the set of statements true. In 2007, Bard and Courtois realised they could be used to test the security of cryptographic functions and measure their complexity, and today they are important tools in cryptanalysis; they have already been used for a long time in other applications such as verifying hardware and software. In this particular paper, Courtois, Hulme, and Mourouzis focused on optimising S-boxes for industrial block ciphers; the paper reports the results of applying their methodology to the PRESENT and GOST block ciphers. Reducing the complexity and hardware cost of these ciphers is particularly important to build so-called secure implementations of cryptography. These are particularly costly because they need to protect against additional threats such as side-channel attacks, in which the attacker exploits additional information leaked from the physical system – for example, by using an oscilloscope to observe a smart card’s behaviour.
“It’s more a discovery than an invention,” says Courtois. “One of the amazing things SAT solvers can do is give you proof that something is not true.” The semiconductor industry provides one application of the work in this paper: these techniques promise to provide a way to test whether a circuit has been built with the greatest possible efficiency by proving that the chip design uses the smallest possible number of logic gates.
“You’ll get optimal designs and be able to prove they cannot be done better,” he says.
Classical cryptanalysis proceeds by finding approximations to the way a cipher works. Many successful academic attacks have been mounted using such techniques, but they rely on having a relatively large amount of data available for study. That works for large archives of stored data – such as, for example, the communications stored and kept by the Allies after World War II for later cryptanalysis. But in many real-world applications, it is more common to have only very small amounts of data.
“The more realistic scenario is that you’ll just have one or a few messages,” says Courtois. Bluetooth, for example, encrypts only 1,500 bits with a single key. “Most attacks are useless because they won’t work with this quantity of data.” Algebraic cryptanalysis, which he explained in New Frontier in Symmetric Cryptanalysis, an invited talk at Indocrypt 2008, by contrast, is one of the few techniques that can be hoped to work in such difficult situations.
The downside is that algebraic cryptanalysis is computationally very expensive; it is slow and requires the kind of computing power available only to governments, and is sometimes criticised on that basis. Because of that, “On the surface, you might think algebraic cryptanalysis is not the best way to break something. But it may be the only practical way because you don’t have the data. Sometimes it’s the only option.”
Nicolas Courtois has a long history as a leader in the field of cryptography, with more than 50 published papers and 4,000 citations, as well as eight patents on practical cryptology and smart cards. His research focuses on three main areas: cryptanalysis; industrial cryptography, including secure hardware devices, anti-cloning, anti-tampering, and dedicated cryptography; and automated problem solving. He has also published in the field of abstract mathematics, such as his 2011 paper with Gregory V. Bard and Daniel Hulme, A New General-Purpose Method to Multiply 3×3 Matrices Using Only 23 Multiplications.
One of his best-known targets was Mifare, the cipher used in London Transport’s Oyster cards; the same chip is also used in building access systems and transport systems in many other countries. He estimates that his attack broke more than 1 billion smart cards, many of which are still in use even though Transport for London upgraded the technology a year after the attack was published; cards issued since December 2010 are no longer vulnerable.
In 2008, also with Gregory V. Bard and David Wagner, he published the first successful algebraic attack in history on a full round real-life block cipher. It was also the fastest attack ever found on the target cipher, KeeLoq, Algebraic and Slide Attacks on KeeLoq, presented at Fast Software Encryption. KeeLoq, for which the designer was paid $10 million, was kept secret for many years. It is used in remote keyless entry systems, particularly in the automotive industry – and Courtois’ work proved it was severely flawed. “It’s still used,” he says. “Millions of people are affected by this result.”
In 2012, he published Security Evaluation of GOST 28147-89 in View of International Standardisation, a paper examining the Russian national encryption standard, in use since the 1970s. Until 2010 GOST had not been successfully attacked – and it was known to be up to ten times more efficient when implemented in silicon than the prevailing standard, AES. If GOST were just as trustworthy, large sums of money could be saved in the semiconductor industry (which embeds AES in chips) by switching. As Courtois’ paper recounts, however, once GOST was submitted to the International Standards Organisation for certification, the international cryptography community examined it more closely. Many successful attacks have since been found.
Courtois goes on to propose a new paradigm for symmetric cryptanalysis that he calls “algebraic complexity reduction”, which makes it possible to reduce the security of a very complex cipher to that of a simpler cipher, and neatly splits the work of the cryptanalyst into two independent tasks. Cryptanalysts, he argues, need to begin to specialise. “Modern cryptanalysis requires more and more.”