The Dolev-Yao Model and Formal Verification

The topic of the first study group of the new year was cryptographic protocol verification. Anna-Lisa and Peter were tasked with introducing the Dolev-Yao model and an introduction to some of the tools used to verify some of the properties of cryptographic protocols.

The well known paper of Dolev and Yao [pdf] provided a simple model for verification, and many of the main principles are still used today. The original motivation for the paper was to verify public key protocols against active attackers with considerable power. In their framework the following assumptions are made:

1. The underlying public key system is 'perfectly secure'

• one-way functions are unbreakable
• public directory is secure and cannot be tampered with
• everyone has access to all E_X
• only X knows D_X

2. Adversary has complete control over the entire network

• acts as a legitimate user, and can obtain any message from any party
• can initiate the protocol with any party, and can be a receiver to any party in the network

3. Concurrent executions of the protocol can occur

The model has the following features, which can be viewed as either benefits or restrictions depending on what you are trying to do:

• It is simple to describe protocols in this model
• Adversary has unlimited power, so although this is a conservative approach this may not be realistic
• Protocols have a 'black-box' nature, which means that linking individual protocols with others is extremely difficult

As an example Peter introduced the Needham-Schroeder protocol [pdf], which is used to establish a shared secret between two parties, A and B. This example shows the motivation for using verification tools to find attacks. The protocol runs as follows:

• A → B : {N_A, A}_B
• B → A : {N_A, N_B}_A
• A → B : {N_B}_B

In the first step, A creates a nonce N_A and encrypts it, along with B's identity, under the public key of B. Party B then creates its own nonce N_B, and sends it along with A's nonce, encrypted under A's public key, back to A. The final step is to verify the exchanges. In 1996 Lowe presented a simple man-in-the-middle attack [pdf] on this protocol and an amendment which fixes the vulnerability. The attack involves an impostor (I) who convinces B that they are in fact communicating with party A. We write I(A) to indicate I posing as A. The attack runs as follows:

• A → I : {N_A, A}_I
• I(A) → B : {N_A, A}_B
• B → I(A) : {N_A, N_B}_A
• I → A : {N_A, N_B}_A
• A → I : {N_B}_I
• I(A) → B : {N_B, A}_B

At the final step, B thinks he has established a secret with A. The fix suggested by Lowe involves changing the B → A : {N_A, N_B}_A in the protocol, adding in an identity check: B → A : {N_A, N_B, B}_A.

The Dolev-Yao paper covers cascade protocols, in which the only operations allowed on messages are encryption and decryption, and thus D_XE_X = E_XD_X = id. Note that textbook RSA satisfies this property, but in practice no real systems do. It is however a useful and simple class of protocols that can be formally verified. In this model, we have two parties A and B and n functions f₁,...,f_n such that at the start of the protocol, A knows message M, f₁ is applied to M, for even i the functions f_i are applied by B and for odd i the functions f_i are applied by A. An adversary Z has all of the f_i, E_X for all users X, D_Z and f₁(M). The protocol is said to be insecure if Z can construct a function g where g ⋅ f₁ = id.

Note that in a Diffie-Hellman key exchange procedure modified for this framework we have f₁ = E_B ⋅ D_A and f₂ = E_A ⋅ D_B, an adversary can simply set g = f₂ to prove the protocol insecure. Although this is a trivial example, it should indicate how these processes work for more complex systems.

The Dolev-Yao paper also includes so-called Name-Stamp protocols that include identities of the parties, and explains how the verification process works in this setting. The paper includes proofs that verification of both name-stamp protocols and cascade protocols run in polynomial time.

Next it was Anna-Lisa's turn to discuss some of the ideas behind ProVerif, introduced by Bruno Blanchet in 2008 [pdf], a tool that is used to check security properties such as secrecy and authenticity.

The problem of verifying the security of a protocol is undecidable in general, and tools like ProVerif aim to provide answers wherever possible. Some source of the undecidability is the fact that an unlimited number of sessions can occur. To deal with these there are two approaches:

1. Consider some restriction, for example putting a bound on the number of sessions

• useful for finding attacks
• not able to prove correctness as attacks may be missed
• the analysis will always terminate

2. Over-approximations (as used in ProVerif)

• used to prove correctness
• could potentially find false attacks
• in some cases this will be non-terminating

informally, secrecy of a message holds if it is kept secret from a Dolev-Yao adversary in the execution of the protocol. Authenticity means that if party A thinks that he is talking to B then this is in fact the case.

Much work has gone into formal verification in recent years, and ProVerif has been used in the following scenarios: Abadi and Blanchet verified a certified email protocol [pdf], then along with Fournet alaysed the Just Fast Keyring protocol [pdf] and Bhargavan et al. analyzed the TLS protocol [pdf] amongst others.

In ProVerif, protocols are defined by means of the pi-calculus, which is a formalism for describing concurrent systems. In the first stage, the protocol, pi-calculus and cryptographic primitives act as inputs to ProVerif along with the property that we wish to prove. Then an Automatic Translator turns these inputs into Horn clauses and Derivability Queries (an expression of the processes in an abstract form) and then a resolution is the output. This could be one of three outputs:

• Protocol is Correct
• There is a Potential Attack
• Does Not Terminate

The syntax of the pi-calculus can be found on page 6 of [pdf]. The abstraction into Horn clauses is crucial to the treatment of an unbounded number of sessions. Due to this abstraction, the tool is successful at proving security in many cases, but can fail on correct protocols.

Problems can occur in protocols where certain values that are initially secret become public after a length of time, the Horn clause model considers that this value can be reused at the beginning of the protocol, thus breaking the protocol.

VI-MSS workshop: Mathematical and Statistical Aspects of Cryptography

The Virtual Institute for Mathematical and Statistical Sciences (VI-MSS) hosted a workshop on the Mathematical and Statistical Aspects of Cryptography from the 12th to the 14th of January. It took place at the Indian Statistical Institute (ISI) in Kolkata, India. The main focus of the workshop was public key cryptography and this resulted in talks on a broad range of subjects such as lattices, elliptic curves, RSA and even braid cryptography. These talks ranged from practical (the bit-security of ECC and parallel hardware implementations for cryptanalysis) to theoretical (weakly-programmable random oracles and non-malleable commitments). A sizeable portion of the talks was about lattice-based cryptography and the disparity between theory and practice in this area was a general theme throughout the talks. This led to discussions on how to bridge this gap between theory and practice.

One good example of how to do this was illustrated by Damien Stehle in his talk on making NTRU as secure as worst-case problems over lattices (pdf). While this paper describes some changes to the NTRU cryptosystem that lead to theoretical proofs of security, Damien explained that the point was not that these changes should be made in practice, as the result will not be as efficient as desired. Rather, his point was that NTRU is already quite close to something that is provably secure, which should inspire confidence in the system. Additionally, some minor changes might improve the security while retaining efficiency.

Another interesting talk was given by Nadia Heninger on approximate divisors via lattices (pdf). The approximate integer common divisor problem was first posed by Howgrave-Graham (pdf), who also proposed an algorithm to solve it using lattice reduction. The problem arises when factoring numbers while having some information on one of the factors, which is of interest in the RSA setting, where the modulus can be factored if enough bits from one of the primes have leaked. Recently, a multivariate version of the problem was used as a hardness assumption for the construction of fully homomorphic encryption over the integers (pdf) and for an improved version of this construction (pdf). In the talk, Nadia showed how to extend Howgrave-Graham's approach to this multivariate version, the partial approximate common divisor problem. An issue that arises in the analysis of this problem is that current lattice reduction methods such as the LLL algorithm have approximation factors that are exponential in the dimension of the lattice. If these approximation factors were even slightly subexponential in the dimension, this would lead to a polynomial-time break of the fully homomorphic encryption schemes based on approximate common divisor problems. Nadia also showed an analogy of approximate common divisor problems for polynomials, which leads to applications in coding theory such as Reed-Solomon codes and Parvaresh-Vardy codes. An interesting open problem proposed in the talk was to extend the approach to number fields without having to perform lattice basis reduction on the canonical embedding. This would allow for more efficient attacks on fully homomorphic encryption over ideal lattices, as using the canonical embedding leads to a gigantic blowup of the exponential factor for lattice basis reduction methods in this case.

Turing Year

Yesterday was the first meeting in Cambridge in the sixth month workshop devoted to the legacy of Alan Turing. The talks were all introductory in nature; and rather than discuss here what they were about I thought it might be worth looking at Turing's legacy in Crypto somewhat.

The first thing the layman would think of is the second world war work on Enigma. In this Turing took the early work of the Polish cryptographers and helped design (with Welchman) the Bombe. This was an electro-mechanical machine used for finding wheel settings of the Enigma machines. It was not a computer! The key to breaking Enigma was that the Enigma machine never encrypted the same letter to itself, and if (for a particular setting) A encrypted to E, then E would encrypt to A. This last property is what made the Welchman diagonal board on the Bombe improve the Bombe's performance.

The layman also often confused Enigma with Tunny (a.k.a. Lorenz). The breaking of Lorenz was by far the most impressive bit of work done by Bletchley Park. The initial mathematics being done by Bill Tutte and the design of the resulting machine, Colossus, being the work of Tommy Flowers. However, Colossus was a real computer; it was digital, had input and output devices, an "ALU" and could be programmed (sort of). Thus whilst Turing may not have had a hand in the design of Colossus one can see that Colossus follows on from Turing's early paper on the decision problem.

In fact it is Turing's work on the decision problem which has had the most lasting impact on cryptography. In the paper he wrote Turing imagined a computing machine (now called a Turing machine) which was able to perform any computational task. The key idea was that there was one machine, now called the Universal Turing Machine, which could be "programmed" to perform any specific computational task. This is quite revolutionary idea; it is the reason why you only need buy one computer and it can do word-processing, games, internet access etc. The computer is "general purpose". Compare this to your kitchen where you have a toaster for toasting, a kettle for boiling water, a stove for boiling saucepans, and an oven for baking.

Imagine if you needed to buy a different device for each computational task you wanted to do. For example one device to read books (a Kindle), one device to play games (an XBox), one device to listen to music (an iPod). Hmmm, we seem to be going backwards these days!!!

Anyway back to the plot. The Turing machine is not only important as it is basically what a modern computer is; it is also important as it models what an arbitrary computer can do. Thus in cryptography we always consider our adversaries to be Turing machines; or more specifically probabilistic Turing machines whose run-times are bounded by some polynomial function of the length of their input (a PPT, or Probabilistic Polynomial-time Turing machine).  I would say Turing's name is mentioned more often than any other name in cryptographic talks; even if it is just by the TLA of a PPT.

Finally, there is one other philosophical contribution Turing made to cryptography in my opinion. The "Turing Test" in Artificial Intelligence is about whether someone can tell the difference between a real human and a computer by simply asking questions via a remote link. In this test the computers goal is to simulate the human so that an observer is unable to tell the difference between a human and the simulator. The is exactly what we do in many security proofs in cryptography. For a specific algorithm (having access to some special bit of information or functions) we define a simulator (which does not have access to the information or functions). We can then argue that if someone cannot tell the difference between the simulator and the real algorithm, then the algorithm is "secure".

Anyway, welcome to the Turing Year of 2012

IMA Cryptography & Coding - Day 2

The invited talk on Day 2 of IMACC was given by Ivan Damgård on secure multiparty computation (MPC). The goal of MPC is to jointly compute some function on a number of players' secret inputs. Ivan began with a nice explanation of how to achieve this with information theoretic security. He described how MACs can be used to verify the computations of each player, thus achieving security against active adversaries.

The talk then went on to describe recent results concerning the case of a dishonest majority of adversaries. Clearly this scenario is very important to focus on if MPC schemes are to be deployed in the real world. Early efforts to obtain this level of security were very inefficient, but some recent innovations have proposed using a homomorphic encryption scheme to improve this. This was first suggested in Eurocrypt 2011 by Bendlin, Damgård, Orlandi and Zakarias (pdf). By dividing the computation into two phases ('offline' and 'online'), they manage to perform a secure multiplication in around 8ms. These results are improved upon in a recent paper by Damgård, Pastro, Smart and Zakarias (pdf), which reduces the complexity and storage requirements of the scheme even further. Multiparty computation is an active area of research in Bristol, and it was nice to see it represented in Oxford with Ivan's excellent talk.

One session that interested me in the afternoon was on cryptanalysis and security analysis. This began with Martin Albrecht presenting joint work with Kenny Paterson on breaking a recent IBE scheme of Chen et al. (pdf). The basic attack involved exploiting the relationship between the master secret key and the private keys for each identity that are generated from the master key. Specifically, each private key is given by a quadratic function in the master key components. So given enough of these keys, an attacker has a system of multivariate quadratic equations in the master key that can be solved using a Gröbner basis computation.
Whilst this attack was considered in the original paper, the authors severely underestimated the efficiency with which Gröbner bases can be computed. Apparently this problem is surprisingly common in the literature, and stems from using analysis of the XL algorithm to obtain security estimates, whereas in practice the F4 and F5 algorithms are far more efficient. Although in the original paper security of the scheme was proven to be based on the DHIES scheme, this attack does not allow you to break DHIES. The key flaw is that their proof assumes that a specific function can be modelled by a random oracle, when in fact the output of this function is dependent on the secret key. So the use of a random oracle here is completely inappropriate, and invalidates the security proof.

The third talk in the session, given by Julia Borghoff, followed in a similar vein, attacking the lightweight stream cipher A2U2. The attack also involved creating a system of multivariate quadratic equations and using Gröbner basis computations to solve this. Firstly an efficient chosen plaintext attack was presented, followed by a more complex 'guess and determine' attack requiring only a known plaintext. However, some doubts were raised afterwards as to how feasible this attack would be in practice due to the high number of Gröbner basis applications required.

In between these talks on cryptanalysis, our recent PhD graduate Steve Williams presented his work on the security analysis of the SSH key exchange protocol. Although the underlying application layer of SSH has been thoroughly analysed in the past, no-one had yet performed an analysis of the vital key exchange protocol used to initiate the shared secret. Since the initial messages transmitted in the protocol contain a signature, it is not possible to obtain indistinguishability of the key generated in this stage. So the security of this can only be shown to be one-way, which Steve successfully proves. A transformation is then applied to this shared key, and Steve went on to show that this transformation in fact means that the final keys generated in SSH are indistinguishable.

IMA Coding and Crypto, Day 1 Morning

This year is the 25th anniversary of the conference colloquially known as Cirencester. It is traditionally held every two years at the agricultural college in Cirencester. It's a rather remote location and it has the effect that in the evening everybody cozies up in the college bar with big wooden fire. A few years back I remember I kept having to climb a big mould of whatever just in order to get telephone reception.

Anyway, this year's Cirencester is not actually in Cirencester, instead it is in Oxford, at the Lady Margaret Hall. This college used to be women only, but these days it is mixed (just like Royal Holloway, University of London). It is located a bit north of the center, about 10-15 mins walk and the buildings are all rather new (certainly for Oxford college standards). So it's not quite as remote as the real Cirencester, but it is a decent emulation (including some of the agricultural whiffs that occassionally manage to make it into the lecture theatre).

The first talk of the conference was by David Nacchache who gave an invited talk consisting of three parts. The first part dealt with code obfuscation. The goal of code obfuscation is simple: you take a piece of code and modify it in such a way that it behaves exactly the same as the original piece, yet all other information about the original code is hidden. For instance, a programmer might want to hide the control flow of a problem, or a cryptographer might want to hide a key that is a fixed input to the program. Obfuscation is a rather hard problem cryptographically, rife with negative results. The main negative result is due to Barak et al., who showed that there exist programs that cannot be obfuscated at all: any obfuscation will invariably leak a predicate about the original. In his talk, Naccache explained programs of a much higher degree of unobfuscatability: any (functionally equivalent) obfuscation will necessarily leak the original code. The main tool of this remarkable result is the concept of Quines, that is programs that print themselves. While this may sound rather negative, Naccache also pointed out a positive, namely their transformation takes any program and turns it into a fully unobfuscatable one, which creates a potential mechanism for detecting forgeries of some original piece of code.

The second part was dedicated to identifying finger prints. While there are many algorithms for this already, most boil down to comparing a fingerprint found on a crime scene against a database, checking for a match one by one. These matches are quite costly and Naccache showed how one can use relatively lightweight statistical methods to precompute an ordering on the database that increases the probability of finding a hit sooner rather than later (thus reducing overall search time).

Finally, Naccache discussed the problem of figuring out the computation that was performed based on inputs and outputs only. In the past work had been done related to the partial extraction of an exponent based on the projective representation of a scalar multiple, here the focus was on arithmetic circuits over a finite field of small depth. As it was still work in progress, the details are left for later.

After a very short break, the first contributed talk was delivered by our very own Peter Scholl. I think it was his first conference presentation and he did a sterling job! The topic under investigation was improved key generation for Gentry's fully homomorphic encryption scheme. When Gentry proposed his breakthrough scheme, the efficiency left much to be desired and in fact, it was completely impractical to deploy the scheme for a realistic security setting. Much progress has been made in the mean time, but this progress does not always blend well: Gentry and Halevi presented a vastly improved key generation scheme and Smart and Vercauteren presented several significant improvements to other parts of the scheme, yet the Gentry-Halevi key generation sadly does not apply to the parameters Smart and Vercauteren need for their key ideas. In this work, Peter (in joint work with Nigel) adapted the ideas of the Gentry and Halevi to the Smart-Vercauteren setting. It turned out that by introducing several neat new techniques and optimizations, key generation suddenly becomes feasible. I would especially like to draw attention to one of the conclusions, namely that you really need to implement these more complicated schemes to see where the challenges are and what can be done about the bottlenecks. This point was also brought home in later talks, for instance the excellent invited talk by Ivan Damgaard and the inspiring talk by Mike Scott.

After Peter, Frederik Armknecht (fresh from presenting at Asiacrypt) gave a talk on constructing homomorphic encryption schemes from coding theory. The advantages of using coding theory are obvious: the computations involved are almost guaranteed to be simple, plus linear codes naturally allow one homomorphism naturally. The hope was that this simplicity could be leveraged to create an efficient scheme supporting both additions and multiplications. As it turns out, this is not as easy as one might hope for. The schemes presented by Armknecht still had some limitations that would reduce their overall useability. Chief amongst these were fairly strict restrictions on the number of ciphertexts allowed (which also implied a secret-key only setting) and a limitation on the number of multiplications that could be handled. Nonetheless, one can imagine that in some scenarios these scheme deliver exactly what is needed in a relative cheap and painful way.

HB+ and its variants

Today's study group, led by Luke and Gareth, was on the topic of HB+ and variants thereof, with particular focus on the following three papers:

• Efficient Authentication from Hard Learning Problems (Kiltz et al, Eurocrypt 2011) [pdf]
  

• Parallel and Concurrent Security of the HB and HB+ Protocols (Katz et al, Eurocrypt 2006) [pdf]
  

• HB#: Increasing the Security and Efficiency of HB+ (Gilbert et al, Eurocrypt 2008) [pdf]
  

The motivating problem for HB-related schemes is secure authentication for low-cost devices such as RFID tags, whose power and storage constraints necessitate lightweight protocols. The motivation for the original HB protocol (Hopper and Blum, Asiacrypt 2001) [pdf] was actually secure human-executable identification, performed using only such undemanding computations as dot products and XORs -- so, although their proposal does not fulfill all the desired security requirements, it is nevertheless an excellent starting point for developing (very) low complexity schemes.

HB authentication derives its security from the NP-hard 'Learning Parity with Noise' (LPN) problem, which corresponds to the task of decoding random linear codes:

• Let A be a (q × k) binary matrix; x a random k-bit vector; η ∈ (0,½) a (fixed) noise parameter; ν a random q-bit vector such that HW(ν) ≤ ηq. Given A, η, z = (Ax)⊕ν the LPN problem is to find a k-bit vector x's.t. HW((Ax')⊕z) ≤ ηq.

The basic HB protocol is as follows:

1. Tag and reader share a key x ∈ {0,1}ⁿ.
2. For rounds j = 1,...r:
1. Reader draws a^j ∈_R {0,1}ⁿ and sends to tag
2. Tag computes u^j = a^j · x and draws ε^j ∈_η {0,1}
3. Tag sends z^j = u^j ⊕ ε^j to reader
4. If z^j = a^j · x for a clear majority of j ∈ {1,...,r} then the reader accepts the tag as authentic.

This is clearly attractive as the only computations performed on the tag are bit-wise computable dot-products and single bit XORs. However, it turns out to be vulnerable to an active attack in which the adversary retrieves x bit-by-bit by sending challenges of the form a^j_k = 1, a^j_i = 0, i ≠ k, that is: (0,0,...,1,...0,0). Then z^j = x_k ⊕ ε^j so that the majority over r rounds will reveal x_k.

To resist the above attack Juels and Weis (Crypto 2005) [pdf] proposed HB+:

1. Tag and reader share two keys x, y ∈ {0,1}ⁿ.
2. For rounds j = 1,...r:
1. Tag draws b^j ∈_R {0,1}ⁿ and sends to reader
2. Reader draws a^j ∈_R {0,1}ⁿ and sends to tag
3. Tag computes u^j = (a^j · x) ⊕ (b^j · y) and draws ε^j ∈_η {0,1}
4. Tag sends z^j = u^j ⊕ ε^j to reader
5. If z^j = (a^j · x) ⊕ (b^j · y) for a clear majority of j ∈ {1,...,r} then the reader accepts the tag as authentic.

This is provably secure in the 'detection-based' adversarial model, and therefore no longer vulnerable to the active attack described above. However, several problems remain:

• The revised protocol introduces the problem of generating random vectors on the tag.
• The proof supposes that the rounds are performed sequentially and does not extend to a parallelised implementation (desirable as a strategy to reduce communication complexity).
• The false rejection rates (under the proposed acceptance thresholds) are very high -- as much as 44% for 80 rounds with a noise level of ¼. (See table 1 of (Gilbert et al, Eurocrypt 2008)).
• The adequacy of the adversarial model (which supposes the adversary can interact only with the tag before impersonating it to the reader) has been questioned.

In fact, HB+ is vulnerable to a man-in-the-middle attack in which the adversary is able to interact with the reader as well as the tag before attempting to impersonate (Gilbert et al, 2005) [pdf]. We discussed the fact that such an attack poses a material threat: whilst it would be difficult to carry out an opportunistic MIM on a nearby tag carried by a passer-by, an attacker in possession of a tag with incentive to clone it could very well use a reader of his own to do so, with comparatively unconstrained time and resources.

The same authors solve this problem and also answer to the parallelisation challenge with RANDOM-HB#, in which the secrets become (n_X × m) and (n_Y × m) binary vectors X and Y rather than n_X- and n_Y-bit vectors x and y, and the protocol operates (in one go) in matrix form rather than round-by-round, so that the final verification consists of the comparison of two m-bit vectors a · X ⊕ b · Y and z. This adaptation is secure against the above MIM (known as GRS-MIM after the authors), as well as having a much smaller false rejection rate. However, when the adversary is afforded more powers (i.e. he is allowed to modify more of the elements of the protocol) another MIM attack has been found -- though with increased complexity.

The last paper we looked at was concerned with constructing MACs based on the hardness of LPN (Kiltz et al, Eurocrypt 2011). The protocol can be informally described as follows:

1. Tag and reader share a key x ∈ {0,1}ⁿ.
2. Reader selects a random subset of bits of x and sends to the tag.
3. Tag computes a noisy inner product z of the selected bits and sends to the reader.
4. Reader verifies that z matches the inner product (without noise) 'most of the time'.

This acheives 2-round authentication with active security. The proof derives from the hardness of the subspace LPN problem (Pietrzak 2010 [pdf]) and because it doesn't use rewinding technqiues it remains valid against quantum adversaries.

Single-sample DPA (aka horizontal DPA)

This week's study group covered 'old' papers by Colin Walter (big-mac attack) to current work of Mike where focus is to apply DPA techniques to a single trace. More specifically, we discussed the following papers:

• Colin D. Walter “Sliding Windows Succumbs to Big Mac Attack” [pdf]
• Colin D. Walter “Longer Keys May Facilitate Side Channel Attacks” [pdf]
• Jean-Christophe Courrège et al. “Simple Power Analysis on Exponentiation Revisited” [pdf]
• Werner Schindler and Kouichi Itoh “Exponent Blinding Does Not Always Lift (Partial) Spa Resistance to Higher-Level Security” [pdf]

Stefan kicked off the study group by explaining us why longer keys may facilitate Side Channels Attacks (SCAs). Common sense would suggest that longer keys should be used to provide more security. This is true for the mathematical strength of a cipher, however, Colin Walter shows in his work that for embedded RSA crypto-systems the increase in leaked data through longer keys in fact lowers security. We discussed two types of attacks, namely a timing and a power analysis attack, that may be possible from increasing the key length. The implementation under attack uses a variant of the binary "square-and-multiply" algorithm to compute the RSA exponentiation. As so often when trying to attack such implementations, the goal is to distinguish between squares and multiplications to extract secret key material.

One way to distinguish these two core operations is to look at timing variations that occur for computing the modular products. Typically, a form of Montgomery's modular multiplication (MMM) is used to compute these products. From a side-channel perspective, the interesting aspect of MMM is the fact that it includes a final conditional subtraction which reduces the output to less than the modulus. This final subtraction occurs with higher probability for squares than for multiplications and this forms a timing side-channel that can be exploited by an attacker that observes a number of exponentiations. The data leaked through this side-channel is proportional to the square of the key length and thus longer keys are being less safe. The simplest countermeasure to thwart this kind of attack is to use an unconditional subtraction and select the appropriate result afterwards.

The second attack that Stefan described exploits the power leakage of the internal hardware multiplier. For MMM a number of single precision multiplications need to be computed. The idea is here to fix one of the multiplier inputs while the second input is more or less random and then average the power traces over a number of multiplications. The power trace that we end up with is then dependent on the Hamming weight of the fixed operand. If we apply this technique to all chunks of a long integer multiplication we can build templates during pre-computation which we can then use during the actual exponentiation to guess which operation has been computed. The nice property of this attack is that we only need to collect a single power trace of an exponentiation to characterise the different operations plus mount the actual attack.

In the second part, Mike was talking a bit about the stuff he is doing at the moment. For example, on an ARM chip it is apparently easy to identify the occurrence of the different single precision multiplication operations in the power trace while executing an exponentiation. Using a horizontal DPA, the idea is to recover in each iteration the i-th operation (whether a square or multiplication has been executed) under the assumption that we have successfully recovered the first i − 1 operations. Next, an attacker makes a prediction (e.g., using the Hamming weight) of how the power consumption should look like for the two core operations. Depending on which of these two power profiles correlates best with the actual power trace reveals another operation of the exponentiation. Collecting one power trace of the device under attack is enough to mount such attack.

Mike also described another attack on the exponentiation that exploits some bias in the Hamming weight of the output of single precision multiplication and squaring operations. Basically, what is exploited in this attack is the fact that the second most least significant bit of a single precision squaring operations will always be zero. With this information we can build templates by characterising these squaring and multiplication operations to try to make a distinction between the operations. Mike reports that he had a 95% success rate in choosing the right operation using this technique. The advantages of this attack is that the bias is caused by the operation itself and it will remain there irrespective of the message input.

Finally, Mike briefly discussed some techniques to attack implementations that use exponent blinding as countermeasure.