Marcella Autran
email: marcella@pet.coppe.ufrj.br

Burlier Drummond

Amaranto Lopes Pereira
email: amaranto@pet.coppe.ufrj.br

Félix Mora-Camino

A global model for long term planning of multimodal freight transportation systems

Keywords: freight flows, transportation networks, bi-level programming

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

In this communication is considered the problem of long term forecasting of freight traffic growth in a large transportation network. This problem is crucial when planning the necessary investments in terminals, transportation links and fleets. One of the main difficulty of this task is related with the estimation of future demand over the network which has direct influence on the operational conditions and costs. The proposed approach makes use of two different optimization models: One model is devoted to demand forecasting, the other one defines the global transport supply according with a profit maximization behavior for the whole transport sector operating in this area. The freight demand forecasting process is based a new entropy maximization approach to determine the distribution of origin-destination matrices. The supply optimization model considers simultaneously two classes of flows: vehicle flows providing transportation capacity and freight flows generating revenues to the transportation operators. Hence, no classical flows in networks optimization technique is available to solve this problem while two level solution techniques considering vehicle flows at the first level and passengers/freight flows at the second level can be considered. A global optimization problem is associated to a full scenario with respect to demand and operations costs. Each of the optimization problems, taken separately is convex, however, the whole problem, through the global definition of the revenue and of a cost constraint is non convex. A proposed solution schemes is composed of an iterative process between the current solutions of the demand and the supply optimization problems: the entropy maximizing/minimum freight distribution cost problems provides the freight origin-destination matrices given a fare structure, while the supply optimization problem provides the fare structure given passengers/freight origin-destination matrices. To enforce convergence while maintaining convexity of the two problems, the effective-potential demand level constraints of the supply optimization problem are modified.

2.DISTRIBUTION OF FREIGHT DEMAND

To perform the prevision of freight demand, it is supposed that a priori trip distribution is available:

{ } N i O i ..., , 1 , ∈ and { } N j D j ..., , 1 , ∈ (1)
We consider that the demand for a given origin destination i-j and for a given modality m is such that there exists a positive constant m ij λ with :

) / ( ) ( ∑ ∈ - - = M n ij ij m ij n ij n ij m ij m ij e e T T π λ π λ π (2)
where m ij π is the mean freight fare between i and j with modality m. Considering that the potential origin and destination levels are

{ } N i O i ..., , 1 , ∈ and { } N j D j ..., , 1 , ∈
, we have the following constraints:

∑ ≠ = = = ∑ ∈ - = - ∑ ∈ N i j j N to i i O M n n ij n ij e i O m ij ij e ij T M m m , 1 1 ) ( π λ π λ (3-1) ∑ ≠ = = = ∑ ∈ - = - ∑ ∈ N j i i N to j j D M n n ij n ij e j D m ij ij e ij T M m m , 1 1 ) ( π λ π λ (3-2)
The demand distribution estimation problem is taken here as a constrained entropy maximization problem. Then to a choice of an instance

I={[ m ij T ˆ], { } N i O i ..., , 1 , ∈ , { } N j D j ..., , 1 , ∈
} is associated the following maximization problem, Problem D:

∑ ∑ = ≠ =       - N i N i j j ij ij ij T T Ln T 1 , 1 / max (4) under constraints (3-1), (3-2) and j i N to j N to i T ij ≠ = = ≥ , 1 , 1 , 0 (5)
The adopted optimization criteria, a conditional entropy function, is representative of the global distortion between the a priori and the predicted demand distributions. The above optimization problem being convex it is useful to introduce the Lagrangian associated to this problem :

( ) ∑ ∑ ∑ ∑ ∑ ∑ ∑ ∑ = ≠ = - ∈ = ≠ = - ∈ = ≠ = - + - + - = N j N j i i j ij M m j N i N i j j i ij M m i N i N i j j ij ij ij ij D e T O e T T T Ln T L m ij m ij m ij m ij 1 , 1 1 , 1 1 , 1 ) ( ) ( / π λ π λ β α (6)
The first order optimality conditions are such as :

0 / = ∂ ∂ ij T L j i N to j N to i ≠ = = , 1 , 1 (7)
or :

j i N to j N to i m ij m ij e j m ij m ij e i M m ij T ij T Ln ≠ = = = + ∈ + - - ∑ , 1 , 1 0 ) ( ) / ( 1 π λ β π λ α (8)
Then the solution is such as :

j i N to j N to i m ij m ij M m j i e ij ij e T T ≠ = = ∑ ∈ + + - = , 1 , 1 ) ( 1 ( * ˆπ λ β α (9)
The dual variables are such as:

N to i i O j i ij p N i j j ij 1 ) ( , 1 = = + ∑ ≠ = β α ρ (10) N to j j D j i ij p N j i i ij 1 ) ( , 1 = = + ∑ ≠ = β α ρ (11)
where

) 1 ( ˆ-∈ = ∑ m ij m ij M m e ij T ij π λ ρ and n ij ij e ij e p π λ = (12)
The numerical solution of an instance of Problem D can be obtained using an extension of the Furness algorithm. Linear convex algorithms such as the Simplex-Convex or the Frank-Wolfe algorithms [START_REF] Assad | Multicommodity network flows-a survey[END_REF] appears to be very cumbersome in computational terms. Another interesting direction for numerical resolution is through the solution of the geometric primal associated to this problem [START_REF] Mora-Camino | Introduction à la Programmation Géométrique[END_REF].

ASSIGNMENT OF FREIGHT FLOWS

The different vehicle flows along each network provide the physical support for the freight flows. Then considering that [ m ij φ ] are the freight flows over the network corresponding to transportation mode m, they obey to the following capacity constraints :

M m G j i f m m ij m ij ∈ ∈ ≤ ≤ , ) , ( 0 φ σ φ (13) where [ m ij f ] is the flow of vehicles of the m th modality over G m, φ
σ is a scaling factor. For each origin-destination pair a set of concurrent paths composed of a succession of links is retained according to directness criteria for freight:

{ } m M m n ij ij G j i n to n Ch Ch ∈ ∪ ∈ = = ) , ( 1 , max (14)
Here it is considered that demand for a given O-D pair, is assigned to these possible paths according with the available capacities. This approach is acceptable when available capacity is close to demand levels. Let [β(i,j,n,k,l,m) ] be the incidence matrix between path Ch n ij and arc (k,l) of G m : β(i,j,n,k,,l,m) = 1 if (k,l)∈ Ch n ij β(i,j,n,k,l,m) = 0 else. Then the flow of freight between vertices i and j is given by :

( ) m M m M m N G l k N n k ij G j i m j i n l k m ij ∈ ∈ ∈ = ∪ ∈ = ∑ ∑ ∑ ) , ( ) , , , , , ( ) , ( 1 ln
θ β φ ( 15
)
where ijn θ is the flow of freight between origin i and destination j using the n th path between them.

The mean freight fare for the i-j origin-destination pair is then given by :

m M m G j i ijn ij N n ijn ij N n n ij ij ∈ ∪ ∈ ∑ = ∑ = = ) , ( ) 1 /( ) 1 ( θ θ π π (16)

TRANSPORTATION SUPPLY MODEL

The proposed model takes into account m+1 types of flows: m vehicle flows according to the different transport modalities and freight flows using the resulting transport capacity. The fleets of vehicles and their operation generate fixed and variable costs, while freight flows are the main source of revenue for the freight transportation sector. To each transportation modality is associated a network linking the N transportation centers such as:

R m = [G m ,[ m ij f ]] ( 17
)
where G m is the graph associated to the m th modality, [ m ij f ] is the flow of vehicles of the m th modality over G m . The different networks some common vertices and links. The flow of vehicles associated to each transportation mode satisfies to conservation and positivity constraints:

M m G i f f m m ik G i j N G j i m ji m m m ∈ ∈ = ∑ ∑ ∈ ∈ , ) , ( ) , ( (18)
0 ≥ m ij f , (i, j) ∈G m m∈M (19)
where N m is the number of vertices of graph G m . Here flows integrity constraints are not taken into account since no scheduling or routing problem will be formulated according to these flows which should only provide a global view of the future development of the multimodal transportation system. However for sake of realism, a fleet capacity constraint can be introduced:

m m m ij N G j i m ij F D d f m m ≤ ∑ ∈ ) , ( M m ∈ (20)
where m ij d is the block time for travel, including departure and arrival activities, between vertices i and j , D m is the average time availability of a vehicle for modality m. It can be also of interest to introduce node capacity constraints related with intermodal stations and terminals:

T t Q f t j i S t G G j i m ij mn M n m n m ∈ ≤ ∑ ∑ ∪ ∈ ∈ ) , ( , ) , , ( (21)
where

t m
Q is the traffic capacity of terminal t, S mn (i, j, t) are incidence matrices between vehicle flows of different transportation modes.

SUPPLY OPTIMIZATION MODEL

Given the distribution of potential demands

] [ * ij T associated to an instance of [ ij T ˆ] , { } N i O i ..., , 1 , ∈ and { } N j D j ..., , 1 , ∈
, as well as to mean transportation fares ) between the different centers and the fares ( mn ij π ) applied to each selected path between the centers. To solve this problem it is also necessary to introduce the effective flows of goods ( ijn θ ) associated to each selected path between the connected centers. The optimization criterion of Problem S is given by:

{ }         + + - + ∑ ∑ ∑ ∑ ∈ ∈ = ∈ ) ( ) 1 /( ) ( max ) , ( ) , ( 1 , , N G j i m ij mcv ij m m cv m cf r G j i N n ijn mn ij M m f m m m ij ij n ij ij f c F c c τ θ π θ π (22)
where τ is a return rate and the m uv c are coefficients related with fixed and variable fleets and flows costs. Problem S must satisfy the following constraints:

M m G i f f m m ik G i j N G j i m ji m m m ∈ ∈ = ∑ ∑ ∈ ∈ , ) , ( ) , ( (23)
M m F D d f m m m ij N G j i m ij m m ∈ ≤ ∑ ∈ ) , ( (24)
( )

M m G j i f m j i n l k m m ij m G l k N n k m ij ∈ ∈ ≤ ∑ ∑ ∈ = , ) , ( ) , , , , , ( ) , ( 1 ln φ
σ θ β ( 25
) T t Q f t j i S t G G j i m ij m M n m m ∈ ≤ ∑ ∑ ∪ ∈ ∈ ) , ( , ) , , ( (26)
[ ]

M m G j i T m ij ij N n ijn m ij ∈ ∈ ≤ ∑ = , ) , ( * 1 π θ (27)
with the positivity conditions: Each of the optimization problems, taken separately is a convex programming problem, however, the whole problem when integrating Problem D through constraint ( 27) is non convex. Then it seems interesting to solve numerically these problems separately and design an interactive process towards equilibrium. In this case, some questions are of interest: -the easiness to solve numerically each of the optimization problems, -the guarantee of convergence of the iterative process towards global solution, -the speed of convergence, -the quality of the limit solution. These three linked problems constitute a non standard bi-level programming problem [START_REF] Dempe | Foundations of bilevel programming[END_REF] where Problem S is the leader's problem while Problem D are the followers' problems. This results from the adoption of a deregulated point of view in which transport

{ } M m G l k N n m m ij k ∈ ∈ ∈ ≥ , ) , ( , ,.., 1 , 0 ln θ (28) M m G j i f m m ij ∈ ∈ ≥ , ) , ( 0 (29) m mn ij G j i ∈ ≥ ) , ( 0 φ π , m ij N n ∈ , M m ∈ (30)

GLOBAL SOLUTION SCHEME

It appears that

Problem S [ m ij f ] [ χ θ ln [ k ] Problem D [ ] χ π ij       * χ ij T
firms operate as a whole the transport network according to their direct economic interest without considering any social surplus. Constraint (27) plays a central role in the articulation of the two optimization levels and the convergence of their solutions towards a common global solution. Since these constraints transmit to the revenue optimization problem the reaction of demand with respect to changes in mean fares between the different origins and destinations, it is useful to makes apparent this effect so that limited fare values will be provided by the solutions of Problem S. However, the relation between origin-destinations flows is quite complex and at least non linear. So, to maintain the convexity of Problem S, these constraints can be replaced by their first order approximation where the reference values are the solutions of the two problems at the previous iteration:

) ( ( ) 1 ( 1 1 1 1 , 1 * ) 1 ( * 1 - - = - = ≠ = - = - ∂ ∂ ∂ ∂ + ≤ ∑ ∑ ∑ ∑ k n lp n lp k N n n lp lp k N l N l p p lp ij k ij N n ijn lm ij T T π π π π π θ ν (31) M m G j i m ∈ ∈ , ) , (
Since the following inequalities are likely:

0 1 * ≤ - ∂ ∂ k ij ij T π ν 0 1 * ≥ - ∂ ∂ k lp ij T π ν π ν ν π ν 1 * 1 * - ∂ ∂ << - ∂ ∂ k ij ij T k lp ij T (32) M m p l A p l G j i m m ∈ ≠ ∈ ∈ , , , , ) , (    - = + - + = ) exp( 0 ) 2 /( ) 1 1 ( k k c k k π λ θ θ λ λ π λ π (45)
It is clear that the limit when k →+ ∞ of (π k , θ k ) is ((1+c λ)/λ, θ 0 e -(1+c λ ). Here, the convergence rate is such as:

) 2 1 1 ( ) 2 / 1 ( - - - - = - k k k k π π π π (46)
Other bi-level schemes have been considered in (Alou et al, 2006) and (Brotcome et al, 2000) for different transportation problems while numerical convergence conditions have been discussed in [START_REF] Scheel | Mathematical programs with equilibrium constraints: stationarity, optimality et sensitivity[END_REF].

CONCLUSION

This communication has considered the problem of long term forecasting of freight transportation in a large network. The proposed approach has introduced two different optimization models: A model devoted to demand forecasting and another one describing a profit maximization supply behavior by transportation firms. The distribution demand forecasting model introduces in a new way elasticity of demand with respect to fares. The supply optimization model considers simultaneously two flows: vehicle flows providing transportation capacity and freight flows generating revenues to the transport operators. Then a global optimization problem is associated to each scenario with respect to demand and operations costs. A solution scheme composed of an iterative process between the current solutions of the demand and the supply optimization problems is proposed: the entropy maximizing problem provides the freight origin-destination matrices given the fare structure, while the supply optimization problem provides the fare structure given freight origindestination matrices. Convergence conditions are discussed for this iterative process between the two levels, which can be seen as inverse of each other.

  optimization of transportation supply (capacities and fares) can be considered: This problem (Problem S) is concerned with the optimization of the global economic performance over a period of time of the multimodal freight transportation network. Here the decision variables are the vehicle flows ( m ij f

  Problems D on one side and Problem S on the other side, are strongly interdependent: while Problem D provides to Problem S potential levels of demand 27) ), Problem S provides mean fare values ] [ ij π to Problems D.

Figure 1 :

 1 Figure 1: Interaction between problems


F Courvoisier
email: francois.courvoisier@femto-st.fr

A Mathis

J Zhang

L Froehly

V Jukna

L Furfaro

M Jacquot

R Giust

C Xie

P A Lacourt

A Couairon

J M Dudley

Filamentation of high-angle nondiffracting beams and applications to ultrafast laser processing

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Filamentation of high-angle nondiffracting beams and applications to ultrafast laser processing

François Courvoisier, Amaury Mathis, Jinggui Zhang, Luc Froehly, V. Jukna, Luca Furfaro, Maxime Jacquot, Remo Giust, Chen Xie, Pierre-Ambroise Lacourt, et al. We have recently developed a novel approach to fabricate controlled high aspect structures using novel Bessel and Airy beams, and this contribution will review our recent work in this field. The key concept behind the use of Bessel and Airy beams in controlled femtosecond fabrication is to control the direction of the incident light field rather than simply shaping the laser intensity pattern in one plane. With Bessel beams, light propagates along a cone and for sufficiently high conical angles, the nonlinear propagation of femtosecond Bessel filaments is stationary [START_REF] Porras | Nonlinear Unbalanced Bessel Beams: Stationary Conical Waves Supported by Nonlinear Losses[END_REF][START_REF] Polesana | Filamentation in Kerr media from pulsed Bessel beams[END_REF]. In this regime, we have reported high aspect ratio (100:1) nanochannels drilled in glass using single femtosecond laser shots [START_REF] Bhuyan | High aspect ratio nanochannel machining using single shot femtosecond Bessel beams[END_REF]. Numerical simulations of the nonlinear propagation of femtosecond Bessel pulses allow us to accurately reproduce the experimental results, confirming that the propagation of Bessel filaments during nanochannel drilling is stationary. In addition, we report extremely high plasma densities, even higher than the optical critical density on long propagation distances, as recently confirmed by others [START_REF] Faccio | Nonlinear light-matter interactions with femtosecond high-angle Bessel beams[END_REF]. This arises because of the very specific Bessel beam conical structure that allows the pulse to propagate with minimal dynamical effects, thus generating a high aspect ratio cylinder of plasma. Airy beams and more generally accelerating beams constitute another family of beams that possess quasinondiffracting behaviour. Their primary intensity lobe propagates along a curved trajectory that can be arbitrarily shaped [START_REF] Greenfield | Accelerating light beams along arbitrary convex trajectories[END_REF][START_REF] Froehly | Arbitrary accelerating micronscale caustic beams in two and three dimensions[END_REF] (Fig. 1(c)). These beams can be described and designed conveniently using the notion of optical caustics and the tools of mathematical catastrophe theory, and we have recently applied this to generate femtosecond beams accelerating on non-paraxial circular trajectories [START_REF] Courvoisier | Sending femtosecond pulses in circles: highly non-paraxial accelerating beams[END_REF]. Significantly, the region of maximal intensity in accelerating beams is adjacent to a region where no light propagates. This has been used for direct curved edge profiling of silicon and diamond (Fig. 1(d)) [START_REF] Mathis | Micromachining along a curve: Femtosecond laser micromachining of curved profiles in diamond and silicon using accelerating beams[END_REF]. In addition, Airy accelerating beams also exhibit stationary propagation as demonstrated by other groups in the paraxial regime [START_REF] Lotti | Stationary nonlinear Airy beams[END_REF] and we expect this has important applications in the control of light propagation with high acceleration and applications to nanoprocessing of curved channels.

To cite this version:

As a conclusion, our results show that the control of energy deposition in materials with stationary filaments is a key new approach for technological applications and provides access to novel regimes of intense light-matter interaction on long distances and small diameters.

François Courvoisier ,Fig. 1 (

 Courvoisier1 Fig. 1 (a) Conical structure of a Bessel beam generating a uniform dense plasma at its center. (b) Through channel drillled in glass by a single Bessel shot. Blue and red curves show the plasma density iso-contours at the plasma critical density and threshold density for ablation obtained numerically.(c) 3D iso-intensity surfaces at 5%(gold) and 50%(red) of a beam accelerating on a circular trajectory. (d) typical results of edge profiling with circularly accelerating beams.


Pablo Rauzy

Sylvain Guilley

A Formal Proof of Countermeasures Against Fault Injection Attacks on CRT-RSA

Keywords: RSA (Rivest, Shamir, Adleman [RSA78]) CRT (Chinese Remainder Theorem) fault injection BellCoRe

In this article, we describe a methodology that aims at either breaking or proving the security of CRT-RSA implementations against fault injection attacks. In the specific case-study of the BellCoRe attack, our work bridges a gap between formal proofs and implementation-level attacks. We apply our results to three implementations of CRT-RSA, namely the unprotected one, that of Shamir, and that of Aumüller et al. Our findings are that many attacks are possible on both the unprotected and the Shamir implementations, while the implementation of Aumüller et al. is resistant to all single-fault attacks. It is also resistant to double-fault attacks if we consider the less powerful threat-model of its authors.

Introduction

It is known since 1997 that injecting faults during the computation of CRT-RSA could yield to malformed signatures that expose the prime factors (p and q) of the public modulus (N = p • q). Notwithstanding, computing without the fourfold acceleration conveyed by the CRT is definitely not an option in practical applications. Therefore, many countermeasures have appeared that consist in step-wise internal checks during the CRT computation. To our best knowledge, none of these countermeasures have been proven formally. Thus without surprise, some of them have been broken, and then patched. The current state-ofthe-art in computing CRT-RSA without exposing p and q relies thus on algorithms that have been carefully scrutinized by cryptographers. Nonetheless, neither the hypotheses of the fault attack nor the security itself have been unambiguously modeled. This is the purpose of this paper. The difficulties are a priori multiple: in fault injection attacks, the attacker has an extremely high power because he can fault any variable. Traditional approaches thus seem to fall short in handling this problem. Indeed, there are two canonical methodologies: formal and computational proofs. Formal proofs (e.g., in the so-called Dolev-Yao model) do not capture the requirement for faults to preserve some information about one of the two moduli; indeed, it considers the RSA as a blackbox with a key pair. Computational proofs are way too complicated (in terms of computational complexity) since the handled numbers are typically 2, 048 bit long.

The state-of-the-art contains one reference related to the formal proof of a CRT-RSA implementation: it is the work of Christofi, Chetali, Goubin and Vigilant [START_REF] Christofi | Formal verification of an implementation of CRT-RSA Vigilant's algorithm[END_REF]. For tractability purposes, the proof is conducted on reduced versions of the algorithms parameters. One fault model is chosen authoritatively (the zeroization of a complete intermediate data), which is a strong assumption. In addition, the verification is conducted on a pseudo-code, hence concerns about its portability after its compilation into machine-level code. Another reference related to formal proofs and fault injection attacks is the work of Guo, Mukhopadhyay, and Karri. In [START_REF] Guo | Provably secure concurrent error detection against differential fault analysis[END_REF], they explicit an AES implementation that is provably protected against differential fault analyses [START_REF] Biham | Differential Fault Analysis of Secret Key Cryptosystems[END_REF]. The approach is purely combinational, because the faults propagation in AES concerns 32-bit words called columns; consequently, all fatal faults (and thus all innocuous faults) can be enumerated.

Contributions. Our contribution is to reach a full fault coverage of the CRT-RSA algorithm, thereby keeping the proof valid even if the code is transformed (e.g., compiled or partitioned in software/hardware). To this end we developed a tool called finja1 based on symbolic computation in the framework of modular arithmetic, which enables formal analysis of CRT-RSA and its countermeasures against fault injection attacks. We apply our methods on three implementations: the unprotected one, the one protected by Shamir's countermeasure, and the one protected by Aumüller et al.'s countermeasure. We find many possible fault injections that enable a BellCoRe attack on the unprotected implementation of the CRT-RSA computation, as well as on the one protected by Shamir's countermeasure. We formally prove the security of the Aumüller et al.'s countermeasure against the BellCoRe attack, under a fault model that considers permanent faults (in memory) and transient faults (one-time faults, even on copies of the secret key parts), with or without forcing at zero, and with possibly faults at various locations.

Organization of the paper. We recall the CRT-RSA cryptosystem and the BellCoRe attack in Sec. 2; still from an historical perspective, we explain how the CRT-RSA implementation has been amended to withstand more or less efficiently the BellCoRe attack. Then, in Sec. 3, we define our approach. Sec. 4, Sec. 5, and Sec. 6 are case studies using the methods developed in Sec.

CRT-RSA and the BellCoRe Attack

This section recaps known results about fault injection attacks on CRT-RSA (see also [Koc ¸94] and [START_REF]Introduction to Hardware Security and Trust[END_REF]Chap. 3]). Its purpose is to settle the notions and the associated notations that will be used in the later sections (that contain novel contributions).

CRT-RSA

RSA is both an encryption and a signature scheme. It relies on the identity that for all message 0 ≤ m < N, (m d ) e ≡ m mod N, where d ≡ e -1 mod ϕ(N), by Euler's theorem. In this equation, ϕ is Euler's totient function, equal to ϕ(N) = (p -1) • (q -1) when N = p • q is a composite number, product of two primes p and q. For example, if Alice generates the signature S = m d mod N, then Bob can verify it by computing S e mod N, which must be equal to m unless Alice is pretending to know d although she does not. Therefore the pair (N, d) is called the private key, while the pair (N, e) is called the public key. In this paper, we are not concerned about the key generation step of RSA, and simply assume that d is an unknown number in 1, ϕ(N) = (p -1) • (q -1) . Actually, d can also be chosen equal to the smallest value e -1 mod λ (n), where λ (n) = (p-1)•(q-1) gcd(p-1,q-1) is the Carmichael function. The computation of m d mod N can be speededup by a factor four by using the Chinese Remainder Theorem (CRT). Indeed, figures modulo p and q are twice as short as those modulo N. For example, for 2, 048 bit RSA, p and q are 1, 024 bit long. The CRT-RSA consists in computing S p = m d mod p and S q = m d mod q, which can be recombined into S with a limited overhead. Due to the little Fermat theorem (special case of the Euler theorem when the modulus is a prime), S p = (m mod p) d mod (p-1) mod p. This means that in the computation of S p , the processed data have 1, 024 bit, and the exponent itself has 1, 024 bits (instead of 2, 048 bits). Thus the multiplication is four times faster and the exponentiation eight times faster. However, as there are two such exponentiations (modulo p and q), the overall CRT-RSA is roughly speaking four times faster than RSA computed modulo N.

This acceleration justifies that CRT-RSA is always used if the factorization of N as p • q is known. In CRT-RSA, the private key is a more rich structure than simply (N, d): it is actually comprised of the 5-tuple (p, q, d p , d q , i q ), where:

• d p . = d mod (p -1), • d q . = d mod (q -1), • i q .
= q -1 mod p. The unprotected CRT-RSA algorithm is presented in Alg. 1. It takes advantage of the CRT recombination proposed by Garner in [START_REF] Harvey | Number Systems and Arithmetic[END_REF]. It is straightforward to check that the signature computed at line 3 belongs to 0, p • q -1 . Consequently, no reduction modulo N is necessary before returning S.

Algorithm 1: Unprotected CRT-RSA Input : Message m, key (p, q, d p , d q , i q ) Output: Signature m d mod N

1 S p = m d p mod p /* Signature modulo p */ 2 S q = m d q mod q /* Signature modulo q */ 3 S = S q + q • (i q • (S p -S q ) mod p) /* Recombination */ 4 return S

BellCoRe Attack on CRT-RSA

In 1997, an dreadful remark has been made by Boneh, DeMillo and Lipton [START_REF] Boneh | On the Importance of Checking Cryptographic Protocols for Faults[END_REF], three staff members of BellCoRe: Alg. 1 could reveal the secret primes p and q if the computation is faulted, even in a very random way. The attack can be expressed as the following proposition.

Proposition 1 (Orignal BellCoRe attack). If the intermediate variable S p (resp. S q ) is returned faulted as S p (resp. S q )2 , then the attacker gets an erroneous signature S, and is able to recover p (resp. q) as gcd(N, S -S) (with an overwhelming probability).

Proof. For all integer x, gcd(N, x) can only take 4 values:

• 1, if N and x are coprime,

• p, if x is a multiple of p but not of q, • q, if x is a multiple of q but not of p,

• N, if x is a multiple of both p and q, i.e., of N.

In Alg. 1, if S p is faulted (i.e., replaced by S p = S p ), then S -S = q • ((i q • (S p -S q ) mod p) -(i q • ( S p -S q ) mod p)), and thus gcd(N, S -S) = q.

If S q is faulted (i.e., replaced by S q = S q ), then S -S ≡ (S q -S q ) -(q mod p) • i q • (S q -S q ) ≡ 0 mod p because (q mod p) • i q ≡ 1 mod p. Thus S -S is a multiple of p. Additionally, S -S is not a multiple of q. So gcd(N, S -S) = p.

In both cases, the greatest common divisor could yield N. However, (S -S)/q in the first case (resp. (S -S)/p in the second case) is very unlikely to be a multiple of p (resp. q). Indeed, if the random fault is uniformly distributed, the probability that gcd(N, S -S) is equal to p (resp. q) is negligible3 . This version of the BellCoRe attack requires that two identical messages with the same key can be signed; indeed, one signature that yields the genuine S and an other that is perturbed and thus returns S are needed. Little later, the BellCoRe attack has been improved by Joye, Lenstra and Quisquater [START_REF] Joye | Chinese Remaindering Based Cryptosystems in the Presence of Faults[END_REF]. This time, the attacker can recover p or q with one only faulty signature, provided the input m of RSA is known.

Proposition 2 (One faulty signature BellCoRe attack). If the intermediate variable S p (resp. S q ) is returned faulted as S p (resp. S q ), then the attacker gets an erroneous signature S, and is able to recover p (resp. q) as gcd(N, m -S e ) (with an overwhelming probability).

Proof. By proposition 1, if a fault occurs during the computation of S p , then gcd(N, S -S) = q (most likely). This means that:

• S ≡ S mod p, and thus S e ≡ S e mod p (indeed, if the congruence was true, we would have e|p -1, which is very unlikely); • S ≡ S mod q, and thus S e ≡ S e mod q; As S e ≡ m mod N, this proves the result. A symmetrical reasoning can be done if the fault occurs during the computation of S q .

Protection of CRT-RSA Against the BellCoRe Attack

Several protections against the BellCoRe attack have been proposed. A non-exhaustive list is given below, and then, the most salient features of these countermeasures are described:

• Obvious countermeasures: no CRT optimization, or with signature verification;

• Shamir [START_REF] Shamir | Method and apparatus for protecting public key schemes from timing and fault attacks[END_REF];

• Aumüller et al. [ABF + 02];
• Vigilant, original [START_REF] Vigilant | RSA with CRT: A New Cost-Effective Solution to Thwart Fault Attacks[END_REF] and with some corrections by Coron et al. [CGM + 10];

• Kim et al. [START_REF] Kim | An efficient CRT-RSA algorithm secure against power and fault attacks[END_REF].

Obvious Countermeasures

Fault attacks on RSA can be thwarted simply by refraining from implementing the CRT.

If this is not affordable, then the signature can be verified before being outputted. If S = m d mod N

is the signature, this straightforward countermeasure consists in testing S e ? ≡ m mod N. Such protection is efficient in practice, but is criticized for three reasons. First of all, it requires an access to e, which is not always present in the secret key structure, as in the 5-tuple example given in Sec. 2.1. Nonetheless, we attract the author's attention on paper [START_REF] Marc | Protecting RSA against Fault Attacks: The Embedding Method[END_REF] for a clever embedding of e into [the representation of] d. Second, the performances are incurred by the extra exponentiation needed for the verification. In some applications, the public exponent can be chosen small (for instance e can be equal to a number such as 3, 17 or 65537), and then d is computed as e -1 mod λ (N) using the extended Euclidean algorithm or better alternatives [START_REF] Joye | GCD-Free Algorithms for Computing Modular Inverses[END_REF]. But in general, e is a number possibly as large as d (both are as large as N), thus the obvious countermeasure doubles the computation time (which is really non-negligible, despite the CRT fourfold acceleration). Third, this protection is not immune to a fault injection that would target the comparison. Overall, this explains why other countermeasures have been devised.

Shamir

The CRT-RSA algorithm of Shamir builds on top of the CRT and introduces, in addition to the two primes p and q, a third factor r. This factor r is random4 and small (less than 64 bit long), and thus co-prime with p and q. The computations are carried out modulo p ′ = p • r (resp. modulo q ′ = q • r), which allows for a retrieval of the intended results by reducing them modulo p (resp. modulo q), and for a verification by a reduction modulo r. Alg. 2 describes one version of Shamir's countermeasure. This algorithm is aware of possible fault injections, and thus can raise an exception if an incoherence is detected. In this case, the output is not the (purported faulted) signature, but a specific message "error".

Aum üller

The CRT-RSA algorithm of Aumüller et al. is a variation of that of Shamir, that is primarily intended to fix two shortcomings. First it removes the need for d in the signature process, and second, it also checks the recombination step. The countermeasure, given in Alg. 3, introduces, in addition to p and q, a third prime t. The computations are done modulo p ′ = p • t (resp. modulo q ′ = q • t), which allows for a retrieval of the intended results by reducing them modulo p (resp. modulo q), and for a verification by a reduction modulo t. However, the verification is more subtle than for the case of Shamir. In Shamir's CRT-RSA (Alg. 2), the verification is symmetrical, in that the computations modulo p • r and q • r operate on the same object, namely m d . In Aumüller et al.'s CRT-RSA (Alg. 3), the verification is asymmetrical, since the computations modulo p•t and q•t operate on two different objects, namely m d p mod (t-1) and m d q mod (t-1) . The verification consists in an identity that resembles that of ElGamal for instance: is (m d p mod (t-1) ) d q mod (t-1) equivalent to (m d q mod (t-1) ) d p mod (t-1) modulo t? Specifically, if we note S ′ p the signature modulo p ′ , then S p = S mod p is equal to S ′ p mod p. Furthermore, let us denote

• S pt = S ′ p mod t, • S qt = S ′ q mod t, • d pt = d p mod (t -1), and • d qt = d q mod (t -1).
Algorithm 2: Shamir CRT-RSA Input : Message m, key (p, q, d, i q ), 32-bit random prime r Output: Signature m d mod N, or error if some fault injection has been detected.

1 p ′ = p • r 2 d p = d mod (p -1) • (r -1) 3 S ′ p = m d p mod p ′ // Signature modulo p ′ 4 q ′ = q • r 5 d q = d mod (q -1) • (r -1) 6 S ′ q = m d q mod q ′ // Signature modulo q ′
7 S p = S ′ p mod p 8 S q = S ′ q mod q // Same as in line 3 of Alg. 1 9 S = S q + q • (i q • (S p -S q ) mod p) if S ′ p ≡ S ′ q mod r then return error

else return S end

It can be verified that those figures satisfy the identity: S d qt pt ≡ S d pt qt mod t, because both terms are equal to m d pt •d qt mod t. The prime t is referred to as a security parameter, as the probability to pass the test (at line 23 of Alg. 3) is equal to 1/t (i.e., about 2 -32 ), assuming a uniform distribution of the faults. Indeed, this is the probability to find a large number that, once reduced modulo t, matches a predefined value.

Alg. 3 does some verifications during the computations, and reports an error in case a fault injection can cause a malformed signature susceptible of unveiling p and q. More precisely, an error is returned in either of these seven cases:

1. p ′ is not a multiple of p (because this would amount to faulting p in the unprotected algorithm)

2. d ′ p = d p + random 1 • (p -1)
is not equal to d p mod (p -1) (because this would amount to faulting d p in the unprotected algorithm) 3. q ′ is not a multiple of q (because this would amount to faulting q in the unprotected algorithm)

4. d ′ q = d q + random 2 • (q -1)
is not equal to d q mod (q -1) (because this would amount to faulting d q in the unprotected algorithm)

S -S ′

p mod p is nonzero (because this would amount to faulting the recombination modulo p in the unprotected algorithm) 6. S -S ′ q mod q is nonzero (because this would amount to faulting the recombination modulo q in the unprotected algorithm) 7. S d q pt mod t is not equal to S d p qt mod t (this checks simultaneously for the integrity of S ′ p and S ′ q )

Notice that the last verification could not have been done on the unprotected algorithm, it constitutes the added value of Aumüller et al.'s algorithm. These seven cases are informally assumed to protect the algorithm against the BellCoRe attack. The criteria for fault detection is not to detect all faults; for instance, a fault on the final return of S (line 26) is not detected. However, of course, such a fault is not exploitable by a BellCoRe attack.

Remark 1. Some parts of the Aumüller algorithm are actually not intended to protect against fault injection attacks, but against side-channel analysis, such as the simple power analysis (SPA). This is the case of lines 2 and 8 in Alg. 3. These SPA attacks consist in monitoring via a side-channel the activity of the chip, in a view to extract the secret exponent, using generic methods described in [START_REF] Paul | Differential Power Analysis[END_REF] or more accurate techniques such as wavelet transforms [SED + 11, DSE + 12]. They can be removed if a minimalist protection against only fault injection attacks is looked for; but as they do not introduce weaknesses (in this very specific case), they are simply kept as such.

Vigilant

The CRT-RSA algorithm of Vigilant [START_REF] Vigilant | RSA with CRT: A New Cost-Effective Solution to Thwart Fault Attacks[END_REF] also considers computations in a larger ring than Z p (abbreviation for Z/pZ) and Z q , to enable verifications. In this case, a small random number r is cast, and computations are carried out in Z p•r 2 and Z q•r 2 . In addition, the computations are now conducted not on the plain message m, but on an encoded message m ′ , built using the CRT as the solution of those two requirements:

i: m ′ ≡ m mod N, and ii: m ′ ≡ 1 + r mod r 2 .

Algorithm 3: Aumüller CRT-RSA Input : Message m, key (p, q, d p , d q , i q ), 32-bit random prime t Output: Signature m d mod N, or error if some fault injection has been detected.

1 p ′ = p • t 2 d ′ p = d p + random 1 • (p -1)
// Against SPA, not fault attacks

3 S ′ p = m d ′ p mod p ′ // Signature modulo p ′ 4 if (p ′ mod p = 0) or (d ′ p ≡ d p mod (p -1)) then 5 return error 6 end 7 q ′ = q • t 8 d ′ q = d q + random 2 • (q -1) // Against SPA, not fault attacks 9 S ′ q = m d ′ q mod q ′ // Signature modulo q ′ if (q ′ mod q = 0) or (d ′
q ≡ d q mod (q -1)) then return error end S p = S ′ p mod p S q = S ′ q mod q S = S q + q • (i q • (S p -S q ) mod p) // Same as in line 3 of Alg. 1 if (S -S ′ p ≡ 0 mod p) or (S -S ′ q ≡ 0 mod q) then return error end

S pt = S ′ p mod t S qt = S ′ q mod t d pt = d ′ p mod (t -1) d qt = d ′ q mod (t -1) if S d qt pt ≡ S d pt qt mod t then return error else return S end
This system of equations has a single solution modulo N × r 2 , because N and r 2 are coprime. Such a representation allows to conduct in parallel the functional CRT-RSA (line i) and a verification (line ii). The verification is elegant, as it leverages this remarkable equality:

(1 + r) d p = ∑ d p i=0 d p i • r i ≡ 1 + d p • r mod r 2 .
Thus, as opposed to Aumüller et al.'s CRT-RSA, which requires one exponentiation (line 23 of Alg. 3), the verification of Vigilant's algorithm adds only one affine computation (namely 1 + d p mod r 2 ).

The original description of Vigilant's algorithm involves some trivial computations on p and q, such as p -1, q -1 and p × q. Those can be faulted, in such a way the BellCoRe attack becomes possible despite all the tests. Thus, a patch by Coron et al. has been released in [CGM + 10] to avoid the reuse of p -1, q -1 and p × q in the algorithm.

Kim

Kim, Kim, Han and Hong propose in [START_REF] Kim | An efficient CRT-RSA algorithm secure against power and fault attacks[END_REF] a CRT-RSA algorithm that is based on a collaboration between a customized modular exponentiation and verifications at the recombination level based on Boolean operations. The underlying protection concepts being radically different from the algorithms of Shamir, Aumüller and Vigilant, we choose not to detail this interesting countermeasure.

Other Miscellaneous Fault Injections Attacks

When the attacker has the power to focus its fault injections on specific bits of sensitive resources, then more challenging security issues arise [START_REF] Berzati | A Survey of Differential Fault Analysis Against Classical RSA Implementations[END_REF]. These threats require a highly qualified expertise level, and are thus considered out of the scope of this paper.

Besides, for completeness, we mention that other fault injections mitigating techniques have been promoted, such as the infective computation scheme (refer to the seminal paper [START_REF] Blömer | A new CRT-RSA algorithm secure against bellcore attacks[END_REF]). This family of protections, although interesting, is neither covered by this article.

In this paper, we will focus on three implementations, namely the unprotected one (Sec. 4), the one protected by Shamir's countermeasure (Sec. 5), and the one protected by Aumüller et al.'s countermeasure (Sec. 6).

Formal Methods

For all the countermeasures presented in the previous section (Sec. 2), we can see that no formal proof of resistance against attacks is claimed. Informal arguments are given, that convince that for some attack scenarii, the attack attempts are detected hence harmless. Also, an analysis of the probability that an attack succeeds by chance (with a low probability of 1/t) is carried out, however, this analysis strongly relies on assumptions on the faults distribution. Last but not least, the algorithms include protections against both passive side-channel attacks (typically SPA) and active side-channel attacks, which makes it difficult to analyze for instance the minimal code to be added for the countermeasure to be correct.

CRT-RSA and Fault Injections

Our goal is to prove that a given countermeasure works, i.e., that it delivers a result which does leak information about neither p nor q even when the implementation is subject to fault injections and to a BellCoRe attack. In addition, we wish to reach this goal with the two following assumptions:

• our proof applies to a very general attacker model, and • our proof applies to any implementation that is a (strict) refinement of the abstract algorithm.

First, we must define what computation is done, and what is our threat model.

Definition 1 (CRT-RSA). The CRT-RSA computation takes as input a message m, assumed known by the attacker, and a secret key (p, q, d p , d q , i q ). Then, the implementation is free to instantiate any variable, but must return a result equal to S = S q + q • (i q • (S p -S q ) mod p), where:

• S p = m d p mod p, and • S q = m d q mod q.

Definition 2 (fault injection). An attacker is able to request RSA computations, as per Def. 1. During the computation, the attacker can modify any intermediate value by setting it to either a random value or zero.

At the end of the computation the attacker can read the result.

Of course, the attacker cannot read the intermediate values used during the computation, since the secret key and potentially the modulus factors are used. Such "whitebox" attack would be too powerful; nonetheless, it is very hard in practice for an attacker to be able to access intermediate variables, due to specific protections (e.g., blinding) and noise in the side-channel leakage (e.g., power consumption, electromagnetic emanation). Remark that our model only takes into account fault injection on data; the control flow is supposed not to be mutable.

As a side remark, we notice that the fault injection model of Def. 2 corresponds to that of Vigilant ([Vig08]), with the exception that the conditional tests can also be faulted. To summarize, an attacker can:

• modify a value in memory (permanent fault), and • modify a value in a local register, cache, or bus (transient fault), but cannot

• inject a permanent fault in the input data (message and secret key), nor • modify the algorithm control flow graph.

The independence of the proofs on the algorithm implementation demands that the algorithm is described at a high level. The two properties that characterize the relevant level are as follows:

1. The description should be low level enough for the attack to work if protections are not implemented. 2. Any additional intermediate variable that would appear during refinement could be the target of an attack, but such a fault would propagate to an intermediate variable of the high level description, thereby having the same effect. From those requirements, we deduce that:

1. The RSA description must exhibit the computation modulo p and q and the CRT recombination; typically, a completely blackbox description, where the computations would be realized in one go without intermediate variables, is not conceivable. 2. However, it can remain abstract, especially for the computational parts5 .

In our approach, the protections must thus be considered as an augmentation of the unprotected code, i.e., a derived version of the code where additional variables are used. The possibility of an attack on the unprotected code attests that the algorithm is described at the adequate level, while the impossibility of an attack (to be proven) on the protected code shows that added protections are useful in terms of resistance to attacks.

Remark 2. The algorithm only exhibits evidence of safety. If after a fault injection, the algorithm does not simplify to an error detection, then it might only reveal that some simplification is missing. However, if it does not claim safety, it produces a simplified occurrence of a possible weakness to be investigated further.

finja

Several tools are a priori suitable for a formal analysis of CRT-RSA. PARI/GP is a specialized computer algebra system, primarily aimed at solving number theory problems. Although PARI/GP can do a fair amount of symbolic manipulation, it remains limited compared to systems like Axiom, Magma, Maple, Mathematica, Maxima, or Reduce. Those last software also fall short to implement automatically number theoretic results like Euler's theorem. This explains why we developed from scratch a system to reason on modular numbers from a formal point of view. Our system is not general, in that it cannot for instance factorize terms in an expression. However, it is able to simplify recursively what is simplifiable from a set of unambiguous rules. This behavior is suitable to the problem of resistance to fault attacks, because the redundancy that is added in the computation is meant to be simplified at the end (if no faults happened).

Our tool finja works within the framework of modular arithmetic, which is the mathematical framework of CRT-RSA computations. The general idea is to represent the computation term as a tree which encodes the computation properties. This term can be simplified by finja, using rules from arithmetic and the properties encoded in the tree. Fault injections in the computation term are simulated by changing the properties of a subterm, thus impacting the simplification process. An attack success condition is also given and used on the term resulting from the simplification to check whether the corresponding attack works on it. The outputs of finja are in HTML form: easily readable reports are produced, which contains all the information about the possible fault injections and their outcome.

Computation Term

The computation is expressed in a convenient statement-based input language. This language's Backus Normal Form (BNF) is given in Fig. 1.

A computation term is defined by a list of statements finished by a return statement. Each statement can either:

• declare a variable with no properties (line 3);

• declare a variable which is a prime number (line 4);

• declare a variable by assigning it a value (line 5), in this case the properties of the variable are the properties of the assigned expression;

• perform a verification (line 6).

As can be seen in lines 9 to 15, an expression can be:

• zero, one, or an already declared variable;

• the sum (or difference) of two expressions;

• the product of two expressions;

• the exponentiation of an expression by another; • the modulus of an expression by another.

The condition in a verification can be (lines 18 to 23):

• the equality or inequality of two expressions;

• the equivalence or non-equivalence of two expressions modulo another (lines 20 and 21);

• the conjunction or disjunction of two conditions.

Optionally, variables (when declared using the prime or noprop keywords), expressions, and conditions can be protected (lines 3, 4, 7 and 16, mp stands for "maybe protected") from fault injection by surrounding them with curly braces. This is useful for instance when it is needed to express the properties of a variable which cannot be faulted in the studied attack model. For example, in CRT-RSA, the definitions of variables d p , d q , and i q are protected because they are seen as input of the computation.

Finally, line 25 gives the regular expression that variable names must match (they start with a letter and then can contain letters, numbers, underscore, and simple quote).

After it is read by finja, the computation expressed in this input language is transformed into a tree (just like the abstract syntax tree in a compiler). This tree encodes the arithmetical properties of each of the intermediate variable, and thus its dependencies on previous variables. The properties of intermediate variables can be everything that is expressible in the input language. For instance, being null or being the product of other terms (and thus, being a multiple of each of them), are possible properties.

Fault Injection

A fault injection on an intermediate variable is represented by changing the properties of the subterm (a node and its whole subtree in the tree representing the computation term) that represent it. In the case of a fault which forces at zero, then the whole subterm is replaced by a term which only has the property of being null. In the case of a randomizing fault, by a term which have no properties.

finja simulates all the possible fault injections of the attack model it is launched with. The parameters allow to choose:

• how many faults have to be injected (however, the number of tests to be done is impacted by a factorial growth with this parameter, as is the time needed to finish the computation of the proof);

• the type of each fault (randomizing or zeroing);

• if transient faults are possible or if only permanent faults should be performed.

Attack Success Condition

The attack success condition is expressed using the same condition language as presented in Sec. 3.2.1. It can use any variable introduced in the computation term, plus two special variables and @ which are respectively bound to the expression returned by the computation term as given by the user and to the expression returned by the computation with the fault injections. This success condition is checked for each possible faulted computation term.

Simplification Process

The simplification is implemented as a recursive traversal of the term tree, based on pattern-matching. It works just like a naive interpreter would, except it does symbolic computation only, and reduces the term based on rules from arithmetic. Simplifications are carried out in Z ring, and its Z N subrings. The tool knows how to deal with most of the Z ring axioms:

• the neutral elements (0 for sums, 1 for products);

• the absorbing element (0, for products);

• inverses and opposites (only if N is prime);

• associativity and commutativity.

However, it does not implement distributivity as it is not confluent. Associativity is implemented by flattening as much as possible ("removing" all unnecessary parentheses), and commutativity is implemented by applying a stable sorting algorithm on the terms of products or sums. The tool also knows about most of the properties that are particular to Z N rings and applies them when simplifying a term modulo N:

• identity:

-(a mod N) mod N = a mod N, -N k mod N = 0; • inverse: -(a mod N) × (a -1 mod N) mod N = 1, -(a mod N) + (-a mod N) mod N = 0;
• associativity and commutativity:

-(b mod N) + (a mod N) mod N = a + b mod N, -(a mod N) × (b mod N) mod N = a × b mod N; • subrings: (a mod N × m) mod N = a mod N.
In addition to those properties a few theorems are implemented to manage more complicated cases where the properties are not enough when conducting symbolic computations:

• Fermat's little theorem;

• its generalization, Euler's theorem. If the properties that interest us is to know whether t is congruent with a modulo b, we can use t =[b] a as the attack success condition. Of course it will be true for t, but it will only be true for the fifth version of faulted t. If we had used the zeroing fault, it would also have been true for the third and fourth versions.

Study of an Unprotected CRT-RSA Computation

The description of the unprotected CRT-RSA computation in finja code is given in Fig. 2 (note the similarity of finja's input code with Alg. 1).

1 noprop m, e ; 2 prime {p}, {q} ; 3 4 dp := { e^-1 mod (p-1) } ; 5 dq := { e^-1 mod (q-1) } ; 6 iq := { q^-1 mod p } ; 7 8 Sp := m^dp mod p ; 9 Sq := m^dq mod q ; 10 11 S := Sq + (q * (iq * (Sp -Sq) mod p)) ; 12 13 return S ; As we can see, the definitions of d p , d q , and i q are protected so the computation of the values of these variables cannot be faulted (since they are seen as inputs of the algorithm). After that, S p and S q are computed and then recombined in the last expression, as in Def. 1.

14 15 %% 16 17 _ != @ /\ ( _ =[p] @ \/ _ =[q] @ )
To test whether the BellCoRe attack works on a faulted version S, we perform the following tests (we note |S| for the simplified version of S):

1. is |S| equal to | S|? 2. is |S mod p| equal to | S mod p|? 3. is |S mod q| equal to | S mod q|?

If the first test is false and at least one of the second and third is true, we have a BellCoRe attack, as seen in Sec. 2. This is what is described in the attack success condition (after the %% line).

Without transient faults enabled, and in a single fault model, there are 12 different fault injections of which 8 enable a BellCoRe attack with a randomizing fault, and 9 with a zeroing fault. As an example, replacing the intermediate variable holding the value of i q • (S p -S q ) mod p in the final expression with zero or a random value makes the first and second tests false, and the last one true, and thus allows a BellCoRe attack.

Study of Shamir's Countermeasure

The description, using finja's formalism, of the CRT-RSA computation allegedly protected by Shamir's countermeasure is given in Fig. 3 (again, note the similarity with Alg. 2).

1 noprop error, m, d ; 2 prime {p}, {q}, r ; 3 iq := { q^-1 mod p } ; 4 5 p' := p * r ; 6 dp := d mod ((p-1) * (r-1)) ; 7 Sp' := m^dp mod p' ; 8 9 q' := q * r ; 10 dq := d mod ((q-1) * (r-1)) ; 11 Sq' := m^dq mod q' ; 12 13 Sp := Sp' mod p ; 14 Sq := Sq' mod q ; 15 16 S := Sq + (q * (iq * (Sp -Sq) mod p)) ; Using the same settings as for the unprotected implementation of CRT-RSA, we find that among the 31 different fault injections, 10 enable a BellCoRe attack with a randomizing fault, and 9 with a zeroing fault. This is not really surprising, as the test which is done on line 18 does not verify if a fault is injected during the computations of S p or S q , nor during their recombination in S. For instance zeroing or randomizing the intermediate variable holding the result of S p -S q during the computation of S (line 16) results in a BellCoRe attack. To explain why there is this problem in Shamir's countermeasure, some context might be necessary. It can be noted that the fault to inject in the countermeasure must be more accurate in timing (since it targets an intermediate variable obtained by a subtraction) than the faults to achieve a BellCoRe attack on the unprotected CRT-RSA (since a fault during an exponentiation suffices). However, there is today a consensus to believe that it is very easy to pinpoint in time any single operation of a CRT-RSA algorithm, using a simple power analysis method [START_REF] Paul | Differential Power Analysis[END_REF]. Besides, timely fault injection benches exist. Therefore, the weaknesses in Shamir's countermeasure can indeed be practically exploited.

If the attacker can do transient faults, there are a lot more attacks: 66 different possible fault injections of which 24 enable a BellCoRe attack with a randomizing fault and 22 with a zeroing fault. In practice, a transient faults would translate into faulting the variable when it is read (e.g., in a register or on a bus), rather than in (persistent) memory. This behavior could also be the effect of a fault injection in cache, which is later replaced with the good value when it is read from memory again. To the authors knowledge, these are not impossible situations. Nonetheless, growing the power of the attacker to take that into account break some very important assumptions that are classical (sometimes even implicit) in the literature. It does not matter that the parts of the secret key are stored in a secure "key container" if their values can be a faulted at read time. Indeed, we just saw that allowing this kind of fault enable even more possibilities to carry out a BellCoRe attack successfully on a CRT-RSA computation protected by the Shamir's countermeasure. For instance, if the value of p is randomized for the computation of the value of S p (line 13), then we have S = S, but also S ≡ S mod q, which enables a BellCoRe attack, as seen in Sec. 2.

It is often asserted that the countermeasure of Shamir is unpractical due to its need for d (as mentioned in [ABF + 02] and [START_REF] Vigilant | RSA with CRT: A New Cost-Effective Solution to Thwart Fault Attacks[END_REF]), and because there is a possible fault attack on the recombination, i.e., line 16 (as mentioned in [START_REF] Vigilant | RSA with CRT: A New Cost-Effective Solution to Thwart Fault Attacks[END_REF]). However, the attack on the recombination can be checked easily, by testing that S -S p ≡ 0 mod p and S -S q ≡ 0 mod q before returning the result. Notwithstanding, to our best knowledge, it is difficult to detect all the attacks our tool found, and so the existence of these attacks (new, in the sense they have not all been described previously) is a compelling reason for not implementing Shamir's CRT-RSA.

Study of Aum üller et al.'s Countermeasure

The description of the CRT-RSA computation protected by Aumüller et al.'s countermeasure is given in Fig. 4 (here too, note the similarity with Alg. 3) Using the same method as before, we can prove that on the 52 different possible faults, none of which allow a BellCoRe attack, whether the fault is zero or random. This is a proof that the Aumüller et al.'s countermeasure works when there is one fault6 .

Since it allowed more attacks on the Shamir's countermeasure, we also tested the Aumüller et al.'s countermeasure against transient faults such as described in Sec. 5. There are 120 different possible fault injections when transient faults are activated, and Aumüller et al.'s countermeasure is resistant against such fault injections too.

We also used finja to confirm that the computation of d p , d q , and i q (in terms of p, q, and d) must not be part of the algorithm. The countermeasure effectively needs these three variables to be inputs of the algorithm to work properly. For instance there is a BellCoRe attack if d q happens to be zeroed. However, even with d p , d q , and i q as inputs, we can still attempt to attack a CRT-RSA implementation protected by the Aumüller et al.'s countermeasure by doing more than one fault.

We then used finja to verify whether Aumüller et al.'s countermeasure would be resistant against high order attacks, starting with two faults. We were able to break it if at least one of the two faults was a zeroing fault. We found that this zeroing fault was used to falsify the condition of a verification, which is possible in our threat-model, but which was not in the one of the authors of the countermeasure. If we protect the conditions against fault injection, then the computation is immune two double-fault attacks too. However, even in this less powerful threat-model, a CRT-RSA computation protected by Aumüller et al.'s countermeasure is breakable using 3 faults, two of which must be zeroing the computations of d pt and d qt .

Conclusions and Perspectives

We have formally proven the resistance of the Aumüller et al.'s countermeasure against the BellCoRe attack by fault injection on CRT-RSA. To our knowledge, it is the first time that a formal proof of security is done for a BellCoRe countermeasure.

During our research, we have raised several questions about the assumptions traditionally made by countermeasures. The possibility of fault at read time is, in particular, responsible for many vulnerabilities. The possibility of such fault means that part of the secret key can be faulted (even if only for one computation). It allows an interesting BellCoRe attack on a computation of CRT-RSA protected by Shamir's countermeasure. We also saw that the assumption that the result of conditional expression cannot be faulted, which is widespread in the literature, is a dangerous one as it increased the number of fault necessary to break Aumüller et al.'s countermeasure from 2 to 3.

The first of these two points demonstrates the lack of formal studies of fault injection attack and their countermeasures, while the second one shows the importance of formal methods in the field of implementation security.

As a first perspective, we would like to address the hardening of software codes of CRT-RSA under the threat of a bug attack. This attack has been introduced by Biham, Carmeli and Shamir [START_REF] Biham | Bug attacks[END_REF] at CRYPTO 2008. It assumes that a hardware has been trapped in such a way that there exists two integers a and b, for which the multiplication is incorrect. In this situation, Biham, Carmeli and Shamir mount an explicit attack scenario where the knowledge of a and b is leveraged to produce a faulted result, that can lead to a remote BellCoRe attack. For sure, testing for the correct functionality of the multiplication operation is impractical (it would amount to an exhaustive verification of 2 128 multiplications on 64 bit computer architectures). Thus, it can be imagined to use a countermeasure, like that of Aumüller, to detect a fault (caused logically). Our aim would be to assess in which respect our fault analysis formal framework allows to validate the security of the protection. Indeed, a fundamental difference is that the fault is not necessarily injected at one random place, but can potentially show up at several places.

As another perspective, we would like to handle the repaired countermeasure of Vigilant [CGM + 10] and the countermeasure of Kim [START_REF] Kim | An efficient CRT-RSA algorithm secure against power and fault attacks[END_REF]. Regarding Vigilant, the difficulty that our verification framework in OCaml [INR] shall overcome is to decide how to inject the remarkable identity (1 + r) d p ≡ 1 + d p • r mod r 2 : either it is kept as such such, like an ad hoc theorem (but we need to make sure it is called only at relevant places, since it is not confluent), or it is made more general (but we must ascertain that the verification remains tractable). However, this effort is worthwhile7 , because the authors themselves say in the conclusion of their article [CGM + 10] that: "Formal proof of the FA-resistance of Vigilant's scheme including our countermeasures is still an open (and challenging) issue."

Regarding the CRT-RSA algorithm from Kim, the computation is very detailed (it goes down to the multiplication level), and involves Boolean operations (and, xor, etc.). To manage that, more expertise about both arithmetic and logic must be added to our software. Eventually, we wish to answer a question raised by Vigilant [START_REF] Vigilant | RSA with CRT: A New Cost-Effective Solution to Thwart Fault Attacks[END_REF] about the prime t involved in Aumüller et al.'s countermeasure:

"Is it fixed or picked at random in a fixed table?"

The underlying issue is that of replay attacks on CRT-RSA, that are more complicated to handle; indeed, they would require a formal system such as ProVerif [Bla], that is able to prove interactive protocols.

Concerning the tools we developed during our research, they currently only allow to study fault injection in the data, and not in the control flow, it would be interesting to enable formal study of fault injections affecting the control flow.

Eventually, we would like to define and then implement an automatic code mutation algorithm that could transform an unprotected CRT-RSA into a protected one. We know that with a few alterations (see that the differences between Alg. 1 and Alg. 3 are enumerable), this is possible. Such promising approach, if successful, would uncover the smallest possible countermeasure of CRT-RSA against fault injection attacks.

  3 of respectively an unprotected version of the CRT-RSA computation, a version protected by Shamir's countermeasure, and a version protected by Aumüller et al.'s countermeasure. Conclusions and perspectives are in Sec. 7.

Figure 1 :

 1 Figure 1: BNF of finja's input language.

Example.

  If we have the term t := a + b * c, it can be faulted in five different ways (using the randomizing fault): 1. t := Random, the final result is faulted; 2. t := Random + b * c, a is faulted; 3. t := a + Random, the result of b × c is faulted; 4. t := a + Random * c, b is faulted; 5. t := a + b * Random, c is faulted.

Figure 2 :

 2 Figure 2: finja code for the unprotected CRT-RSA computation.

Figure 3 :

 3 Figure 3: finja code for the Shamir CRT-RSA computation.

http://pablo.rauzy.name/sensi/finja.html

In other papers related to faults, the faulted variables (such as X) are noted either with a star (X * ) or a tilde ( X); in this paper, we use a hat, as it can stretch, hence cover the adequate portion of the variable. For instance, it allows to make an unambiguous difference between a faulted data raised at some power and a fault on a data raised at a given power (contrast X e with X e ).

If it nonetheless happens that gcd(N, S -S) = N, then the attacker can simply retry another fault injection, for which the probability that gcd(N, S -S) ∈ {p, q} increases.

The authors notice that in Shamir's countermeasure, r is a priori not a secret, hence can be static and safely divulged.

For example, a fault in the implementation of the multiplication is either inoffensive, and we do not need to care about it, or it affects the result of the multiplication, and our model take it into account without going into the details of how the multiplication's is computed

This result is worthwhile some emphasis: the genuine algorithm of Aumüller is thus proved resistant against single-fault attacks. At the opposite, the CRT-RSA algorithm of Vigilant is not immune to single fault attacks (refer to [CGM + 10]), and the corrections suggested in the same paper by Coron et al. have not been proved yet.

Some results will appear in the proceedings of the 3rd ACM SIGPLAN Program Protection and Reverse Engineering Workshop (PPREW 2014)[START_REF] Rauzy | Formal Analysis of CRT-RSA Vigilant's Countermeasure Against the BellCoRe Attack -A Pledge for Formal Methods in the Field of Implementation Security[END_REF], collocated with POPL 2014.

Acknowledgements

The authors wish to thank Jean-Pierre Seifert and Wieland Fischer for insightful comments and pieces of advice. We are also grateful to the anonymous reviewers of PROOFS 2013 (UCSB, USA), who helped improve the preliminary version of this paper. Eventually, we acknowledge precious suggestions contributed by Jean-Luc Danger, Jean Goubault-Larrecq, and Karine Heydemann.

noprop error, m, e, r1, r2 ; prime {p}, {q}, t ; dp := { e^-1 mod (p-1) } ; dq := { e^-1 mod (q-1) } ; iq := { q^-1 mod p } ; p' := p * t ; dp' := dp + r1 * (p-1) ; Sp' := m^dp' mod p' ; if p' !=[p] 0 \/ dp' !=[p-1] dp abort with error ; q' := q * t ; dq' := dq + r2 * (q-1) ; Sq' := m^dq' mod q' ; if q' !=[q] 0 \/ dq' !=[q-1] dq abort with error ; Sp := Sp' mod p ; Sq := Sq' mod q ; S := Sq + (q * (iq * (Sp -Sq) mod p)) ; if S !=[p] Sp' \/ S !=[q] Sq' abort with error ; Spt := Sp' mod t ; Sqt := Sq' mod t ; dpt := dp' mod (t-1) ; dqt := dq' mod (t-1) ; if Spt^dqt !=[t] Sqt^dpt abort with error ; return S ; %% _ != @ /\ ( _ =[p] @ \/ _ =[q] @ )