V Cortier

S Delaune

G Steel

chkEven(xk3)

Keywords: protocoles de sécurité, interface de programmation, ou exclusif, procédure de décision xk1, chkEven(xtype), y, xk2, chkEven(xtype), y, chkEven(xtype), y, xtype, z → {dec(y, dec( chkOdd(dec(z, km ⊕ exp)), y, xtype

Modélisation de la conjuration de clefs

Résumé : Les interfaces de programmation (IP) sont omniprésentes. Une classe particulière est celle des IP dites de sécurité qui utilisent des primitives cryptographiques (e.g. chiffrement, signature, . . . ) pour assurer des propriétés dites de sécurité (e.g. secret). L'interface de programmation de sécurité la plus connue à l'heure actuelle est sans aucun doute SSL.

Nous proposons un formalisme à la Dolev-Yao permettant de prendre en compte la technique de conjuration de clefs. Cette technique permet à un attaquant de faire croire qu'il a en sa possession une clef particulière. Pour cela, il utilise les commandes de l'IP avec pour entrée un nombre aléatoire jusqu'à ce que la commande interprète ce nombre aléatoire comme un chiffré valide. Nous montrons que le problème de la sécurité dans ce modèle est décidable pour une classe d'IP particulière comprenant l'architecture cryptographique commune d'IBM (Common Cryptographic Architecture). Cette IP de sécurité est notamment présente dans les automates bancaires.

Introduction

Cryptographic security APIs are sets of functions designed to facilitate the secure generation, storage, use and destruction of cryptographic keys. Security APIs for secure hardware devices typically manage keys by keeping a secret master key inside the device. This is used to encrypt all the 'working keys' used for operational functions, so that they can be securely stored outside the device. One technique used by attackers attempting to breach security is to try calling API functions with random values in the place of encrypted keys, to see if they are allowed to pass, or whether the device signals an error. This process is known as key conjuring [START_REF] Bond | Attacks on cryptoprocessor transaction sets[END_REF]. Learning the encrypted value of a key might not seem useful, but several attacks have been presented that leverage this trick in order to compromise the security of an API [START_REF] Bond | Attacks on cryptoprocessor transaction sets[END_REF][START_REF] Clulow | On the security of pkcs#11[END_REF].

A promising approach to security API analysis involves adapting Dolev-Yao style protocol analysis techniques [START_REF] Dolev | On the security of public key protocols[END_REF], where details of cryptographic algorithms used are abstracted away, and a logical model is constructed, with rules describing the operations of the intruder and protocol. This can be adapted quite naturally to API analysis by considering the API to be a set of 2-party protocols, each describing an exchange between the secure hardware module and the host machine [START_REF] Steel | Deduction with XOR constraints in security API modelling[END_REF][START_REF] Youn | Robbing the bank with a theorem prover[END_REF][START_REF] Cortier | Automatic analysis of the security of xorbased key management schemes[END_REF]. However, in previous work, the key conjuring trick was treated in an ad-hoc fashion, by adding a number of pre-chosen keys to the intruder's initial knowledge [START_REF] Steel | Deduction with XOR constraints in security API modelling[END_REF][START_REF] Youn | Robbing the bank with a theorem prover[END_REF][START_REF] Cortier | Automatic analysis of the security of xorbased key management schemes[END_REF], or by adding a rule to allow particular keys to be conjured [START_REF] Keighren | Model checking IBM's common cryptographic architecture API[END_REF]. This raises doubts about completeness of the search for attacks, and hence the strength of any proofs of security.

The aim of the work in this paper is to address this problem by proposing a formal model that identifies all computationally feasible key conjuring operations, and allows these to be incorporated into a Dolev-Yao style model for security analysis of the API. We propose a transformation that automatically computes all the possible ways of performing key conjuring from the API rules. Our transformation takes as input a set of formal rules representing the behaviour of an API and outputs new formal rules representing key conjuring. In this manner, we eliminate the need for the user to generate key conjuring rules by hand. As far as we are aware, this paper presents the first formal treatment that allows an exhaustive set of key conjuring rules to be obtained.

Our second main contribution is to show decidability of the security of APIs (expressed as a reachability property) for a class of APIs that includes for example the key management API of IBM's Common Cryptographic Architecture (CCA). In particular, it requires consideration of the algebraic properties of the Exclusive Or operation. Our decidability result holds for an unlimited number of sessions, though we do bound the number of times key conjuring operations are used. Indeed, it would not be realistic to allow the intruder to conjure as many keys as he wishes since it requires a significant amount of access to the API. This class is related to the class proposed in [START_REF] Cortier | Automatic analysis of the security of xorbased key management schemes[END_REF], with two main differences. First, we consider explicit decryption, since it was more appropriate for modelling key conjuring, and it reflects better the implementation. Second, we have to consider key conjuring rules which introduce fresh nonces.

INRIA

Some other decidability results have already been proposed for security protocols with Exclusive Or. In [START_REF] Comon-Lundh | Intruder deductions, constraint solving and insecurity decision in presence of exclusive or[END_REF] and [START_REF] Chevalier | An NP decision procedure for protocol insecurity with xor[END_REF], it is shown that secrecy is decidable, but only for a bounded number of sessions. Decidable classes of protocols with Exclusive Or and an unbounded number of sessions have been proposed in [START_REF] Comon-Lundh | New decidability results for fragments of first-order logic and application to cryptographic protocols[END_REF] and [START_REF] Verma | On the complexity of equational Horn clauses[END_REF], but API rules do not fit the restrictions made on the occurrences of variables in the protocol rules.

In the rest of the paper, we first explain the purpose and operation of security APIs, and define our formalism for describing them (Section 2). We then propose a transformation for key conjuring in Section 3. In Section 4, we explain the security problem we are interested in, and define a restricted class of APIs, arguing that these restrictions are quite natural. In Section 5 we show that certain classes of key conjuring operations are of no use to the intruder, and need not be considered in a formal model. We then show (Section 6) that security for our class of APIs is decidable in the presence of key conjuring operations. The class includes our motivating example, the key management API of the IBM 4758 Hardware Security Module, which was shown to be vulnerable to key conjuring attacks by Bond in [START_REF] Bond | Attacks on cryptoprocessor transaction sets[END_REF]. We conclude, with a discussion of future work, in Section 7.

Background

In this section, we first explain what a security API is, before going on to define the concept more formally.

Security APIs

The purpose of a security application program interface (API) is to allow untrusted code to access sensitive resources in a secure way. Hardware security modules (HSMs), for example, have security APIs which control access to the cryptoprocessor and memory inside the module. This allows the API to manage access to cryptographic keys. HSMs are deployed in security critical environments such as the cash machine network, where they are used to protect customers PINs and other sensitive data. They typically consist of a cryptoprocessor and a small amount of memory inside a tamper-proof enclosure. They are designed so that should an intruder open the casing or insert probes, the memory will auto-erase in a matter of nanoseconds. In a typical ATM network application, all encryption, decryption and verification of PINs takes place inside the HSM. Many different cryptographic keys will be used for these operations. IBM's 4758 CCA 1 API [2] partitions keys into various types, such as data keys, PIN derivation keys, import keys and export keys. Each type has an associated public control vector. The keys the HSM uses for its various operations, called working keys, are stored outside the HSM encrypted under the security module's master key (which is stored inside the HSM) XORed against the appropriate control vector for the key type. For example, a data key would be encrypted under km⊕data. 2 Working keys can then only be used by sending them back into the HSM under an appropriate API command. Only particular types of keys will be accepted by the HSM for particular operations. For example, data keys can be used to encrypt arbitrary messages, but so-called PIN Derivation Keys (PDKs, with control vector pin) cannot. This is critical for security: a customer's PIN is just his account number encrypted under a PIN derivation key. In 2001, Bond discovered attacks in which the intruder uses API commands to change the type of a key, exploiting the algebraic properties of XOR [START_REF] Bond | Attacks on cryptoprocessor transaction sets[END_REF]. The attack allows a PIN derivation key to be converted into a data key, which can then be used to encrypt data. Hence the attack allows the intruder to generate a PIN for any account number.

Formal work on the CCA first concentrated on rediscovering the attacks on the original version of the API [START_REF] Steel | Deduction with XOR constraints in security API modelling[END_REF][START_REF] Youn | Robbing the bank with a theorem prover[END_REF], and then on proving both Bond's proposed fixes [START_REF] Courant | Defending the bank with a proof assistant[END_REF], and the fixes IBM actually implemented [START_REF] Cortier | Automatic analysis of the security of xorbased key management schemes[END_REF], to be secure. However, these works made an informal approximation of the ability of the intruder to 'conjure' keys, a trick used several times in Bond's attacks. To explain precisely what key conjuring is, we first need to define some notation.

Definitions

We now define our (mostly standard) notation for reasoning about APIs, and then define the class of APIs considered in this paper.

Cryptographic primitives are represented by functional symbols. More specifically, we consider a signature Σ which consists of an infinite number of constants including a special constant 0 and three non constant symbols { } (encryption), dec (decryption) and ⊕ (XORing) of arity 2. We also assume an infinite set of variables X . The set of terms, denoted by T (Σ, X ), is defined inductively by

T ::= terms x variable x | f (T 1 , . . . , T n ) function application
where f ranges over the functions of Σ and n matches the arity of f . For instance, the term {m} k is intended to represent the message m encrypted with the key k (using symmetric encryption) whereas the term m 1 ⊕ m 2 represents the message m 1 XORed with the message m 2 . The constants may represent control vectors or keys for example. We rely on a sort system for terms. Terms which respect this sort-system are said to be well-typed. It includes a set of base type Base and a set of ciphertext type Cipher. We have variables and constants of both types. Moreover we assume that our function symbols have the following type:

⊕ : Base × Base → Base { } : Base × Base → Cipher dec : Cipher × Base → Base
A pure term t is a well-typed term whose only encryption symbol (when such a symbol exists) is at its root position. We say that a term t is headed with f if its root symbol INRIA is f . The set of variables occurring in t is denoted vars(t). We denote by st(t) the set of subterms of t. This notation is extended as expected to set of terms. A term is ground if it has no variable. Substitutions are written σ = {x 1 → t 1 , . . . , x n → t n } with dom(σ) = {x 1 , . . . , x n }. A substitution σ is ground if all of the t i are ground. The application of a substitution σ to a term t is written tσ.

We equip the signature Σ with an equational theory E API that models the algebraic properties of our operators:

E API :=    {dec(x, y)} y = x x ⊕ 0 = x dec({x} y , y) = x x ⊕ x = 0 x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z x ⊕ y = y ⊕ x
It defines an equivalence relation that is closed under substitutions of terms for variables and under application of contexts. In particular, we say that two terms t 1 and t 2 are equal, denoted by t 1 = E API t 2 if they are equal modulo the equational theory E API . If two terms are equal using only the equations of the last line (resp. involving ⊕), we say that they are equal modulo Associativity and Commutativity (AC) (resp. modulo Xor).

In the CCA API, as in many others, symmetric keys are subject to parity checking. The 4758 uses the DES (and 3DES) algorithm for symmetric key encryption. A (single length) DES key consists of 64 bits in total, which is divided into eight groups, each consisting of seven key bits and one associated parity bit. For an odd parity key, each parity bit must be set so that the overall parity of its group is odd. For an even parity key, the parity bits must be set so that all groups are of even parity. If the groups have mixed parities, then the key is of undefined parity and considered invalid. The CCA API checks that all DES keys are of odd parity, and all control vectors are even, so that a key XORed against a control vector will give another odd parity key. These parity considerations are important for our analysis of key conjuring, and are represented in our formalism by occurrences of the predicate symbols chkEven and chkOdd, each having a term as argument. Intuitively, chkOdd(t) means that t has an odd parity. Among the constants in Σ, some have a parity. By default (no explicit parity given to a constant), we will assume that such a constant has no parity. Moreover, we have some rules to infer parity from known facts, which are:

chkEven(x 1 ), chkEven(x 2 ) → chkEven(x 1 ⊕ x 2 ) chkOdd(x 1 ), chkOdd(x 2 ) → chkEven(x 1 ⊕ x 2 ) chkEven(x 1 ), chkOdd(x 2 ) → chkOdd(x 1 ⊕ x 2 )
Intruder capabilities and the protocol behaviour are described using rules as defined below.

Definition 1 (API rule) An API rule is a rule of the form

chk 1 (u 1 ), . . . , chk k (u k ), x 1 , . . . ,
chk i ∈ {chkOdd, chkEven}, 1 ≤ i ≤ k.
We also assume that the rule only involves pure terms.

The third condition might seem restrictive. However, it merely requires that we check each component of a sum rather than the entire sum. For example, if the sum v 1 ⊕ • • • ⊕ v k has some expected parity, each v i should also have some expected parity, and we ask that their parity is checked separately.

Example 1

The intruder capabilities are represented by the following set of three API rules:

x, y → {x} y encryption x, y → dec(x, y) decryption x, y → x ⊕ y xoring

Example 2 Commands may include several parity checks. In Figure 1, we give the whole of the symmetric key management subset of the IBM 4758 API, written in our notation. The terms km, imp, exp, kp, data and pin denote constant of Base type whereas xtype, xk1, . . . denote variables. Note that all the rules satisfies conditions stated in Definition 1. For instance, Key Import is used to make a new working key for an HSM. The new key is sent to the target HSM encrypted under a transport key. The command decrypts the imported package, and returns the key encrypted under the local master key XOR the appropriate control vector.

A Formal Theory of Key Conjuring

We first introduce key conjuring informally, giving an example of a key conjuring attack. This will help to explain our transformation. We then formally define our transformation that takes a set of API rules, and extends it with rules that permit key conjuring.

Key Conjuring

As we have seen, key management APIs like the CCA keep working keys outside the HSM, safely encrypted, so that they can only be used by sending them back into the HSM under the terms of the API. What happens when an intruder wants to use a particular command in an attack, but does not have access to an appropriate key? For example, suppose he has no data keys (terms of the form {d1} km⊕data ), but wants to use the Encipher command. In an implicit decryption formalism, the command is defined like this

x, {xkey} km⊕data → {x} xkey

RR n 6134

This suggests that the command cannot be used if the intruder does not have a data key. However, in reality, an intruder could just guess a 64 bit value and use that in place of the data key. The HSM will decrypt the guessed value under km ⊕ data, and check the parity of the resulting 64 bit term to see if it is a valid key before, enciphering the data. Usually, the check will fail and the HSM will refuse to process the command, but if the intruder guesses randomly, he can expect that 1 in every 256 guessed values will result in a valid key. This notion is captured by our formalism, in which we write the Encipher command like this: chkOdd(dec(y, km ⊕ data)), x, y → {x} dec(y,km⊕data)

It may seem useless for the intruder to simply guess values, since the result is a term he knows enciphered under an unknown key, but used cleverly, this technique can result in serious attacks. For example, Bond's so called import-export attack [START_REF] Bond | Attacks on cryptoprocessor transaction sets[END_REF], uses key conjuring to convert a PIN derivation key into an encryption key, allowing an intruder to generate the PIN for any given account number.

Description of Bond's attack. We give Bond's attack in Figure 2, written in our formalism, with explicit decryption and parity checking. We assume that the attacker initial knowledge contains {pdk} km⊕pin , i.e. a PIN key encrypted for transfer, the control vectors pin, data, imp, exp, kp and the constant 0. Moreover, we model the fact that the parity of all the control vectors are even and the parity of the secret keys km and pdk is odd by considering the corresponding facts (e.g. chkEven(pin)). We will show how the PIN derivation key pdk can be converted into a data key, which then can be used to encrypt data. Hence the attack allows a criminal to generate a PIN for any account number. For this, we show that the attacker is able to derive {pdk} km⊕data .

Step 1 is a key conjuring step. The attacker is using the Key Part Import 3 command, using the control vector imp (for xtype) and the key part 0 (for xk3) but without a term of the form {m} km⊕kp⊕imp . Instead, he repeatedly tries random values until some value n 1 decrypts under km ⊕ kp ⊕ imp to give a valid key, i.e. a term of odd parity. Note that we have written this by labelling the arrow to show the conjuring of a new term n 1 , and the odd parity check is now on the right hand side of the rule, indicating that the intruder has learnt the fact chkOdd(dec(n 1 , km ⊕ kp ⊕ imp)). In the rest of the attack we write r in place of dec(n 1 , km ⊕ kp ⊕ imp).

Having succeeded in finding a suitable value n 1 , he uses the command again with imp ⊕ exp as the key part to be added to the key, in Step 2. This yields two unknown key encrypting keys, r and r ⊕ imp ⊕ exp, with a known difference.

In Step 3, the intruder uses key conjuring again, this time with the Key Import command, using random values in place of {xkey} xkek⊕xtype , and using {r} km⊕imp as the key encrypting key. Again, we write this as the generation of a new term n 2 , and the intruder learns the fact chkOdd(dec(n 2 , r ⊕ imp)). In the rest of the attack we write r in place of dec(n 2 , r ⊕ imp). In Step 4, the intruder uses the conjured value again to obtain an export version of the key.

The partial keys obtained by these two operations can then be completed using Key Part Import 3. The exporter is completed to give {r } km⊕exp , in Step 5, whilst the importer is set to change the type of a key from pin to data, in Step 6. A PIN derivation key {pdk} km⊕pin can then be turned into a data key by first exporting it under {r } km⊕exp using Key Export in Step 7, and then changing the type by re-importing it using {r ⊕ data ⊕ pin} km⊕imp as the importer, in Step 8. Having obtained a PIN derivation key as a data key, the intruder can now encrypt account numbers to obtain customer PINs.

INRIA 1. Key Part Imp. 3 ?, 0, imp new n1 → {dec(n 1 , km ⊕ kp ⊕ imp)} km⊕imp , n 1 chkEven(0), chkEven(imp) chkOdd(dec(n 1 , km ⊕ kp ⊕ imp)) Let r = dec(n 1 , km ⊕ kp ⊕ imp) 2. Key Part Imp. 3 n 1 , imp ⊕ exp, imp → {r ⊕ imp ⊕ exp} km⊕imp chkEven(imp), chkEven(imp ⊕ exp) chkOdd(dec(n 1 , km ⊕ kp ⊕ imp)) 3. Key Import ?, imp ⊕ kp, {r} km⊕imp new n2 → {dec(n 2 , r ⊕ imp ⊕ kp))} km⊕imp⊕kp , n 2 chkOdd(r), chkEven(imp ⊕ kp) chkOdd(dec(n 2 , r ⊕ imp ⊕ kp)) Let r = dec(n 2 , r ⊕ imp ⊕ kp) 4. Key Import n 2 , exp ⊕ kp, {r ⊕ imp ⊕ exp} km⊕imp → {r } km⊕exp⊕kp chkEven(exp ⊕ kp), chkOdd(r ⊕ imp ⊕ exp) chkOdd(dec(n 2 , r ⊕ imp ⊕ kp)) 5. Key Part Imp. 3 {r } km⊕exp⊕kp , 0, exp → {r } km⊕exp chkEven(0), chkEven(exp), chkOdd(r )
In 2003, as a result of work by Youn et. al [START_REF] Youn | Robbing the bank with a theorem prover[END_REF], it came to light that this attack was impossible in practice, as an undocumented check in the CCA's implementation prevents key parts being passed to Key Import. This would mean steps 3 and 4 of the attack couldn't be executed. However, further attacks using key conjuring had been discovered by then, [START_REF] Clayton | Experience using a low-cost FPGA design to crack DES keys[END_REF][START_REF] Clulow | On the security of pkcs#11[END_REF], on both the CCA API and other APIs. Clulow notes in [START_REF] Clulow | On the security of pkcs#11[END_REF] that key conjuring can be prevented by using a hash or MAC to test the authenticity of keys, but many designs do not include such measures, which increase the key management overhead.

Our example attack shows the potential of key conjuring to mount attacks. It also demonstrates the features of our formalism which allow us to detect realistic key conjuring operations. A simple 'explicit decryption' model is not sufficient for a key conjuring analysis, since though this allows an attack like Bond's be discovered, it doesn't take into account parity checks. This means that the model cannot distinguish between feasible and nonfeasible key conjuring steps, leading to false attacks. For example, for a command like Key Import (see Example 2), an explicit decryption model without parity checking would allow an intruder to conjure values for both y and z, which in practice is highly unlikely: only 1 in every 2 16 pairs of values will pass. Our transform ensures that the intruder has to guess values for at most one parity check.

Transformation on the API rules

We propose a transformation allowing us to model key conjuring. This transformation is generic enough to deal with any API made up of rules satisfying the conditions given in Definition 1.

We first introduce a set of nonces, denoted by N , a subset of the set of constants that does not contain the special constant 0. We assume an infinite number of nonces of both types. A nonce represents a fresh value that has been never used before. Rules obtained after transformation are called key conjuring rules and have the following form:

x 1 , . . . , x n new n → t, n chk 1 (u 1 ), . . . , chk k (u k ) chk 1 (v 1 ), [chk 2 (n)] The notation [chk 2 (n)] is used to express the fact that chk 2 (n) is optional. Let R l → R r = chk 1 (u 1 ), . . . , chk k (u k ), x 1 , . . . ,
x n → t be an API rule. For each i such that 1 ≤ i ≤ k, since u i is a term of Base type not headed with ⊕ and which contains no encryption symbol, we have that u i is either a constant, a variable or a term of the form dec(z, t). In this last case, we compute the key conjuring rules associated to R l → R r as follows:

INRIA 1. Let σ = {z → n}, we consider the new rule (R l {z, chk j (u j )} new n → R r ∪ {z, chk j (u j )})σ
2. Moreover, we have that

t = p i=1 y i ⊕ i=1 c i ⊕ q i=1 dec(z i , t i ).
for some variables y i , z i , some constants c i and some terms t i . For each j such that 1 ≤ j ≤ p, we let σ = {y j → n} and we consider the new rule

(R l {y j , chk j (u j )} new n → R r ∪ {y j , chk j (u j )})σ
Moreover, we push also on the right hand-side the check performed on y j if such a check exists.

Given an API rule R, we denote by KeyCj(R) the set of rules obtained after applying the transformation described above. This notation is extended as expected to sets of API rules.

Example 3 Consider the rule R, namely Key Part Import 3 described below.

y, xk3, xtype → {dec(y, km ⊕ kp ⊕ xtype) ⊕ xk3} km⊕xtype chkEven(xtype) chkEven(xk3) chkOdd(dec(y, km ⊕ kp ⊕ xtype))
The purpose of this rule is to allow a user to add a final key part xk3 to a partial key y with control vector xtype. After applying our transformation, the set KeyCj(R) contains the two rules described below:

xk3, xtype new n → {dec(n, km ⊕ kp ⊕ xtype) ⊕ xk3} km⊕xtype chkEven(xtype) chkOdd(dec(n, km ⊕ kp ⊕ xtype)) chkEven(xk3) y, xk3 new n → {dec(y, km ⊕ kp ⊕ n) ⊕ xk3} km⊕n chkEven(xk3) chkOdd(dec(y, km ⊕ kp ⊕ n)) chkEven(n)
This represents the two ways the intruder can use the rule for key conjuring. In the first, he conjures a partially completed key (this is the rule used in step 1 of the Bond attack in Figure 2). In the second, for a fixed constant y, he conjures a control vector that will allow y to be decrypted to form a valid partial key. Note that the conjured control vector is of even parity, so the intruder learns two parity facts in this case. Our transform allows this kind of conjuring because it is assumed the intruder can set the parity of the terms he uses as guesses. The value that is checked for even parity is under his control. Hence the probability of success is the same as for the first conjuring variant.

The rules obtained by applying our key conjuring transformation on the IBM CCA Symmetric Key Management Transaction Set is fully described in Appendix (Figure 3).

Note that our transformation will sometimes produce rules which the intruder cannot use. This happens when the fresh nonce appears in a parity check on the left, as in the first rule for Key Import in Figure 3. The intruder cannot use this rule, since he does not know any parity information about the new nonce before the command is used. This corresponds to a case where the intruder would have to guess a value that decrypts to give a valid key, k, such that k also decrypts some other value to give a valid key. For single length DES keys, this gives the intruder a 1 in 2 16 chance of success, which we consider unrealistic. However, if the intruder has extended access to a live HSM running the API, we believe our transformation could be quite naturally extended to these more costly operations (see Section 7).

Intruder rules

We denote by I the three API rules representing the capabilities of the intruder (see Example 1). We observe that the intruder does not have to follow any parity checks when encrypting or decrypting, but that he can also check the parity of terms he produces. Recall that parity is defined only on terms of Base type. If an intruder makes a new term by XORing, he can already predict the parity of the outcome following the rules in Section 2.2. However, when decrypting, the intruder may learn new parity information by decrypting a known constant with a random key, or by decrypting a random constant with a known key. We refer to this as offline key conjuring. The rules corresponding to this are described below: by decrypting a random constant with a known key y new n → dec(n, y), n with X ∈ {Odd, Even} chkX(dec(n, y))

Let I + 1 be the set of these two rules. decrypting a known constant with a random key

x new n → dec(x, n), n, chkX(n) with X, Y ∈ {Odd, Even} chkY(dec(x, n))
Let I + 2 be the set of these four rules. In Section 5, we will see that for a certain class of APIs, the class considered in this paper, the offline key conjuring rules can be safely ignored. Our final set of intruder rules, including offline key conjuring, is denoted by

I + = I ∪ I + 1 ∪ I + 2 .

A New Decidable Class

In this section, we define the semantics of our API-rules and we introduce the class of rules for which we prove our decidability result.

Security Problem

The problem we consider is the problem of deciding whether a particular term, for example a PIN derivation key, can be learnt by an attacker. The intruder starts with a fixed set of terms that constitute his initial knowledge. He can then use the rules of the API and also the key conjuring variants of the rules in any order to extend his knowledge. We first need to make sure that parity checks are performed consistently.

Definition 2 (consistent) Let S = {chk 1 (u 1 ), . . . , chk i (u i )}∪T where u 1 , . . . , u i are ground terms of Base type and T is a set of terms. We denote by SatChk(S) the smallest set which contains S and that is closed by application of the following rules modulo Xor.

chkEven(x 1 ), chkEven(x 2 ) → chkEven(x 1 ⊕ x 2 ) chkOdd(x 1 ), chkOdd(x 2 ) → chkEven(x 1 ⊕ x 2 ) chkEven(x 1 ), chkOdd(x 2 ) → chkOdd(x 1 ⊕ x 2 )
We say that S is consistent if for any term t, chkOdd(t) and chkEven(t) are not both in SatChk(S).

A fact is either a term t or a parity check, i.e. chkX(t). A fact is ground if the term t is ground and it is said pure if the term t is pure and of Base type inside a parity check.

Example 4 Let S be the following set: A term u is deducible from S by using the set of rules A modulo the equational theory E, denoted by S A,E u if u ∈ S (modulo E) or there exists some sets of facts F 1 , . . . , F n such that u ∈ F n and

S = {chkEven(a ⊕ b), chkEven(b ⊕ c), chkOdd(a ⊕ c)} S is not consistent. Indeed, since (a ⊕ b) ⊕ (b ⊕ c) = Xor a ⊕ c,
F i is one-step deducible from S ∪ F 1 ∪ . . . ∪ F i-1 . The sequence F 1 , . . . , F n is a proof that S A,E u.
Of course, at each step of the proof the set of ground facts obtained has to be consistent with respect to the parity checking predicates. However, this will be the case by construction, since the only rules which add parity facts are the key conjuring ones, which always introduce something fresh in the parity facts.

Example 5 Let S = {{s} a , a ⊕ b, b}. We have that s is deducible from S by using the rules I modulo E API . Indeed, we have that S, {a}, {s} is a proof of S I,E API s.

Example 6 (Bond's Import/Export attack) Let A be the rules described in Figure 1, V = {pin, data, exp, imp, kp}. Let S be a set which contains: {pdk} km⊕pin , chkOdd(pdk), chkOdd(km), t and chkEven(t) for any t ∈ V.

We have that {pdk} km⊕data is deducible from S by using the rules in A∪KeyCj(A)∪I modulo E API . The proof witnessing this fact can be easily extracted from Figure 2.

Note that this attack involves two online key conjuring steps. Each key conjuring attempt has a 1 in 256 chance of success, due to the parity checks. Each time the adversary wants to conjure a key, it requires a significant amount of access to the API. We assume in what follows that the use of these rules by the adversary is limited. This is modelled by introducing a parameter k that bounds the maximum number of applications of the key conjuring rules induced by the protocol. The value of k could be set based on the amount of time an attacker may have access to a live HSM, based on physical security measures, auditing procedures in place, etc. Note however that we do not bound the number of offline key conjuring since it is much easier for an adversary to try numerous values off-line.

Formally, we write S A2 ≤k A1,E API u if u is deducible from S by using the rules in A 1 and at most k instances of the rule in A 2 (modulo E API ). In this paper we rely on a fixed equational theory, denoted by E API (see Section 2.2) and a fixed set of intruder rules denoted by I + . Hence our problem is the following one:

Security Problem

Entries: A finite set A of API rules, a set S of pure ground facts that is consistent (the initial knowledge of the attacker), a pure ground term s (the secret) and a bound k ∈ N (number of key conjuring steps).

Question: Is the secret s deducible from S by using the rules in A ∪ I + and at most k instances of rules in KeyCj(A) (modulo E API ), i.e. does S KeyCj(A) ≤k A∪I + ,E API s?

Well-formed API

API-rules as defined in Definition 1 are slightly too general for our decidability result. Hence we introduce further assumptions, that we believe are very reasonable in practice. Note that these hypotheses are checked on the API rules before performing the key conjuring transformation.

INRIA

Definition 4 Let S 0 be a set of pure ground fact that is consistent. Let R = R l new n → R r be a rule and t be a term of Base type. We say that t is checked in R w.r.t.

S 0 if chkX(t) ∈ SatChk(S 0 ∪ R l ∪ R r ).
Definition 5 Let R be a rule. KeyTerm(R) are the subterms of R which appear at a key position. More formally, KeyTerm(R) = {KeyTerm(t) | t ∈ R or chkX(t) ∈ R} where KeyTerm(t) is defined as follows:

KeyTerm(t) = {u 2 | dec(u 1 , u 2 ) ∈ st(t) for some u 1 } ∪ {u 2 | {u 1 } u2 ∈ st(t) for some u 1 }.
We will restrict our attention to APIs such that a term which appears at a key position has to be parity checked. This hypothesis is natural, since it corresponds to the API designer being consistent about checking the parity of keys before they are used.

Example 7 Let V = {imp, kp, exp, pin, data}. and S 0 be a set that is consistent and which contains at least chkEven(t) for any t ∈ V and chkOdd(km). The rules given in Figure 1 are such that each term which appears at a key position is checked w.r.t. S 0 .

Definition 6 (dec-property) Let T be a set of terms. We say that T has the dec-property

if dec(x, v 1 ), dec(x, v 2 ) ∈ st(T ) ⇒ v 1 = v 2 .
We say that a rule R has the dec-property if the set of terms T = {t | t ∈ R or chkX(t) ∈ R} satisfies the dec-property.

In the API we consider, we will assume that all the rules satisfy the dec-property. This hypothesis is natural, since it only forbids the API from decrypting the same input under two different keys. Note that the dec-property is clearly satisfied by the rules given in Figure 1.

Definition 7 (well-formed API rule) Let S 0 be a set of pure ground fact that is consistent. Let R be an API rule.

chk 1 (u 1 ), . . . , chk k (u k ), x 1 , . . . , x n → t
We say that R is well-formed w.r.t. S 0 if: for all i such that 1 ≤ i ≤ k, we have that u i ∈ st(t), R satisfies the dec-property,

for all v ∈ KeyTerm(R), v is checked in R w.r.t. S 0 .
An API rule satisfying only the two first points is said to be weakly well-formed.

The first point requires that the API only checks the parity of objects that are to be used in generating the output. Since the form of our rules has only variables on the left, and all decryption explicitly stated on the right, this is quite natural. We would not expect an API to check the parity of a term that is subsequently discarded. For instance, the API rules given in Figure 1 are well-formed. However, the rules describing the capabilities of the attacker (see Example 1) are not well-formed, but only weakly well-formed.

Decidability

Theorem 1 (Main result) Let P be an instance of the security problem (as stated at the end of Section 4.1) where the set A of API rules is well-formed w.r.t. the set S 0 ∈ S, the terms in S ∪ {s} do not contain any symbol dec.

We can decide whether P is a positive or a negative instance of the security problem.

The remainder of the paper is devoted to the proof of this result. We proceed in several steps:

1. From I + to I. In Section 5, we establish some reduction results allowing us to get rid of the offline key conjuring rules. These results are obtained for any set of API rules as defined in Definition 1, and not only the well-formed ones introduced in Definition 7.

2. From E API to AC. In Section 6.1, we show that we can get rid of some axioms of the equational theory by using the fact that E API satisfies the finite variant property introduced in [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF]. This can be done safely by considering some new rules, namely the variants denoted Var (A), which are obtained from the rules A we have at the beginning by instantiating them.

3. Controlling the form of the rules. In Section 6.2, we show that the variants computed at the previous step satisfy some properties. Given a set A of (weakly) well-formed API rules, we have that Var (A ∪ KeyCj(A)), rules obtained after our both transformations, are (weakly) well-adapted (see Definition 9).

4. Existence of a pure attack. In Section 6.3, we show that for a set of weakly well-adapted rules, if there exists an attack then there is one which only involves pure terms (see Proposition 5).

5.

Bounded the number of subterms headed with dec. Now, to obtain our decidability result it is sufficient to bound the number of terms headed with dec in an attack (see Section 6.4). This allows us to consider only a finite number of terms.

Off-line key conjuring is useless

The adversary can perform as many off-line key conjuring as he wishes, since it is very easy for him to try numerous values off-line, until the decryption algorithm yields a bitstring of the desired parity. We show now that in fact, off-line key conjuring does not provide any extra possibilities for the adversary to mount an attack. Thus there is no need to consider these rules.

INRIA

We first show that the rules of I + 1 are useless as soon as the adversary knows a fixed constant of each parity.

Proposition 1 Let A be a set of API rules and S be a set of pure ground facts. We have that

S KeyCj(A) ≤k A∪I + ,E API u ⇔ S KeyCj(A) ≤k A∪I∪I + 2 ,E API u
where S = S ∪ {c 1 , c 2 , chkOdd(c 1 ), chkEven(c 2 )} and c 1 , c 2 are constants of Base type that do not appear in A, S and u.

Then, we show that there is no need to consider rules of I + 2 if the intruder already knows terms of the form dec(1, c i ) of each parity. Intuitively, the intruder knows an instance of each of the four rules.

Proposition 2 Let A be a set of API rules and S be a set of pure ground facts. We have that S The idea of the proof is to replace each application of a rule

KeyCj(A) ≤k A∪I∪I + 2 ,E API u ⇔ S KeyCj(A) ≤k A∪I,E API
x new n
→ dec(n, x), chkX(dec(x, n)), chkY(n) in I + 2 by its corresponding instance. In particular, x is always replaced by the same constant 1. We can show that we still obtain a proof. Intuitively, if it was not the case, it would mean that it was important for x to be an encryption or a decryption. This would be the case only if there was nested encryption on the right hand side of the rule, which is not the case for API rules.

Decidability for Well-Formed APIs

In the remainder of this section we describe a decision procedure to deal with any set of well-formed API rules.

Getting rid of some equations

The goal of this section is to get rid of all the axioms of the equational theory but associativity and commutativity, decomposing the theory into a convergent rewriting system modulo AC equations. The idea is to pre-compute variants of the rules so that there is no need to apply the full equational theory anymore.

Let R be a term rewriting system (TRS) and E be an equational theory, we write u → R,E v when v can be written into v modulo E . A decomposition of an equational theory E is a pair (R, E ) such that R is an E -convergent system for E, i.e. u = E API v if and only if u↓ = v↓ where u↓ denotes the normalized form of u w.r.t. → R,E .

For instance, for the equational theory E API , we can show that (R ⊕ , AC) is a decomposition of E API where

R ⊕ =    dec({x} y , y) → x x ⊕ x → 0 {dec(x, y)} y → x x ⊕ 0 → 0 x ⊕ (x ⊕ y) → y
Definition 8 (finite variant property) A decomposition (R, E ) of a given theory E has the finite variant property if for every term t, there is a finite set of subtitutions Σ(t) such that ∀σ∃θ ∈ Σ(t), ∃τ such that σ↓ = E θτ ∧ (tσ)↓ = E (tθ)↓τ.

In other words, all possible reductions in an instance of t can be computed in advance. Given a term t, we denote by Var (t) the set of its variants, i.e. Var (t) = {(tθ)↓ | θ ∈ Σ(t)}. In [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF], the authors give sufficient condition to establish that a given presentation satisfies the finite variant property. Moreover they give an algorithm allowing us to compute the variants associated to a given term. By using their result, it is easy to establish that (R ⊕ , AC) is a decomposition of E API which satisfies the finite variant property. The so-called variants of a rule R are obtained by performing narrowing with R ⊕ modulo AC.

Narrowing. The subterm of t at position p ∈ O(t) is written t| p . The term obtained by replacing t| p with u is denoted t[u] p . We denote by Ō(t) the set of non-variable position of t. Given a TRS R, we say that a term t narrows to t with the substitution σ, at p ∈ Ō(t), by l → r ∈ R if there exists a renaming l → r of l → r ∈ R such that σ is a unifier of t| p and l and t = (t[r] p )σ. In this case, we write t σ t . We write t * σ t if there exists a narrowing derivation t = t 1 σ1 t 2 . . . σn-1 t n = t such that σ = σ 1 . . . σ n-1 . If E is a set of equations such that an E -unification algorithm exists, we define E -narrowing as expected (σ is an E -unifier of t| p and l). In particular, this allows us to define AC-narrowing.

Computation of the variants. Let R be an API rule and k be the number of occurrences of { } , dec and ⊕. According to [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF], we have that Example 8 For instance, consider the following rule R = x, y → dec(x, y). We have that Var (R) = {R, R } where R = {z} y , y → z. Note that R is a normalized instance of R. Indeed R = Rθ↓ where θ = {x → {z} y }.

Var (R) = {R | R * σ R

Controlling the form of the rules

We need to control the form of the rules after computation of the key conjuring transformation and computation of the variants. We show that the set Var (A∪KeyCj(A)) obtained from a set A which only contains (weakly) well-formed rules w.r.t. S is (weakly) well-adapted w.r.t. S. Definition 9 (well-adapted) Let S 0 be a set of pure ground fact that is consistent. Let

R = R l [new n] → R r . We say that R is well-adapted w.r.t. S 0 if 1. R is well-typed and vars(R r ) ⊆ vars(R l ) ,
2. a term of type Cipher appearing as a strict subterm position in R is either a nonce or a variable, 3. for all t ∈ KeyTerm(R), t is checked in R w.r.t. S 0 , 4. there is at most one term u in a check in R r not equal to n and we are in one of the following cases:

u = dec(y, n ⊕ u ), u = dec(n, u ), or
n occurs in R l and hence the rule R is useless.

A set of rules which satisfies the two first points is said to be weakly well-adapted.

Proposition 4 Let S 0 be a set of pure ground fact that is consistent. Let A be a set of (weakly) well-formed API rules w.r.t. S 0 . Let A = Var (A ∪ KeyCj(A)). We have that A is a set of (weakly) well-adapted rules w.r.t. S 0 .

The notion of well-adapted relies on four conditions (see Definition 9). The conditions 1, 3 and 4 are established by using the fact that a variant R is just a nomalized instance of wellformed API rule R, that is R = Rθ↓ for some θ. Proving condition 2 is more involved. As shown in the example below, Condition 2 is not stable by AC-narrowing, i.e. by computation of the variants thus we had to first enforce it.

Example 9 Let R = x → {dec(x, k 1 )} dec(x,k2) . The condition 2 is satisfied by R. Now, consider the rule

R = {y} k1 → {y} dec({y} k 1 ,k2)
We have that R ∈ Var (R). However, R does not satisfy the condition. This problem comes from the fact that there is a variable of type Cipher which involved in two differents subterms headed with dec. Here we have that x is involved in dec(x, k 1 ) and also in dec(x, k 2 ). Since k 1 = k 2 , the rule R does not satisfy the dec-property and hence is not a well-formed rule.

Existence of a pure attack

We show in this section that we can restrict our attention to proofs which only involve pure terms. The following result holds for any set of weakly well-adapted rules. The conditions 3 and 4 of Definition 9 are only used for the last part of our decision procedure (see Section 6.4).

A position in a term is impure if the subterm at that position is not of the expected type and form. By convention the root position is always an impure position. Note that in a pure term t the only impure position is Λ. We first prove that whenever an impure term occurs in a deducible term t at a position p, the term t| p is itself deducible.

Lemma 1 Let A be a set of weakly well-adapted rules and S be a set of pure ground facts that is consistent and which contains 0. Let u be a ground term deducible from S and F 1 , . . . , F n be a proof that S A,AC u. Let p be an impure position of u. We have that u| p ∈ S ∪ F 1 ∪ . . . ∪ F n .

We are now ready to state our result which says that only pure terms need to be considered when checking for deducibility.

Proposition 5 Let A be a set of weakly well-adapted rules and S be a set of pure ground facts that is consistent and which contains 0. Let u be a pure ground term. If S A,AC u then there is a proof of S A,AC u which only involve pure terms.

To establish this result, we assume given a proof P of S A,AC u and we show how to compute a proof P from P which only involves pure term. The proof P uses exactly the INRIA same rule at each step but not the same instance. In particular any term appearing at an impure position will be replaced to obtain a pure term. From this, we easily deduce the following corollary.

Corollary 1 Let A 1 , A 2 be two set of weakly well-adapted rules and S be a set of pure ground facts that is consistent and which contains 0. Let u be a pure ground term. If S A1 ≤k A2,AC u then there is a proof witnessing this fact which only involves pure terms.

A bound on the number of dec terms

From Corollary 1 we know that if there is an attack, there is an attack that involves only pure terms. Pure terms are well-typed and contain at most one encryption symbol. However, the dec symbols might be arbitrarily nested. Our goal is to bound the size of an attack by limiting the use of dec symbols.

A dec-term is a term of the form dec(u, v). Given a proof F 1 , . . . , F n of some deduction fact S R,AC w, we say that a dec-term t is legal if it is checked in S, that is chkX(t) ∈ SatChk(S) or it has been produced by a key-conjuring rule, that is chkX(t) ∈ F j for some 1 ≤ j ≤ n. The term t is said illegal otherwise. Let k be the number of legal dec terms occurring in S. Since there are at most k applications of the key-conjuring rules and since each key-conjuring rule introduces at most one term that is not a name, there are at most k + k legal dec term occurring as subterm in a proof F 1 , . . . , F n . We wish to show that, besides the legal dec-terms, no decryption symbol can occur under a key position. This ensures that illegal dec-terms can only occur as plaintext thus can not be nested. We first show that illegal dec-term cannot occur in checks.

Lemma 2 (No illegal dec-term in checks) Let A be a set of well-adapted rules and S be a set of pure ground facts such that no dec terms occurs in KeyTerm(S). Let w be a pure ground term deducible from S and F 1 , . . . , F n be a proof that S A∪Var (I),AC w that involves only pure facts. We assume that there is no dec-term subterm of w. For any term t such that chk(t) ∈ SatChk(S ∪ F 1 ∪ . . . ∪ F n ), for any dec(u, v) subterm of t, the dec-term dec(u, v) is legal.

The intuitive idea for proving this lemma is that new checks can only be introduced by the key-conjuring rules, which are limited. In addition, when a chkX(t) is introduced, illegal dec-terms cannot occur since the rules are well-adapted.

We then prove that illegal dec-terms cannot occur in key position or they can be replaced by 0. Let N and N be two terms. For any term M , we denote by M δ N,N the term M where any occurence of N in key position is replaced by N .

Lemma 3 (Replacement of dec-terms in key position) Let A be a set of well-adapted rules and S be a set of pure ground facts such that no dec terms occurs in KeyTerm(S). Let w be a pure ground term deducible from S and F 1 , . . . , F n be a proof that S A∪Var (I),AC w that involves only pure facts. We assume that there is no dec-term subterm of w. Let t be a term such that t ∈ F j for some 1 ≤ j ≤ n and let p be some key position of t such that t| p = dec(u, v) ⊕ t (t being possibly empty in which case by convention, t| p = dec(u, v)).

Either the term dec(u, v) is legal.

Or F 1 δ (dec(u,v)⊕t ,0) , . . . , F j δ (dec(u,v)⊕t ,0) is a pure proof of S R∪Var (I),AC tδ (dec(u,v)⊕t ,0) .
The lemma is proved by induction. Now, we are able to prove our main result (Theorem 1). Proof. Let P be an instance of the security problem where the set A of API rules is wellformed w.r.t. S and 0 ∈ S. Let S be the set of facts obtained from S by adding 1 (constant of type Cipher),

c 1 , c 2 , c 1 , c 2 , c 3 , c 4 constants of Base type, chkOdd(c 1 ), chkOdd(c 1 ), chkOdd(c 3 ), chkEven(c 2 ), chkEven(c 2 ), chkEven(c 4 ), chkOdd(dec(1, c 1 )), chkOdd(dec(1, c 2 )), chkOdd(dec(1, c 3 )), chkOdd(dec(1, c 4 )).
Note that no dec terms occurs in KeyTerm(S ).

Thanks to Propositions 1 and 2, we easily deduce that u then there exists a proof witnessing this fact which involves only pure terms. Lastly, Lemmas 2 and 3 allow us to bound the number of dec-terms which can appear in such a proof. This allows us to consider only a finite number of terms: we have a finite number of constants and nonces which can only be combined to produce pure terms involving some precise dec-terms.

Complexity. Our decision procedure works as follows. We first guess the k legal terms that are produced by key conjuring rules and then saturate the set S with all deducible terms that are pure terms with no illegal dec terms under key position. Let n by the number of constants occurring in S plus k. Illegal dec terms cannot occur nested thus it is easy to see that there are at most n × 2 n illegal dec terms. These dec terms can be arbitrarily XORed in plaintext position but cannot occur under key position. Thus we have to consider at most 2 2 O(n) terms. Thus our procedure terminates after at most 2 2 O(n) steps. Altogether, we can show that our algorithm is non-deterministic 2-EXPTIME.

Conclusion

We have presented a formalism for key conjuring, obtained by applying a transformation to a model of a security API with explicit parity checks. We have shown that the security problem is decidable for a general class of APIs (well-formed).

In this paper, we have concentrated on the example of the IBM CCA API, with its XOR-based scheme for key management. However, we believe our approach can be applied in general to security API analysis. In particular, our language for defining API commands, with variables on the left hand side and all decryption made explicit on the right, seems more natural than the use of an Alice-Bob style implicit decryption formalism. Our decidability suggests that analysis can still be tractable in this kind of explicit decryption formalism. The use of predicates to specify input checks could be extended beyond parity checking, to predicates that depend on state. Our transformation could then be used to identify operations that allow the intruder to learn state information. We could also extend our transformation to allow more computationally expensive key conjuring operations, by allowing multiple fresh terms to be generated in a single rule.

We plan to extend our results to a larger class of APIs, incorporating pairing and further cryptographic primitives, and to implement our model in an analysis tool. There remains a significant class of known API attacks that has not been dealt with formally: so-called parallel key search attacks. Formalising key conjuring is an important first step towards this, since many of these attacks rely on building up a set of conjured keys.

RR n 6134 exists a position p ∈ O(s) such that s| p = E lσ and t = s[rσ] p for some substitution σ and rule l → r ∈ R. A rewrite system R is E -confluent if and only if for every s, t such that s = R∪R -1 ∪E t, there exists s , t such that s * -→ E \R s , t * -→ E \R t , and s = E t . It said to be

E -convergent if, in addition, = E • → R • = E is well founded.
A term t is in normal form (w.r.t. → E \R ) if there is no term s such that t → E \R s. If t * -→ E \R s and s is in normal form then we say that s is a normal form of t. When this normal form is unique, we write s = t↓ E \R or shortly s = t↓ when E \R is clear from the context. A substitution σ is called normalized if for every x ∈ dom(σ), xσ is in normal form.

Finite Variant Property In [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF], the authors give sufficient condition to establish that a given presentation satisfies the finite variant property. Moreover they give an algorithm allowing us to compute the variants associated to a given term. By using their result, to establish the fact that (R ⊕ , AC) is a decomposition of E API which satisfies the finite variant property, it is sufficient to establish what they have called the boundedness property. For this, we can easily show that: Lemma 4 Let t 1 and t 2 be irreducible terms (w.r.t. R ⊕ /AC), dec(t 1 , t 2 ), {t 1 } t2 and t 1 ⊕ t 2 can be reduced to its normal form using at most 1 reduction step.

Lemma 4 given in [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF], allows us to conclude that (R ⊕ , AC) is a decomposition of E API which satisfies the boundedness proeprty and hence the finite variant property. Proposition 3 is an easy consequence of the fact that (R ⊕ , AC) is a decomposition of E API which satisfies the finite variant property.

C Controlling the form of the rules

We need to ensure some conditions after computation of the Key conjuring transformation and computation of the variants. The proofs of this section are devoted to establishing the following proposition: Proposition 4 Let S 0 be a set of pure ground fact that is consistent. Let A be a set of (weakly) well-formed API rules w.r.t. S 0 . Let A = Var (A ∪ KeyCj(A)). We have that A is a set of (weakly) well-adapted rules w.r.t. S 0 .

We prove this Proposition by establishing each condition separately.

C.1 Condition 1

Lemma 5 Let R be a weakly well-formed API rule.

Let R = R l [new n] → R r ∈ Var (R ∪ KeyCj(R)).
We have that R is well-typed and vars(R r ) ⊆ vars(R l ).

Proof. Let R = R l → R r be a weakly well-formed API rule and consider a rule R ∈ Var (R). We have that there exists a substitution θ such that R = AC Rθ↓. We can assume w.l.o.g. conclude). Otherwise this would contradict our second hypothesis. Hence we know that t 1 is a variable say that x. We have that σ = {y 2 → t 2 , x → {y 1 } t2 }. Let R = Rσ, we have that R ↓ = AC R ↓ and the two conditions are satisfied.

Narrowing with {dec(y 1 , y 2 )} y2 → y 1 . There exists t ∈ R and σ = mgu AC (t, {dec(y 1 , y 2 )} y2 ). Moreover, we have that t = {t 1 } t2 . We distinguish two cases: either t 1 = dec(t 1 , t 2 ) or t 1 is a variable. Indeed, otherwise unification would not be possible.

t 1 = dec(t 1 , t 2 ). If t 2 = AC t 2 ,
we have that R ↓ = R↓ and we easily conclude. Otherwise, we have that σ ∈ mgu AC (t 2 , t 2 ). Let R = Rσ, we have that R ↓ = AC R ↓. The fact that R satisfies the two conditions is an easy consequence of Lemma 6.

t 1 is a variable, say that x. We have that σ = {x → dec(y 1 , t 2 )}. Let R = Rσ, we have that R ↓ = AC R ↓ and R satisfies the two conditions.

Narrowing with y 1 ⊕ y 1 → 0. By definition, we know that there exists t ∈ R, p ∈ Ō(t) and σ ∈ mgu AC (t| p , y 1 ⊕ y 1 ). Hence, we have that t = AC t 1 ⊕ t 2 and σ ∈ mgu AC (t 1 , t 2 ). Let R = Rσ, we have that R ↓ = AC R ↓ and we easily conclude by using Lemma 6.

The other cases, i.e. narrowing with y 1 ⊕ (y 1 ⊕ y 2 ) → y 2 or y 1 ⊕ 0 → y 1 can be done similarly. Lastly the case of a key conjuring rule can be done similarly.

C.3 Condition 3

Lemma 8 Let S 0 be a set of pure ground facts that is consistent. Let R be a well-formed API rule w.r.t.

S 0 . Let R ∈ Var (R ∪ KeyCj(R)). Let v ∈ KeyTerm(R ) we have that v is checked in R w.r.t. S 0 .
Proof. Let R be a well-formed API rule. We have that R = AC Rθ↓ and we can assume w.l.o.g. that θ is a normalized substitution. We have that

KeyTerm(Rθ↓) ⊆ KeyTerm(R)θ↓ ∪ KeyTerm(θ) = KeyTerm(R)θ↓
The last equality is due to the fact that for all x ∈ vars(R), we have that x ∈ R. Now, let v ∈ KeyTerm(R ). We have to show that v is checked in R w.r.t. S 0 . We know that there exists v ∈ KeyTerm(R) such that vθ↓ = AC v . Moreover, by hypothesis, we know that v is checked in R. Hence there exists v 1 , . . . , v such that v = Xor v 1 ⊕ . . . ⊕ v and for each i,

1 ≤ i ≤ we have that chkOdd(v i ) ∈ S 0 ∪ R or chkEven(v i ) ∈ S 0 ∪ R. For each i such that 1 ≤ i ≤ , let v i = v i θ↓. For each i, 1 ≤ i ≤ we have that chkOdd(v i ) ∈ S 0 ∪ R or chkEven(v i ) ∈ S 0 ∪ R and v = Xor v 1 ⊕ . . . ⊕ v , i.e. v is checked in R w.r.t. S 0 .
A similar reasoning allows us to deal with the case of a rule in KeyCj(R).

This would conclude the proof since u ∈ F n and u = u.

Base Case: The base case u ∈ S is trivial. Indeed, we have that t = t for all t ∈ S and chkX(t) 0 = chkX(t) for all chkX(t) ∈ SatChk(S). This last point is due to the fact that S contains only checks on pure terms of type Base.

Induction

Step: Assume now that there are sets of pure ground facts G 1 , . . . G p such that

G 1 , . . . , G p is a proof of S t for any t ∈ S ∪ F 1 ∪ . . . ∪ F i , chkX(t) 0 ∈ SatChk(S ∪ G 1 ∪ . . . ∪ G p ) for any check chkX(t) ∈ SatChk(S ∪ F 1 ∪ . . . ∪ F i ).
Let us show that we can construct a set of pure ground facts G p+1 such that

G 1 , . . . , G p+1 is a proof of S t for any t ∈ S ∪ F 1 ∪ . . . ∪ F i+1 , chkX(t) 0 ∈ SatChk(S ∪ G 1 ∪ . . . ∪ G p+1 ) for any chkX(t) ∈ SatChk(S ∪ F 1 ∪ . . . ∪ F i+1 ).
The set of ground facts F i+1 is one-step deducible from S ∪ F 1 ∪ . . . F i , thus there exists a weakly well-adapted rule R l new n → R r ∈ A and a ground substitution θ such that It is easy to verify that:

R l θ ⊆ SatChk(S ∪ F 1 ∪ . . . ∪ F i ) and F i+1 = R r θ (modulo AC).
for any pure term v of type Base, vθ ∈ {vθ, 0} and we have that vθ = vθ 0 , for any pure term v of type Cipher, vθ ∈ {vθ, 1}.

Moreover, note that in each case, we have that vθ is a pure ground term of the same type as v.

Let t ∈ R l . We know that t is a pure term and we have that tθ = u for some u ∈ S ∪ F 1 ∪ . . . ∪ F i . Hence, we have that tθ ∈ {u, 0, 1} and we easily deduce that for all term t ∈ R l , we have that

tθ ∈ S ∪ {v | v ∈ F 1 ∪ . . . ∪ F i } ⊆ S ∪ G 1 ∪ . . . ∪ G p .
Let chkX(t) ∈ R l . We know that t is a pure term of type Base and we have that chkX(tθ) = chkX(u) for some chkX(u) ∈ SatChk(S ∪ F 1 ∪ . . . ∪ F i ). Thanks to our induction hypothesis, we deduce that chkX(u)

0 ∈ SatChk(S ∪ G 1 ∪ . . . ∪ G p ) and since chkX(tθ ) = chkX(u 0 ), we easily deduce that chkX(tθ ) ∈ SatChk(S ∪ G 1 ∪ . . . ∪ G p ).
Let G p+1 = R r θ . Note that G p+1 is a set containing only pure ground facts and we have shown that R r θ is one step deducible from S ∪ G 1 ∪ . . . ∪ G p .

INRIA

Let v ∈ F i+1 , we have to show that G 1 , . . . G p+1 is a proof of S v. We know that v is such that v = tθ for some t ∈ R r . In the case where tθ = v, we easily conclude. Otherwise, this means that t is a variable, say that x and xθ has not the same type as x. Since vars(R r ) ⊆ vars(R l ), we know that there exists t ∈ R r such that xθ ∈ st(t θ). Moreover, xθ appears at an impure position in tθ. By using our previous proposition, we easily deduce that

xθ ∈ S ∪ F 1 ∪ . . . ∪ F i and thus xθ ∈ S ∪ {w | w ∈ F 1 ∪ . . . ∪ F i } ⊆ S ∪ G 1 . . . ∪ G p .
This allows us to conclude for the first point.

Let chkX(v) ∈ SatChk(S ∪ F 1 ∪ . . . ∪ F i+1 ), we show chkX(v) 0 ∈ SatChk(S ∪ G 1 ∪ . . . ∪ G p+1 ).
To establish this result, it is sufficient to show that chkX(v) 0 ∈ G p+1 for any chkX(v) ∈ F i+1 .

Let chkX(v) ∈ F i+1 , we know that chkX(v) = chkX(tθ) for some chkX(t) ∈ R r . Since tθ = v 0 and chkX(tθ ) ∈ G p+1 , we easily deduce that chkX(v) 0 ∈ G p+1 .

E A bound on the number of dec terms

Lemma 2 (No illegal dec-term in checks) Let A be a set of well-adapted rules and S be a set of pure ground facts such that no dec terms occurs in KeyTerm(S). Let w be a pure ground term deducible from S and F 1 , . . . , F n be a proof that S A∪Var (I),AC w that involves only pure facts. We assume that there is no dec-term subterm of w. For any term t such that chk(t) ∈ SatChk(S ∪ F 1 ∪ . . . ∪ F n ), for any dec(u, v) subterm of t, the dec-term dec(u, v) is legal.

Assume by contradiction that there exists a dec term dec(u, v) subterm of some term t such that chk(t) ∈ SatChk(S ∪ F 1 ∪ . . . ∪ F j ) with j ≤ n and dec(u, v) is illegal. We consider the minimal index j that satisfies this property. Let R be the rule that has been applied to obtain F j . Since R produces a check, R / ∈ Var (I) thus R is well-adapted. R is of the form

R l (new n) → R r . We must have R l θ ⊆ SatChk(S ∪ F 1 ∪ • • • ∪ F j-1 ) and F j = R r θ. Assume that dec(u, v) is not a subterm of some check in F j while chk(t) ∈ SatChk(S ∪ F 1 ∪ • • • ∪ F j ). It means that dec(u, v) is a subterm of t with chk(t ) ∈ SatChk(S ∪ F 1 ∪ • • • ∪ F j-1
), which contradicts the minimality of j. Thus there exists a term t such that t = wθ and chk(w) ∈ R r .

Since dec(u, v) is a subterm of t , we have t = n. In addition, dec(u, v) must be a strict subterm of t otherwise dec(u, v) would be legal. Since R is well-adapted, there is two cases for w.

1. w = dec(n, w ). In that case we must have that dec(u, v) is a subterm of w θ. In addition w ∈ KeyTerm(w) thus w is checked in R. Since w = n and since there is at most one term (w in our case) in a check in R r , we must have chk(w ) ∈ SatChk(R l ) thus dec(u, v) is a subterm of chk(w θ) ∈ SatChk(S ∪F 1 ∪• • • ∪F j-1 ), which contradicts the minimality of j.

2. w = dec(y, w ). Since wθ = t is a pure term, dec(u, v) is not a subterm of yθ thus dec(u, v) is a subterm of w θ. We conclude the proof like for the first case.

Lemma 3 (Replacement of dec-terms in key position) Let A be a set of well-adapted rules and S be a set of pure ground facts such that no dec terms occurs in KeyTerm(S). Let w be a pure ground term deducible from S and F 1 , . . . , F n be a proof that S A∪Var (I),AC w that involves only pure facts. We assume that there is no dec-term subterm of w. Let t be a term such that t ∈ F j for some 1 ≤ j ≤ n and let p be some key position of t such that t| p = dec(u, v) ⊕ t (t being possibly empty in which case by convention, t| p = dec(u, v)).

Either the term dec(u, v) is legal.

Or F 1 δ (dec(u,v)⊕t ,0) , . . . , F j δ (dec(u,v)⊕t ,0) is a pure proof of S R∪Var (I),AC tδ (dec(u,v)⊕t ,0) . This is proved by induction on j. The base case is straightforward since there is no dec terms occurring in KeyTerm(S). Thus any dec term subterm of S is legal. Let dec(u, v) be an illegal term for F 1 , . . . , F n . Let t be a term in F j such that there is a key position p of t such that t| p = dec(u, v) ⊕ t . Let R be the rule that produces F j . R is of the form R l

(new n) → R r , with R l θ ⊆ SatChk(S ∪ F 1 ∪ • • • ∪ F j-1
) and F j = R r θ with t = wθ and w ∈ R r .

Either R ∈ Var (I). Assume for example that R = x, y → {x} y . Thus F j = {t}. The other cases are similar or simpler. There are two cases.

Either yθ = dec(u, v)⊕t . By induction hypothesis F 1 δ (dec(u,v)⊕t ,0) , . . . , F j-1 δ (dec(u,v)⊕t ,0) is a pure proof of S A∪Var (I),AC xθδ (dec(u,v)⊕t ,0) . Since tδ (dec(u,v)⊕t ,0) = {xθδ (dec(u,v)⊕t ,0) } 0 , we conclude that F 1 δ (dec(u,v)⊕t ,0) , . . . , F j δ (dec(u,v)⊕t ,0) is a pure proof of S A∪Var (I),AC tδ (dec(u,v)⊕t ,0) . Or dec(u, v)⊕t only occurs in key position in xθ or yθ. Since xθ, yθ ∈ S ∪F 1 ∪• • •∪F j-1 we deduce by induction hypothesis F 1 δ (dec(u,v)⊕t ,0) , . . . , F j-1 δ (dec(u,v)⊕t ,0) is a pure proof of S A∪Var (I),AC xθδ (dec(u,v)⊕t ,0) and S A∪Var (I),AC yθδ (dec(u,v)⊕t ,0) . Since we have the equality tδ (dec(u,v)⊕t ,0) = {xθδ (dec(u,v)⊕t ,0) } yθδ (dec(u,v)⊕t ,0) , we conclude that F 1 δ (dec(u,v)⊕t ,0) , . . . , F j δ (dec(u,v)⊕t ,0) is a pure proof of S A∪Var (I),AC tδ (dec(u,v)⊕t ,0) . Or R ∈ R is a well-adapted rule.

Either p is a (key) position of w. Since R is well-adapted, w| p is checked in R which means that chk(t| p ) ∈ SatChk(S ∪ F 1 ∪ • • • ∪ F j-1 ), which contradicts Lemma 2 that ensures that no illegal dec term can occur in a check.

Or for any p such that t| p = dec(u, v) ⊕ t , p is not a position of w. This means that there is a variable x in w and a key position p of xθ such that xθ| p = dec(u, v) ⊕ t . Since R is well-adapted, x must occur in R l .

By induction hypothesis F 1 δ (dec(u,v)⊕t ,0) , . . . , F j-1 δ (dec(u,v)⊕t ,0) is a pure proof of S A∪Var (I),AC t for any term t ∈ R l θδ (dec(u,v)⊕t ,0) .

6 .

 6 Key Part Imp. 3 {r } km⊕imp⊕kp , pin ⊕ data, imp → {r ⊕ data ⊕ pin} km⊕imp chkEven(data ⊕ pin), chkEven(imp), chkOdd(r ) 7. Key Export {pdk} km⊕pin , pin, {r } km⊕exp , → {pdk} r ⊕pin chkOdd(pdk), chkEven(pin) 8. Key Import {pdk} r ⊕imp , data, {r ⊕ data ⊕ pin} km⊕imp → {pdk} km⊕data chkOdd(pdk), chkOdd(r ⊕ data ⊕ pin), chkEven(data) "?" represents inputs that are replaced by random values by the attacker.

Figure 2 :

 2 Figure 2: Bond's Import/Export Attack in our formalism

INRIA

  we have that chkEven(a ⊕ c) ∈ SatChk(S) and also that chkOdd(a ⊕ c) ∈ SatChk(S). Definition 3 (one-step deducible, deducible) Let A be a set of rules of the form R l [new n] → R r and E be an equational theory. Let S be a set of pure ground facts that is consistent. The set of facts F is one-step deducible from S if there exists a rule R l [new n] → R r ∈ A and a ground substitution θ such that R l θ ⊆ SatChk(S) (modulo E), F = R r θ (modulo E), and n is fresh, i.e. n does not occur in S.

u

  where S is the set obtained from S by adding the constants 1 (Cipher) andc 1 , c 2 , c 3 , c 4 (Base), chkOdd(dec(1, c 1 )), chkOdd(c 1 ) chkOdd(dec(1, c 2 )), chkEven(c 2 ) chkEven(dec(1, c 3 )), chkOdd(c 3 ) chkEven(dec(1, c 4 )), chkEven(c 4 )and c 1 , c 2 , c 3 , c 4 do not appear in A, S and u.

  by a derivation of length at most k} INRIA Now the proposition below is an easy consequence of the fact that E API satisfies the finite variant property. Proposition 3 Let A 1 , A 2 be two sets of rules, S be a set of ground facts and s be a ground term (in normal form). S KeyCj(A1) ≤k A1∪A2,E API u if and only if S Var (KeyCj(A1)) ≤k Var (A1∪A2),AC u Moreover, we only need to consider instances of the rules which involve terms in normal form.

Example 10

 10 Let t = dec(a ⊕ b, c) where a, b and c are constant of Base type. The position p in t such that t| p = a ⊕ b is impure. Let t = dec({a} b , c) where a, b and c are constant of Base type. The position p in t such that t| p = {a} b is impure.

S

  KeyCj(A) ≤k A∪I + , E API u ⇔ S KeyCj(A) ≤k A∪I, E API u Proposition 3 gives us S KeyCj(A) ≤k A∪I, E API u ⇔ S Var (KeyCj(A)) ≤k Var (A∪I), AC u Thanks to the well-formedness of the rules in A, we deduce (Proposition 4) that the rules in Var (KeyCj(A)) are well-adapted, the rules in Var (A) are well-adapted, the rules in Var (I) are weakly well-adapted. INRIA Note also that Var (A ∪ I) = Var (A) ∪ Var (I). Now, we apply Corollary 1 and we deduce that if S Var (KeyCj(A)) ≤k Var (A∪I), AC

  Let θ be the substitution defined by xθ = xθ 0 for any x ∈ dom(θ) of type Base, xθ = xθ when xθ is a constant or a nonce of type Cipher and 1 otherwise.

Figure 3 :

 3 Figure 3: Key Conjuring rules of the IBM CCA Key Management Transaction Set

INRIA

  x n → t , . . . , x n are variables, t is a term such that vars(t) ⊆ {x 1 , . . . , x n }, u 1 , . . . , u k are terms of Base type not headed with ⊕,

	x 1
	Encrypt Data:
	chkOdd(dec(y, km ⊕ data)), x, y → {x} dec(y,km⊕data)
	Decrypt Data:
	chkOdd(dec(y, km ⊕ data)), x, y → dec(x, dec(y, km ⊕ data))
	Translate Key:
	chkEven(xtype), x, xtype, y1, y2 → {dec(x, dec(y1, km ⊕ imp) ⊕ xtype)} dec(y2,km⊕exp)⊕xtype
	chkOdd(dec(y1, km ⊕ imp))
	chkOdd(dec(y2, km ⊕ exp))
	chkOdd(dec(x, dec(y1, km ⊕ imp) ⊕ xtype))
	Figure 1: IBM CCA Symmetric Key Management Transaction Set
	where
	RR n 6134	INRIA

RR n 6134

CCA stands for 'Common Cryptographic Architecture', while 4758 is the model number of the HSM. See http://www-3.ibm.com/security/cryptocards/pcicc.shtml

⊕ represents bitwise XOR.RR n 6134

A Off-line key conjuring is useless

Proposition 1 Let A be a set of API rules and S be a set of pure ground facts. We have that S KeyCj(A) ≤k A∪I + ,E API u ⇔ S KeyCj(A) ≤k A∪I∪I + 2 ,E API u where S = S ∪ {c 1 , c 2 , chkOdd(c 1 ), chkEven(c 2 )} and c 1 , c 2 are constants of Base type that do not appear in A, S and u.

Proof. Let F 1 , . . . , F n be a proof of S A1 ≤k A2∪I + ,E API u such that the number p of applications of rules in I + 1 is minimal. Assume p ≥ 1 and consider the first occurrence j in the proof where a rule of I + 1 is used. We assume w.l.o.g. that the rule is

→ dec(n, z), chkOdd(dec(n, z))

There exists a substitution θ such that

), and

Let δ be the substitution that replaces the name n by {c 1 } zθ . We show that F 1 δ, . . . , F n δ be a proof of S A1, ≤k A2∪I + ,E API u. Note that uδ = u.

2. F j = {c 1 , chkOdd(c 1 )} ⊆ S thus F j is deducible from S.

3. Since API rules only contain variables on the left-hand side, it is easy to see that we have that t 1 , . . . , t n → t 1 , . . . , t k is an instance of a rule then t 1 δ, . . . , t n δ → t 1 δ, . . . , t k δ is an instance of the same rule. We deduce that F i is deducible from S for any j < i ≤ n.

We obtain a proof of S A1 ≤k A2∪I + ,E API u with k -1 applications of rules in I + 1 , contradiction. We deduce that there exists a proof F 1 , . . . , F n of S A1 ≤k A2∪I + ,E API u that makes no use of rules in

B Getting rid of some equations

Rewriting. A term s rewrites to t by a TRS R, denoted s → R t, if there is l → r in R, p ∈ O(s) and a substitution σ such that s| p = lσ and t = s[rσ] p . A TRS R is terminating if there are no infinite chains t 1 → R t 2 → R . . .. As in [START_REF] Dershowitz | Rewrite systems[END_REF], given a set of rewrite rules R and a set of equations E , rewriting modulo E , is the relation → E \R (others have used → R,E ) defined as follows: s → E \R t iff there INRIA that θ is normalized. Moreover, by using narrowing and rewriting, we obtain a rule R = Rθ↓ that is well-typed. Since vars(R r ) ⊆ vars(R l ), we have that vars(R r θ) ⊆ vars(R l θ). Now, since for all x ∈ vars(R r ) we have that x ∈ R l and θ is normalized, we easily deduce that vars(R r θ) = vars(R r θ↓) and hence vars(R r θ↓) ⊆ vars(R l θ↓). The same kind of reasoning allows us to conlude for a rule R ∈ Var (KeyCj(R)).

C.2 Condition 2

Note that Condition 2 of Definition 9 (well-adapted) is not stable by AC-narrowing, i.e. by computation of the variants (see Example 9). To establish this condition, we have to rely on the fact that weakly well-formed rules satisfy the dec-property.

Definition 10 (dec-property modulo AC) Let T be a set of terms. We say that T has the dec-property modulo AC if

Then by inspecting the algorithm allowing us to compute AC-unifier, we can establish the following lemma.

Lemma 6 Let T be a set of pure terms having the dec property. Let t 1 , t 2 ∈ st(T ) of base type and σ = mgu AC (t 1 , t 2 ). Then T σ↓ has the dec property and contains only pure terms.

We are now ready to prove the following lemma.

Lemma 7 Let R be a weakly well-formed API rule. Let R ∈ Var (R ∪ KeyCj(R)). Let t be a term of type Cipher appearing as a strict subterm position in R, then t is not headed with { } (t is either a nonce, a variable or constant).

Proof. Let R be a well-typed rule such that: if dec(x, t 1 ) and dec(x, t 2 ) are in st(R) then t 1 ↓ = AC t 2 ↓. Given a variable x of type Cipher, we denote by t x the unique term modulo AC (when it exists) such that dec(x, t x ) ∈ st(R). a term t of type Cipher appearing as a strict subterm position in R↓ is not headed with { } .

Let R be a weakly well-formed API rule. Note that the two conditions are satisfied by R and also by the rules in KeyCj(R). Let R be such that R σ R . We have to show that R satisfies the two conditions above. We have to consider several cases:

Narrowing with dec({y 1 } y2 , y 2 ) → y 1 . By definition, we know that there exists t ∈ R, p ∈ Ō(t) and σ = mgu AC (t| p , dec({y 1 } y2 , y 2 )). We have that t = dec(t 1 , t 2 ). Note that if t 1 is not a variable, then either t 1 is a nonce and unification would be not possible or t 1 = {t 1 } t 2 with dec({t 1 } t 2 , t 2 ). Either t 2 = AC t 2 and we have that R ↓ = AC R↓ (in such a case we easily

INRIA

C.4 Condition 4

Lemma 9 Let R be a well-formed API rule and R kc ∈ KeyCj(R). Let R ∈ Var (R kc ). We have that R = R l new n → R r and {t | chkX(t) ∈ R r } {n} = {u}. Moreover, we are in one of the following three cases:

n occurs in R l (and hence the rule R is useless).

Proof. Let R be a well-formed API rule and

First of all note that R kc satisfies one of the two first conditions. Now, let R ∈ Var (R kc ), we have that there exists θ (we can assume w.l.o.g. that θ is normalized) such that R = R kc θ↓. It is easy to see that there is at most one chkX(u) ∈ R r with u = n. Let {u} = {t | chkX(t) ∈ R r kc } {n}. Now it remains to show that we are in one of the three cases:

Either u = dec(n, u ). In such a case, we have that uθ↓ = dec(n, u θ↓) and we easily conclude.

Or u = dec(y, n ⊕ u ). We have already shown that R contains only pure terms (Lemmas 5 and 7). Hence, if uθ↓ is headed with dec, either we are in one of the two first cases or n ∈ img(θ). Since for all x ∈ R kc , we have that x ∈ R l kc , we deduce that n ∈ R l kc θ↓. Now, assume that uθ↓ is not headed with dec. This means that yθ = {t} (n⊕(u θ))↓ for some term t. Hence we have that uθ↓ = t. In such a case, we have also that n ∈ img(θ) and for the same reason as before we easily deduce that n ∈ R l kc θ↓.

D Existence of a pure attack

Lemma 1 Let A be a set of weakly well-adapted rules and S be a set of pure ground facts that is consistent and which contains 0. Let u be a ground term deducible from S and F 1 , . . . , F n be a proof that S A,AC u. Let p be an impure position of u. We have that

Proof. The proof is by induction on the number of steps needed to obtain u. Note that u| p must be ground since u is ground.

Base case: u ∈ S. Since S only contains pure terms, we must have p = Λ, thus u| p ∈ S. Induction step: Otherwise, we have that there exists a weakly well-adapted rule R l new n → R r and a ground substitution θ such that R l θ ⊆ SatChk(S ∪ F 1 ∪ . . . ∪ F n-1 ) and u ∈ F n = R r θ (modulo AC). Let p be an impure position in u.

either p = Λ and in such a case we have that u| p ∈ S ∪ F 1 ∪ . . . ∪ F n , INRIA or u| p is a strict subterm of u. Since R l new n → R r is a weakly well-adapted rule, u| p must be a subterm of xθ for some variable x ∈ R r . Since vars(R r ) ⊆ vars(R l ), we have that there exists t ∈ R l such that tθ ∈ S ∪ F 1 ∪ . . . ∪ F n-1 and u| p ∈ st(tθ). Moreover, we can easily check that u| p appears at an impure position in tθ. By induction hypothesis, we deduce that u| p ∈ S ∪ F 1 ∪ . . . ∪ F n-1 and thus u| p ∈ S ∪ F 1 ∪ . . . ∪ F n .

Proposition 5 Let A be a set of weakly well-adapted rules and S be a set of pure ground facts that is consistent and which contains 0. Let u be a pure ground term. If S A,AC u then there is a proof of S A,AC u which only involve pure terms.

We define the function • over ground terms that replaces any term at an impure position by 0 (neutral element of ⊕) or 1 (constant of type Cipher). More formally • is inductively defined as follows:

where • 0 are defined by: The functions • 0 and • are extended to sets of facts as expected. Moreover, the function • 0 is also defined on checks as follows:

chk X (t) 0 = chk X (t 0 ).

Proof. Consider a proof F 1 , . . . , F n of S u. We show by induction on n that we can construct sets G 1 , . . . , G p which only involve pure facts such that G 1 , . . . , G p is a proof of S t for any t ∈ S ∪ F 1 ∪ . . . ∪ F n , chkX(t) 0 ∈ SatChk(S ∪ G 1 . . . ∪ G p ) for any chkX(t) ∈ SatChk(S ∪ F 1 ∪ . . . ∪ F n ).


M Ščepanskis

A Jakovičs

K Thomsen

T Beinerts

M Sarma

P Vontobel

R Nikoluškins

A Bojarevičs

Dynamic Neutron Radiography for Liquid Metal Applications

Keywords: neutron radiography, liquid metal, particle laden flow, permanent magnets, stirrer

Due to the non-transparency of metals it is nearly impossible to observe how inclusions behave within a liquid metal. At the same time numerical models, which generally are powerful tools for design of different types of metallurgical and other equipment associated with liquid metal, usually contain a high number of degrees of freedom due to the complexity of turbulent flows. Therefore, experimental verification of the numerical models is an essential task, which was hitherto not satisfactorily solved by established technologies. This contribution presents a recent and break-through experimental method, which makes liquid metal transparent: dynamic neutron radiography. It allows to visualize dynamics of solid inclusions in liquid metal flows within a scaled-down equipment, keeping fixed non-dimensional hydrodynamic and electromagnetic parameters and applying a permanent magnets technology for electromagnetic agitation in the set-up. Such method allows to step forward in understanding two-phase liquid metal flows as well as ensure innovative experiments for improvements in metallurgical equipment, bubbly liquid metal columns, preparation of metal matrix nanocomposites and others.

Introduction

Improvement of melt quality is one of the highest priorities in metallurgical processes. The structure and properties of the final product can be radically changed by adding particles to the melt, e.g., admixture of carbon and chromium to iron prevent movement of dislocations and increase tensile strength of the alloy. Due to the non-transparency of metals it is nearly impossible to observe how the solid inclusions behave within the liquid metal. At the same time numerical models, which generally are powerful tools for studying inclusions in melts, usually contain a high number of degrees of freedom due to the complexity of turbulent flows of liquid metal. Therefore, experimental verification of the numerical models is an essential task, which was not satisfactorily solved till nowadays. Furthermore, the development of admixing technology requires better understanding of the structure of the flow, the velocities of the flow and peculiarities of the particle behavior.

The most of the experimental methods developed for the classical transparent flows like the Particle Image Velocimetry (PIV), optical methods, are apparently not applicable for liquid meals. At the same time, electromagnetically (EM) governed liquid metal flows form a very specific class of turbulent flows, which cannot be reproduced by any transparent liquid [1]. This is a very significant difference between the classical fluid engineering and liquid metal technologies, which makes the task of experimental investigation of liquid metal flows much more challenging. Nevertheless, scientists made significant steps forward during the last few decades, a significant number of experimental techniques like ultrasonic Doppler shift method [2,3], the potential probes [4,5] and others have been developed for single phase liquid metals. However, despite some recent attempts to perform verification of two-phase liquid metal models [1,6], no established experimental technique, which is suitable for industrial usage, is known. It should be additionally mentioned that the classical X-ray radiography in heavy metals is significantly limited due to attenuation coefficient proportional to an atomic number and is likely impossible for turbulent liquid metal flows. The authors carried out a dynamic neutron radiography experiment on visualization of solid inclusion motion in liquid gallium, which seems to be promising method for verification of numerical models and for direct industrial application as well. The first known neutron radiography of a two-phase liquid metal flow was performed by Saito et al. in 2004 [7]. Rising gas bubbles were visualized in the Pb-Bi eutectic. However, the flow was initiated only by the rising bubbles without electromagnetic stirring; therefore, intensity of the flow was low. Thus, the present experiment can be considered as a significant step forward.

Experimental method

The experiment, which is reported in the present paper, was done at the internationally available user facility Swiss Spallation Neutron Source (SINQ) in Paul Scherrer Institute (Villigen, Switzerland). SINQ is presently the world's highest flux accelerator-based continuous neutron spallation source. It is situated at the end of a cascade of three accelerators that deliver a proton beam of 590 MeV at a current up to 2.4 mA. The spallation target is an array of lead rods that produce a continuous neutron flux of about 1 e+14 n/cm 2 /s. Instruments are extracting neutrons by evacuated flight tubes and neutron guides from the D 2 O moderator tank or a liquid D 2 cold source. Neutron imaging at SINQ is available at two main facilities: NEUTRA and ICON. The fist one is more suitable for the present goal. The thermal neutron transmission radiography facility (NEUTRA) features an evacuated neutron flight-tube looking through a 20 mm diameter pinhole into the heavy water SINQ moderator tank. It allows neutron radiography and tomography images of medium to large size objects using a thermal neutron energy spectrum. Neutron energy at this facility is about 25 meV; the neutron flux depends on the proton current delivered to SINQ and is not more than 5e6 neutrons cm-2 sec-1 mA-1 (p-current) at the sample position. The primary detection reactions for thermal neutrons are based on neutron capture by an absorbing material subsequently emitting charged particles. A scintillator screen (e.g., 200 μm thick Li 6 doped ZnS) produces light when excited by ionizing radiation. This light is reflected perpendicularly to the neutron beam direction while neutrons pass through the mirror, which is installed in 45° to the direction of the neutron beam. The reflected light is recorded by a CCD or a CMOS camera. As a standard, an Andor Neo sCMOS pixel detector is used in NEUTRA.

Apparently, there are some limitations for an experimental set-up suitable for a neutron radiography experiment. In order to choose a proper metal for the experiment two properties should be considered: 1) low melting temperature to avoid heating close to a detector and a camera that should be situated as close to the vessel as possible; 2) the attenuation of the neutrons (see [8]). It becomes clear that low temperature eutectics, which contain cadmium (Cd) and indium (In), such as Wood's metal and Galinstan, cannot be used due to high values of the attenuation coefficients. Bismuth (Bi) is also unwanted because it can be activated in the neutron beam and tiny amounts of polonium (Po) can appear. For these reasons we chose gallium (Ga), which is acceptable for neutron radiography and has a suitable melting temperature (30 °C). The material properties of the inclusions used for the neutron radiography experiment have to fulfil various requirements. The attenuation coefficient of the particles cannot be in the same range as that of the liquid metal otherwise they will be invisible. Therefore, the typical SiO 2 , ZrO 2 and Al 2 O 3 oxides are useless here. Boron carbide (B 4 C), which has a very high attenuation coefficient, was found to be good for the experiment. However, due to its low density (2.52 g/cm3) and the very low size of available particles, it was a significant problem to mix such a powder from the surface into the metal. Therefore, special composite particles, which consisted of a lead (Pb), gadolinium oxide (Gd 2 O 3 ) and glue were fabricated. Combination of these materials allows to control density and contrast of the particles. The metallurgical equipment apparently should be scaled-down. First of all, the width of the vessel is limited by the width of the neutron beam, which is less than 20 x 20 cm at NEUTRA middle position with stronger aberrations at the periphery. The third size of the examined vessel should be optimized with respect to the beam attenuation by the liquid metal. The dynamic neutron imaging at the existing facilities is available only as 2D shadow images while tomography (3D imaging) is available for static objects. Thus, the liquid metal vessel and the flow inside should be optimized for 2D imaging. Taking into account the mentioned aspects, a rectangular vessel of window glass, inner size 10 x 10 x 3 cm, was built for the experiment.

Taking into account the already mentioned limitation for materials in the way of the neutron beam, designing of an EM environment of the experimental set-up should be carefully considered. Usually EM stirrers have an inductor of alternating current around the liquid metal vessel to ensure mixing. However, the cupper inductor usually is water cooled, that means it is designed as a tube to conduct water inside. Water, which contains hydrogen, has high attenuation coefficient; therefore, it should be avoided in the way of the neutron beam. Theoretically, it should be possible to design the cooling system using liquid metal or another material, which is transparent for neutrons, but such designs are untypical for the metallurgical industry and, consequently, will be very expensive.

Modern permanent magnet technology seems to be a quite nice solution for this problem. It is possible to design a system of rotating permanent magnets in a way to create the same flow structure as in the case of an inductor. The paper Fig. 1 The experimental set-up [9] can be referenced here. Generally, it should be pointed out that the permanent magnet technology proved very essential for our neutron radiography application to metallurgical flows and is a significant innovation of the present experiment.

Taking into account all aspects mentioned in this section, a design, which contains counter-rotating cylindrical magnets, was chosen (see Fig. 1). Such a design allows sparing a high frequency generator and an inductor; however, an additional mechanical system, including gears, belts and bearings, had to be built to ensure the rotation of the magnets.

Results

This section contains the results of the first and the second dynamic neutron radiography experiments in an intense EM induced liquid metal flow, which were performed in July of year 2014 and 2015 respectively at Paul Scherrer Institute, SINQ, NEUTRA. These results generally demonstrate the potential of the method, but do not exhaust it due to possible improvements.

The results of the measurements were obtained as a set of neutron shadow images; some of them can be seen in Fig. 2. Two different exposure times were used -0.01 s and 0.1 s: shorter exposure makes it possible to see separate particles in the flow and was used to create a particle concentration field, but longer exposure shows the trajectories of particles and, consequently, visualizes the structure of the flow as well as it allows to calculate the velocities of the inclusions. Velocity can be calculated also using standard PIV procedure. It should be mentioned that the camera and its environment at the first experiment supported only 1 fps effective imaging frequency. The velocities and frequencies of oscillations of the flow were so high that the frame rate was the limiting factor for postprocessing of the results, i.e. it was not possible to unambiguously follow the same particle in two consecutive frames. This problem was solved in the second experiment, a new camera allows 32 fps frame rate, which makes possible to use PIV technique and software for the analysis. This work is in progress now.

Nevertheless, by doing time consuming image processing work it was possible to evaluate the admixing of particles in the fluid and the average velocities of the particles in the flow even using the results of the first experiment. Maximal concentration of the particles as a function of magnet revolutions is shown in Fig. 3 (a). The noticeable step structure could not be easily explained and required time consuming numerical simulation of the process, which is in progress now. Bojarevics & Beinerts presented an analytical expression for a magnetic field and an iterative solution for the flow velocity in the limit of a two-dimensional model as well as experimental measurements of the velocity in a liquid metal stirrer based on rotating permanent magnets [START_REF] Bojarevics | [END_REF]. This analytical method is used in this work for the estimation of the flow velocity in the present set-up. The average particle velocity in the liquid metal as a function of magnet rotation speed is shown in Fig. 3 (b). The experimental curve in this figure was obtained by using images with longer exposure time (Fig. 2 (a)), which allowed to see particle paths. The velocity of particles was calculated by dividing the length of its path with the exposure time (0.1 s). The results are presented in Fig. 3 (b) as a function of magnet revolution speed. Comparing analytical predictions of the flow with the experimental results, it must be noted that the velocities found analytically are definitely higher than those of particles in the experiment even taking into account the huge errors of the experimental results. This fact seems to be easily explained by inertial effects due to the big size of the inclusions.

Conclusions and further perspectives

The present paper discussed neutron radiography as the promising method for experimental investigation of twophase liquid metal flows and verification of proper numerical models, which are essential issues for liquid metal applications. The possibilities of such method are demonstrated on the example of a scaled-down stirrer, which has been designed using permanent magnet technologies in a way to ensure the same flow structure as in an ICF. The rotation speed of the permanent magnets determines the flow velocity, which is tuned to ensure the same Reynolds number as in the original metallurgical equipment. Time-averaged concentration field and flow velocities as functions of magnet rotation speed are demonstrated as quantitative results of the experiment.

It is possible to establish the neutron particle image velocimetry (NeuPIV) method by using high speed camera. Generally, the results of the two experiments demonstrated potential of the method. It allows deeper understanding of two-phase processes in liquid metal technologies like behavior of alloying inclusions in bulk of a melt, entrapment of slag, bubbly flow in liquid metal columns, micro-and submicro-particle embedding in metal lattice during metal matrix nanocomposite production. Such experimental method in combination with numerical models opens a door for better optimization of equipment and processes as well as new technologies and innovation in metallurgy. Limits of the method for different applications should be further investigated.

Fig. 2

 2 Fig. 2 Examples of neutron images: (a) rotation of the magnets -35.3 rps, exposure time -0.1 s; (b) 35.3 rps, 0.01 s; (c) example of slag entrapment visualization. Figures (a) and (b) corresponds to the first experiment [10]. a b