Georgi Vodev
email: georgi.vodev@univ-nantes.fr

SEMI-CLASSICAL RESOLVENT ESTIMATES FOR SHORT-RANGE L ∞ POTENTIALS. II

Keywords: Schrödinger operator, resolvent estimates, short-range potentials

We prove semi-classical resolvent estimates for real-valued potentials V ∈ L ∞ (R n ), n ≥ 3, of the form V = VL + VS, where VL is a long-range potential which is C 1 with respect to the radial variable, while VS is a short-range potential satisfying VS(x) = O x -δ with δ > 1.

Introduction and statement of results

The goal of this paper is to extend the semi-classical resolvent estimates obtained recently in [START_REF] Klopp | Semiclassical resolvent estimates for bounded potentials[END_REF], [START_REF] Shapiro | Semiclassical resolvent bound for compactly supported L ∞ potentials[END_REF] and [START_REF] Vodev | Semi-classical resolvent estimates for short-range L ∞ potentials[END_REF] to a larger class of potentials. We are going to study the resolvent of the Schrödinger operator P (h) = -h 2 ∆ + V (x) where 0 < h ≪ 1 is a semi-classical parameter, ∆ is the negative Laplacian in R n , n ≥ 3, and V ∈ L ∞ (R n ) is a real-valued potential of the form V = V L + V S , where V L ∈ C 1 ([r 0 , +∞)) with respect to the radial variable r = |x|, r 0 > 0 being some constant, is a long-range potential, while V S is a short-range potential satisfying (1.1) |V S (x)| ≤ C 1 (|x| + 1) -δ with some constants C 1 > 0 and δ > 1. We suppose that there exists a decreasing function p(r) > 0, p(r) → 0 as r → ∞, such that (1.2) V L (x) ≤ p(|x|) for |x| ≥ r 0 .

We also suppose that (1.3) ∂ r V L (x) ≤ C 2 (|x| + 1) -β for |x| ≥ r 0 with some constants C 2 > 0 and β > 1. As in [START_REF] Vodev | Semi-classical resolvent estimates for short-range L ∞ potentials[END_REF] we introduce the quantity g ± s (h, θ) := log (|x| + 1) -s (P (h) -E ± iθ) -1 (|x| + 1) -s

L 2 →L 2
where L 2 := L 2 (R n ), 0 < θ < 1, s > 1/2 is independent of h and E > 0 is a fixed energy level independent of h. Our first result is the following Theorem 1.1. Suppose the conditions (1.1), (1.2) and (1.3) fulfilled with δ and β satisfying the condition

(1.4) δ > 3, β > 3.
Then there exist constants C > 0 and h 0 > 0 independent of h and θ but depending on s and E such that for all 0 < h ≤ h 0 we have the bound (1.5) g ± s (h, θ) ≤ Ch -4/3 log(h -1 ). If the conditions (1.1), (1.2) and (1.3) are fulfilled with δ and β satisfying the condition (1.6) δ > 3, β = 3, then we have the bound (1.7) g ± s (h, θ) ≤ Ch -4/3 log(h -1 ) 3/2 log log(h -1 ) -1 .

When V S ≡ 0 and V L satisfying conditions similar to (1.2) and (1.3), it is proved in [START_REF] Datchev | Quantative limiting absorption principle in the semiclassical limit[END_REF] when n ≥ 3 and in [START_REF] Shapiro | Semiclassical resolvent bounds in dimension two[END_REF] when n = 2 that (1.8) g ± s (h, θ) ≤ Ch -1 with some constant C > 0 independent of h and θ. Previously, the bound (1.8) was proved for smooth potentials in [START_REF] Burq | Lower bounds for shape resonances widths of long-range Schrödinger operators[END_REF] and an analog of (1.8) for Hölder potentials was proved in [START_REF] Vodev | Semi-classical resolvent estimates and regions free of resonances[END_REF]. A high-frequency analog of (1.8) on Riemannian manifolds was also proved in [START_REF] Burq | Décroissance de l'énergie locale de l'équation des ondes pour le problème extérieur et absence de résonance au voisinage du réel[END_REF] and [START_REF] Cardoso | Uniform estimates of the resolvent of the Laplace-Beltrami operator on infinite volume Riemannian manifolds[END_REF]. When V L ≡ 0 and V S satisfying the condition (1.1) with δ > 3, the bound (1.5) has been recently proved in [START_REF] Vodev | Semi-classical resolvent estimates for short-range L ∞ potentials[END_REF]. Previously, (1.5) was proved in [START_REF] Klopp | Semiclassical resolvent estimates for bounded potentials[END_REF] and [START_REF] Shapiro | Semiclassical resolvent bound for compactly supported L ∞ potentials[END_REF] for real-valued compactly supported L ∞ potentials. When n = 1 it was shown in [START_REF] Dyatlov | The mathematical theory of scattering resonances[END_REF] that we have the better bound (1.8) instead of (1.5). The method we use to prove Theorem 1.1 also allows us to get resolvent bounds when the conditions (1.4) and (1.6) are not satisfied, which however are much weaker than the bound (1.5). More precisely, we have the following Theorem 1.2. Suppose the conditions (1.1), (1.2) and (1.3) fulfilled with δ and β satisfying either the condition

(1.9) 1 < δ ≤ 3, β > 1,
or the condition

(1.10) δ > 3, 1 < β < 3.
Then, there exist constants C > 0 and h 0 > 0 independent of h and θ but depending on s and E such that for all 0 < h ≤ h 0 we have the bounds

(1.11) g ± s (h, θ) ≤ Ch -2 3 -m 1 log(h -1 )
ν if (1.9) holds, and

(1.12) g ± s (h, θ) ≤ Ch -4 3 -1 2 (3-β)m 2 log(h -1 ) ν if (1.10) holds,
where

m 1 = max 7 3(δ -1) , 4 3(β -1) ≥ 7 6 , m 2 = max 1 δ -β , 4 3(β -1) > 2 3 , ν = max 1 δ -1 , 1 β -1 .
Clearly, this theorem implies the following Corollary 1.3. Suppose that V L ≡ 0 and let V = V S satisfy the condition (1.1) with 1 < δ ≤ 3.

Then, there exist constants C > 0 and h 0 > 0 independent of h and θ but depending on s and E such that for all 0 < h ≤ h 0 we have the bound

(1.13) g ± s (h, θ) ≤ Ch -2δ+5 3(δ-1) log(h -1 ) 1 δ-1 .
To prove the above theorems we follow the same strategy as in [START_REF] Vodev | Semi-classical resolvent estimates for short-range L ∞ potentials[END_REF] which in turn is inspired by the paper [START_REF] Shapiro | Semiclassical resolvent bound for compactly supported L ∞ potentials[END_REF]. It consists of using Carleman estimates with phase and weight functions, denoted by ϕ and µ below, depending only on the radial variable r and the parameter h, which have very weak regularity. It turns out that it suffices to choose ϕ belonging only to C 1 and µ only continuous. Thus we get derivatives ϕ ′′ and µ ′ belonging to L ∞ , which proves sufficient for the Carleman estimates to hold. Note that higher derivatives of ϕ and µ are not involved in the proof of the Carleman estimates (see the proof of Theorem 3.1 below). In order to be able to prove the Carleman estimates the functions ϕ and µ must satisfy some conditions (see the inequalities (2.3) and (2.9) below). On the other hand, to get as good resolvent bounds as possible we are looking for a phase function ϕ such that max ϕ is as small as possible. The construction of such phase and weight functions is carried out in Section 2 following that one in [START_REF] Vodev | Semi-classical resolvent estimates for short-range L ∞ potentials[END_REF]. However, here the construction is more complicated due to the more general class the potential belongs to.

It is not clear if the bounds (1.5), (1.7), (1.11) and (1.12) are optimal for L ∞ potentials. In any case, they seem hard to improve unless one menages to construct a better phase function. By contrast, the optimality of the bound (1.8) for smooth potentials is well known (e.g. see [START_REF] Datchev | Resonances and lower resolvent bounds[END_REF]).

The construction of the phase and weight functions revisited

We will follow closely the construction in Section 2 of [START_REF] Vodev | Semi-classical resolvent estimates for short-range L ∞ potentials[END_REF] making some suitable modifications in order to adapte it to the more general class of potentials we consider in the present paper. We will first construct the weight function µ as follows:

µ(r) = (r + 1) 2k -1 for 0 ≤ r ≤ a, (a + 1) 2k -1 + (a + 1) -2s+1 -(r + 1) -2s+1 for r ≥ a, where a = h -m with m =            m 0 (1 + 2ǫλ) if (1.4) holds, m 0 + ǫλ/2 + ǫT 1 if (1.6) holds, m 1 + νǫλ + ǫT 2 if (1.9) holds, m 2 + νǫλ + ǫT 3 if (1.10) holds, where ǫ = log 1 h -1 , λ = log log 1 h , m 0 = max 2 3 , 1 δ-3
, m 1 , m 2 and ν are as in Theorem 1.2, while T j > 0, j = 1, 2, 3, are parameters independent of h to be fixed in the proof of Lemma 2.3. Furthermore,

k =            1 -ǫ if (1.4) holds, 1 -ǫλ 2m 0 -ǫt 1 if (1.6) holds, 2 3m 1 -2νǫλ 3m 2 1 -ǫt 2 if (1.9) holds, β-1 2 -(β-1)νǫλ 2m 2 -ǫt 3 if (1.10) holds,

and

(2.1) s = 1 + ǫ 2 where t j > 1, j = 1, 2, 3, are parameters independent of h to be fixed in the proof of Lemma 2.3. Clearly, the first derivative (in sense of distributions) of µ satisfies

(2.2) µ ′ (r) = 2k(r + 1) 2k-1 for 0 ≤ r < a, (2s -1)(r + 1) -2s for r > a.
The following properties of the functions µ and µ ′ are essential to prove the Carleman estimates in the next section.

Lemma 2.1. For all r > 0, r = a, we have the inequalities

(2.3) 2r -1 µ(r) -µ ′ (r) ≥ 0, (2.4) µ ′ (r) ≥ ǫ(r + 1) -2s , (2.5) µ(r) µ ′ (r) ǫ -1 a 2k (r + 1) 2s , (2.6) µ(r) 2 µ ′ (r) ǫ -1 a 4k (r + 1) 2s .
Proof. It is easy to see that for r < a (2.3) follows from the inequality

f (r) := 1 + (1 -k)r -(r + 1) 1-2k ≥ 0 for all r ≥ 0 and 0 ≤ k ≤ 1. It is obvious for 1/2 ≤ k ≤ 1, while for 0 ≤ k < 1/2 we have f ′ (r) = 1 -k -(1 -2k)(r + 1) -2k ≥ k ≥ 0.
Hence in this case the function f is increasing, which implies f (r) ≥ f (0) = 0 as desired. For r > a the left-hand side of (2.3) is bounded from below by

2r -1 ((a + 1) 2k -1 -s) > 0
provided a is taken large enough. The lower bound (2.4) is an immediate consequence of (2.1) and (2.2), while the bounds (2.5) and (2.6) follow from (2.4) and the fact that µ = O(a 2k ). ✷

We now turn to the construction of the phase function ϕ ∈ C 1 ([0, +∞)) such that ϕ(0) = 0 and ϕ(r) > 0 for r > 0. We define the first derivative of ϕ by

ϕ ′ (r) = τ (r + 1) -k -τ (a + 1) -k for 0 ≤ r ≤ a, 0 for r ≥ a, where (2.7) τ = τ 0 h -1/3
with some parameter τ 0 ≫ 1 independent of h to be fixed in Lemma 2.3 below. Clearly, the first derivative of ϕ ′ satisfies

ϕ ′′ (r) = -kτ (r + 1) -k-1 for 0 ≤ r < a, 0 for r > a.
Lemma 2.2. For all r ≥ 0 we have the bounds

(2.8) h -1 ϕ(r)            h -4/3 log(h -1 ) if (1.4) holds, h -4/3 (log(h -1 )) 3/2 (log log(h -1 )) -1 if (1.6) holds, h -2 3 -m 1 (log(h -1 )) ν if (1.9) holds, h -4 3 -1 2 (3-β)m 2 (log(h -1 )) ν if (1.10) holds. Proof. Since k < 1 we have max ϕ = a 0 ϕ ′ (r)dr ≤ τ a 0 (r + 1) -k dr ≤ τ 1 -k (a + 1) 1-k (1 -k) -1 h -1 3 -m(1-k)
and

(1 -k) -1            ǫ -1 if (1.4) holds, (ǫλ) -1 if (1.6) holds, 1 if (1.9) holds, 1 if (1.10) holds. Since m(1 -k) =            O(ǫ) if (1.4) holds, ǫλ/2 + O(ǫ) if (1.6) holds, m 1 -2 3 + νǫλ + O(ǫ) if (1.9) holds, 1 2 (3 -β)m 2 + νǫλ + O(ǫ) if (1.10
) holds, and taking into account that h -ǫλ = ǫ -1 and h -ǫ = e, we get (2.8) from the above bounds.

✷ Let φ ∈ C ∞ 0 ([1, 2]), φ ≥ 0, be a real-valued function independent of h such that ∞ -∞ φ(σ)dσ = 1. Given a parameter b ≫ r 0 to be fixed in the proof of Theorem 3.1 below, independent of h, set ψ b (r) = b -1 ∞ r φ(σ/b)dσ.
Clearly, we have 0

≤ ψ b ≤ 1 and ψ b (r) = 1 for r ≤ b, ψ b (r) = 0 for r ≥ 2b. For r > 0, r = a, set A(r) = µϕ ′2 ′ (r)
and

B(r) = 3 µ(r) h -1 C 1 (r + 1) -δ + h -1 Q b ψ b (r) + |ϕ ′′ (r)| 2 h -1 ϕ ′ (r)µ(r) + µ ′ (r) +µ(r)(1 -ψ b (r))C 2 (r + 1) -β
where Q b ≥ 0 is some constant depending only on b. The following lemma will play a crucial role in the proof of the Carleman estimates in the next section.

Lemma 2.3. There exist constants b 0 = b 0 (E) > 0, τ 0 = τ 0 (b, E) > 0 and h 0 = h 0 (b, E) > 0 so that for τ satisfying (2.7) and for all b ≥ b 0 , 0 < h ≤ h 0 we have the inequality

(2.9) A(r) -B(r) ≥ - E 2 µ ′ (r)
for all r > 0, r = a.

Proof. For r < a we have

A(r) = -ϕ ′2 ′ (r) + τ 2 ∂ r 1 -(r + 1) k (a + 1) -k 2 = -2ϕ ′ (r)ϕ ′′ (r) -2kτ 2 (r + 1) k-1 (a + 1) -k 1 -(r + 1) k (a + 1) -k ≥ 2kτ (r + 1) -k-1 ϕ ′ (r) -2kτ 2 (r + 1) k-1 (a + 1) -k ≥ 2kτ (r + 1) -k-1 ϕ ′ (r) -τ 2 a -k µ ′ (r).
Taking into account the definition of the parameters a and τ we conclude (2.10)

A(r) ≥ 2kτ (r + 1) -k-1 ϕ ′ (r) -O(h km-2/3 )µ ′ (r)
for all r < a. Observe now that if (1.4) holds, we have

km -2/3 = m 0 -2/3 + 2ǫλm 0 -O(ǫ) ≥ 4ǫλ/3 -O(ǫ) ≥ ǫλ provided λ is big enough. If (1.6) holds, we have km -2/3 = 1 - ǫλ 2m 0 -ǫt 1 (m 0 + ǫλ/2 + ǫT 1 ) -2/3 = m 0 -2/3 + ǫ(T 1 -m 0 t 1 ) -O(ǫ 2 λ 2 ) ≥ ǫm 0 t 1 provided we take T 1 = 3m 0 t 1 . If (1.9) holds, we have km -2/3 = 2 3m 1 - 2νǫλ 3m 2 1 -ǫt 2 (m 1 + νǫλ + ǫT 2 ) -2/3 = 2T 2 3m 1 -m 1 t 2 ǫ -O(ǫ 2 λ 2 ) ≥ ǫm 1 t 2
provided we take

T 2 = 6m 2 1 t 2 . If (1.10) holds, we have km -2/3 = β -1 2 - (β -1)νǫλ 2m 2 -ǫt 3 (m 2 + νǫλ + ǫT 3 ) -2/3 = (β -1)m 2 2 - 2 3 + (β -1)T 3 2 -m 2 t 3 ǫ -O(ǫ 2 λ 2 ) ≥ ǫm 2 t 3
provided we take

T 3 = 6m 2 t 3 β-1 . Using that h ǫλ = ǫ, h ǫ = e -1 , we conclude that (2.11) h km-2/3 ≤            ǫ if (1.4) holds, e -m 0 t 1 if (1.6) holds, e -m 1 t 2 if (1.9) holds, e -m 2 t 3 if (1.10) holds.
Taking ǫ small enough and t 1 , t 2 , t 3 big enough, we obtain from (2.10) and (2.11) that in all cases we have the estimate (2.12)

A(r) ≥ 2kτ (r + 1) -k-1 ϕ ′ (r) - E 4 µ ′ (r)
for all r < a. We will now bound the function B from above. Note that taking h small enough we can arrange that 2b < a/2. Let first 0 < r ≤ a 2 . Since in this case we have ϕ ′ (r) ≥ Cτ (r + 1) -k with some constant C > 0, we obtain

B(r) µ(r) h -2 Q b (r + 1) -2δ + ϕ ′′ (r) 2 h -1 ϕ ′ (r) + µ(r)(1 -ψ b (r))(r + 1) -β Q b (τ h) -1 µ(r)(r + 1) 1+k-2δ ϕ ′ (r) 2 τ (r + 1) -k-1 ϕ ′ (r) + h µ(r)ϕ ′′ (r) 2 µ ′ (r)ϕ ′ (r) µ ′ (r) +(1 -ψ b (r))(r + 1) 2k-β Q b τ -3 h -1 (r + 1) 1+5k-2δ τ (r + 1) -k-1 ϕ ′ (r) + τ hµ ′ (r) +(1 -ψ b (r))(r + 1) 1-β µ ′ (r) Q b τ -3 0 τ (r + 1) -k-1 ϕ ′ (r) + (τ 0 h 2/3 + b -β+1 )µ ′ (r)
where Q b > 0 is some constant depending only on b and we have used that k < (2δ -1)/5 in all three cases. Taking h small enough, depending on τ 0 , and b big enough, independent of h and τ 0 , we get the bound

(2.13) B(r) ≤ C Q b τ -3 0 τ (r + 1) -k-1 ϕ ′ (r) + E 4 µ ′ (r)
with some constant C > 0. In this case we get (2.9) from (2.12) and (2.13) by taking τ 0 big enough depending on b and C but independent of h. Let now a 2 < r < a. Then we have the bound

B(r) µ(r) µ ′ (r) 2 h -1 (r + 1) -δ + |ϕ ′′ (r)| 2 µ ′ (r) + (r + 1) -β+1 µ ′ (r) h -2 (r + 1) 2-2δ + τ 2 (r + 1) -2k µ ′ (r) + a -β+1 µ ′ (r) h -2 a 2-2δ + τ 2 a -2k µ ′ (r) + a -β+1 µ ′ (r) h 2m(δ-1)-2 + h 2km-2/3 + h m(β-1) µ ′ (r) ≤ E 4 µ ′ (r)
provided h is taken small enough. Again, this bound together with (2.12) imply (2.9). It remains to consider the case r > a. Using (2.5) we get

B(r) µ(r) h -1 (r + 1) -δ 2 µ ′ (r) + (r + 1) -β µ(r) ǫ -2 h -2 a 4k (r + 1) 4s-2δ µ ′ (r) + ǫ -1 a 2k (r + 1) 2s-β µ ′ (r) ǫ -2 h -2 a 4k+4s-2δ + ǫ -1 a 2k+2s-β µ ′ (r) h 2m(δ-2k-2s)-2-2ǫλ + h m(β-2k-2s)-ǫλ µ ′ (r)
where we have used that ǫ -1 = h -ǫλ . When (1.4) holds we have

m(δ -2k -2s) -1 -ǫλ = (m 0 + 2ǫλm 0 )(δ -3 + ǫ) -1 -ǫλ ≥ m 0 (δ -3) -1 + ǫλ(2(δ -3)m 0 -1) ≥ ǫλ and m(β -2k -2s) -ǫλ ≥ m 0 (β -3) -O(ǫλ) ≥ m 0 (β -3)/2. When (1.6) holds we have m(δ -2k -2s) -1 -ǫλ = (m 0 + ǫλ/2 + ǫT 1 ) δ -3 + ǫλ m 0 + ǫ(2t 1 -1) -1 -ǫλ = m 0 (δ -3) -1 + (δ -3)ǫλ/2 -O(ǫ 2 λ 2 ) ≥ (δ -3)ǫλ/2 -O(ǫ 2 λ 2 ) ≥ (δ -3)ǫλ/3 and m(β -2k -2s) -ǫλ = (m 0 + ǫλ + ǫT 1 ) ǫλ m 0 + ǫ(2t 1 -1) -ǫλ ≥ ǫt 1 m 0 .
When (1.9) holds we have

m(δ -2k -2s) -1 -ǫλ = (m 1 + νǫλ + ǫT 2 ) δ -1 - 4 3m 1 + 4νǫλ 3m 2 1 + ǫ(2t 2 -1) -1 -ǫλ = m 1 (δ -1) - 7 3 + ((δ -1)ν -1)ǫλ + ǫ((δ -1)T 2 + m 1 (2t 2 -1)) -O(ǫ 2 λ 2 ) ≥ ǫm 1 t 2 and m(β -2k -2s) -ǫλ = (m 1 + νǫλ + ǫT 2 ) β -1 - 4 3m 1 + 4νǫλ 3m 2 1 + ǫ(2t 2 -1) -ǫλ = m 1 (β -1) - 4 3 + ((β -1)ν -1)ǫλ + ǫ((β -1)T 2 + m 1 (2t 2 -1)) -O(ǫ 2 λ 2 ) ≥ ǫm 1 t 2 .
When (1.10) holds we have

m(δ -2k -2s) -1 -ǫλ = (m 2 + νǫλ + ǫT 3 ) δ -β + (β -1)νǫλ m 2 + ǫ(2t 3 -1) -1 -ǫλ = m 2 (δ -β) -1 + ((δ -1)ν -1)ǫλ + ǫ((δ -β)T 3 + m 2 (2t 3 -1)) -O(ǫ 2 λ 2 ) ≥ ǫm 2 t 3 and m(β -2k -2s) -ǫλ = (m 2 + νǫλ + ǫT 3 ) (β -1)νǫλ m 2 + ǫ(2t 3 -1) -ǫλ = ((β -1)ν -1)ǫλ + ǫm 2 (2t 3 -1) -O(ǫ 2 λ 2 ) ≥ ǫm 2 t 3 .
We conclude from the above inequalities that

(2.14) h 2m(δ-2k-2s)-2-2ǫλ + h m(β-2k-2s)-ǫλ ≤            ǫ 2 + h γ if (1.4) holds, ǫ γ + e -m 0 t 1 if (1.6) holds, 2e -m 1 t 2 if (1.9) holds, 2e -m 2 t 3 if (1.10) holds,
with some constant γ > 0 independent of h. It follows from (2.14) that taking h small enough and t 1 , t 2 and t 3 large enough, independent of h, we can arrange the bound

(2.15) B(r) ≤ E 2 µ ′ (r).
Since in this case A(r) = 0, the bound (2.15) clearly implies (2.9). ✷

Carleman estimates

In this section we will prove the following Theorem 3.1. Suppose (1.1), (1.2) and (1.3) fulfilled and let s satisfy (2.1). Then, for all

functions f ∈ H 2 (R n ) such that (|x| + 1) s (P (h) -E ± iθ)f ∈ L 2 and for all 0 < h ≤ h 0 , 0 < θ ≤ ǫha -2k
, we have the estimate

(|x| + 1) -s e ϕ/h f L 2 ≤ Ca 2k (ǫh) -1 (|x| + 1) s e ϕ/h (P (h) -E ± iθ)f L 2 (3.1) +Ca k τ θ ǫh 1/2 e ϕ/h f L 2
with a constant C > 0 independent of h, θ and f .

Proof. We will adapt the proof of Theorem 3.1 of [START_REF] Vodev | Semi-classical resolvent estimates for short-range L ∞ potentials[END_REF] to this more general case. We pass to the polar coordinates (r, w) ∈ R + × S n-1 , r = |x|, w = x/|x|, and recall that L

2 (R n ) = L 2 (R + × S n-1 , r n-1 drdw).
In what follows we denote by • and •, • the norm and the scalar product in L 2 (S n-1 ). We will make use of the identity (3.2) r (n-1)/2 ∆r -(n-1)/2 = ∂ 2 r + ∆ w r 2 where ∆ w = ∆ w -1 4 (n -1)(n -3) and ∆ w denotes the negative Laplace-Beltrami operator on S n-1 . Set u = r (n-1)/2 e ϕ/h f and P ± (h) = r (n-1)/2 (P (h) -E ± iθ)r -(n-1)/2 , P ± ϕ (h) = e ϕ/h P ± (h)e -ϕ/h . Using (3.2) we can write the operator P ± (h) in the coordinates (r, w) as follows

P ± (h) = D 2 r + Λ w r 2 -E ± iθ + V
where we have put D r = -ih∂ r and Λ w = -h 2 ∆ w . Since the function ϕ depends only on the variable r, this implies

P ± ϕ (h) = D 2 r + Λ w r 2 -E ± iθ -ϕ ′2 + hϕ ′′ + 2iϕ ′ D r + V. We now write V = V S + V L with V S (x) = V S (x) + ψ b (|x|)V L (x) and V L (x) = (1 -ψ b (|x|))V L (x). For r > 0, r = a, introduce the function F (r) = -(r -2 Λ w -E -ϕ ′ (r) 2 + V L (r, •))u(r, •), u(r, •) + D r u(r, •) 2
where V L (r, w) := V L (rw). It is easy to check that its first derivative is given by

F ′ (r) = 2 r r -2 Λ w u(r, •), u(r, •) + ((ϕ ′ ) 2 -V L ) ′ u(r, •) 2 -2h -1 Im P ± ϕ (h)u(r, •), D r u(r, •) ±2θh -1 Re u(r, •), D r u(r, •) + 4h -1 ϕ ′ D r u(r, •) 2 +2h -1 Im ( V S + hϕ ′′ )u(r, •), D r u(r, •) .
Thus, if µ is the function defined in the previous section, we obtain the identity

µ ′ F + µF ′ = (2r -1 µ -µ ′ ) r -2 Λ w u(r, •), u(r, •) + (Eµ ′ + (µ(ϕ ′ ) 2 -µ V L ) ′ ) u(r, •) 2 -2h -1 µIm P ± ϕ (h)u(r, •), D r u(r, •) ±2θh -1 µRe u(r, •), D r u(r, •) + (µ ′ + 4h -1 ϕ ′ µ) D r u(r, •) 2 +2h -1 µIm ( V S + hϕ ′′ )u(r, •), D r u(r, •) .
Using that Λ w ≥ 0 together with (2.3) we get the inequality

µ ′ F + µF ′ ≥ (Eµ ′ + (µ(ϕ ′ ) 2 -µ V L ) ′ ) u(r, •) 2 + (µ ′ + 4h -1 ϕ ′ µ) D r u(r, •) 2 - 3h -2 µ 2 µ ′ P ± ϕ (h)u(r, •) 2 - µ ′ 3 D r u(r, •) 2 -θh -1 µ u(r, •) 2 + D r u(r, •) 2 -3h -2 µ 2 (µ ′ + 4h -1 ϕ ′ µ) -1 ( V S + hϕ ′′ )u(r, •) 2 - 1 3 (µ ′ + 4h -1 ϕ ′ µ) D r u(r, •) 2 .
In view of the assumptions (1.2) and (1.3) we have

(µ V L ) ′ = µ ′ V L + µ V ′ L = µ ′ (1 -ψ b )V L -µψ ′ b V L + µ(1 -ψ b )V ′ L ≤ µ ′ (1 -ψ b )p(r) + µb -1 φ(r/b)p(r) + µ(1 -ψ b )C 2 (r + 1) -β ≤ µ ′ (1 -ψ b )p(b) + O(r)b -1 φ(r/b)p(b)µ ′ + µ(1 -ψ b )C 2 (r + 1) -β ≤ O(1)p(b)µ ′ + µ(1 -ψ b )C 2 (r + 1) -β ≤ E 3 µ ′ + µ(1 -ψ b )C 2 (r + 1) -β
provided b is taken large enough. Observe also that the assumption (1.1) yields

| V S | ≤ |V S | + ψ b |V L | ≤ C 1 (r + 1) -δ + Q b ψ b where Q b = sup |x|≤2b |V L (x)|.
Combining the above inequalities we get

µ ′ F + µF ′ ≥ 2E 3 µ ′ + (µ(ϕ ′ ) 2 ) ′ u(r, •) 2 -3µ 2 (µ ′ + h -1 ϕ ′ µ) -1 (h -1 C 1 (r + 1) -δ + h -1 Q b ψ b + |ϕ ′′ |) 2 + µ(1 -ψ b )C 2 (r + 1) -β u(r, •) 2 - 3h -2 µ 2 µ ′ P ± ϕ (h)u(r, •) 2 -θh -1 µ u(r, •) 2 + D r u(r, •) 2 = 2E 3 µ ′ + A(r) -B(r) u(r, •) 2 - 3h -2 µ 2 µ ′ P ± ϕ (h)u(r, •) 2 -θh -1 µ u(r, •) 2 + D r u(r, •) 2 .
Now we use Lemma 2.3 to conclude that

µ ′ F + µF ′ ≥ E 6 µ ′ u(r, •) 2 - 3h -2 µ 2 µ ′ P ± ϕ (h)u(r, •) 2 -θh -1 µ u(r, •) 2 + D r u(r, •) 2 .
We integrate this inequality with respect to r and use that, since µ(0) = 0, we have

∞ 0 (µ ′ F + µF ′ )dr = 0.
Thus we obtain the estimate

E 6 ∞ 0 µ ′ u(r, •) 2 dr ≤ 3h -2 ∞ 0 µ 2 µ ′ P ± ϕ (h)u(r, •) 2 dr (3.3) +θh -1 ∞ 0 µ u(r, •) 2 + D r u(r, •) 2 dr.
Using that µ = O(a 2k ) together with (2.4) and (2.6) we get from (3.3)

∞ 0 (r + 1) -2s u(r, •) 2 dr ≤ Ca 4k (ǫh) -2 ∞ 0 (r + 1) 2s P ± ϕ (h)u(r, •) 2 dr (3.4) +Cθ(ǫh) -1 a 2k ∞ 0 u(r, •) 2 + D r u(r, •) 2 dr
with some constant C > 0 independent of h and θ. On the other hand, we have the identity

Re ∞ 0 2iϕ ′ D r u(r, •), u(r, •) dr = ∞ 0 hϕ ′′ u(r, •) 2 dr and hence Re ∞ 0 P ± ϕ (h)u(r, •), u(r, •) dr = ∞ 0 D r u(r, •) 2 dr + ∞ 0 r -2 Λ w u(r, •), u(r, •) dr - ∞ 0 (E + ϕ ′2 ) u(r, •) 2 dr + ∞ 0 V u(r, •), u(r, •) dr. This implies ∞ 0 D r u(r, •) 2 dr ≤ O(τ 2 ) ∞ 0 u(r, •) 2 dr (3.5) +γ ∞ 0 (r + 1) -2s u(r, •) 2 dr + γ -1 ∞ 0 (r + 1) 2s P ± ϕ (h)u(r, •) 2 dr
for every γ > 0. We take now γ small enough, independent of h, and recall that θ(ǫh) -1 a 2k ≤ 1. Thus, combining the estimates (3.4) and (3.5), we get

∞ 0 (r + 1) -2s u(r, •) 2 dr ≤ Ca 4k (ǫh) -2 ∞ 0 (r + 1) 2s P ± ϕ (h)u(r, •) 2 dr (3.6) +Cθ(ǫh) -1 a 2k τ 2 ∞ 0 u(r, •) 2 dr
with a new constant C > 0 independent of h and θ. Clearly, the estimate (3.6) implies (3.1). ✷

Resolvent estimates

Theorems 1.1 and 1.2 can be obtained from Theorem 3.1 in the same way as in Section 4 of [START_REF] Vodev | Semi-classical resolvent estimates for short-range L ∞ potentials[END_REF]. Here we will sketch the proof for the sake of completeness. Observe that it follows from the estimate (3.1) and Lemma 2.2 that for 0 < h ≪ 1, 0 < θ ≤ ǫha -2k and s satisfying (2.1) we have the estimate It follows from (4.4) that the resolvent estimate (4.5) (|x| + 1) -s (P (h) -E ± iθ) -1 (|x| + 1) -s L 2 →L 2 ≤ 4M 2 holds for all 0 < h ≪ 1, 0 < θ ≤ ǫha -2k and s satisfying (2.1). On the other hand, for θ ≥ ǫha -2k the estimate (4.5) holds in a trivial way. Indeed, in this case, since the operator P (h) is symmetric, the norm of the resolvent is upper bounded by θ -1 = O(h -2km-2 ). Finally, observe that if (4.5) holds for s satisfying (2.1), it holds for all s > 1/2 independent of h. Indeed, given an arbitrary s ′ > 1/2 independent of h, we can arrange by taking h small enough that s defined by (2.1) is less than s ′ . Therefore the bound (4.5) holds with s replaced by s ′ as desired.

1 )Ch - 4 / 3

 143 -s f L 2 ≤ M (|x| + 1) s (P (h) -E ± iθ)f L 2 + M θ 1/2 f L 2 log(h -1 ) if (1.4) holds,Ch -4/3 (log(h -1 ))

  3/2 (log log(h -1 )) -1 if (1.6) holds, On the other hand, since the operator P (h) is symmetric, we haveθ f 2 L 2 = ±Im (P (h) -E ± iθ)f, f L 2 (4.2) ≤ (2M ) -2 (|x| + 1) -s f 2 L 2 + (2M ) 2 (|x| + 1) s (P (h) -E ± iθ)f 2 L 2 . -s f L 2 + 2M 2 (|x| + 1) s (P (h) -E ± iθ)f L 2 . -s f L 2 ≤ 4M 2 (|x| + 1) s (P (h) -E ± iθ)f L 2 .

		Ch -2 3 -m 1 (log(h -1 )) ν	if (1.9) holds,
		Ch -4 3 -1
	We rewrite (4.2) in the form
	(4.3) (|x| + 1) We now combine (4.1) and (4.3) to get M θ 1/2 f L 2 ≤ 1 2
	(4.4)	(|x| + 1)

2 (3-β)m 2 (log(h -1 )) ν if (1.10) holds,

with a constant C > 0 independent of h and θ.


Pascal Lafourcade
email: pascal.lafourcade@uca.fr

Matthieu Giraud
email: matthieu.giraud@uca.fr

Narjes Ben

Mouhebeddine Berrima
email: berrima.mouheb@gmail.com

Narjes Ben Rajeb
email: narjes.benrajeb@gmail.com

Formal Analysis of a Private Access Control Protocol to a Cloud Storage

Keywords: Cloud storage, formal methods, attribute based signature, attribute based encryption, data and user privacy

come

Formal analysis of a private access control protocol to a cloud storage

Mouhebeddine Berrima,

Introduction

Cloud storage refers to data storage services hosted over Internet. The cloud users store data online, so other authorized users can access them from any location via the Internet. Due to the features of cloud storage such as large storage capacity, high availability, scalability and reduced costs, many applications manipulating sensitive data are using a cloud storage. However, sharing sensitive data on a third party through a public network brings some security challenges. In particular, there are concerned with the privacy of users and data. Protecting privacy in clouds is more difficult than in traditional environments, because sensitive data may be disseminated and stored over many external locations managed by external service providers [START_REF] Wang | Toward publicly auditable secure cloud data storage services[END_REF], and both cloud and their user can be malicious [START_REF] Mulazzani | Dark clouds on the horizon: Using cloud storage as attack vector and online slack space[END_REF][START_REF] Zhang | Key research issues for privacy protection and preservation in cloud computing[END_REF]. User privacy is required in many applications where users have a right of privacy when storing their sensitive information like financial or health data [START_REF] Tang | Study on data security of cloud computing[END_REF]. There are two important privacy requirements when a user stores data on the cloud: anonymity and unlinkability. The ISO/IEC standard (governmental organisations, 2009) define anonymity as the property ensuring that a user may use a service or a resource without disclosing his (or her) identity. However, preserving the anonymity property may still release information about a user by allowing an adversary to track several uses of a resource by the same user. Such information might allow an adversary to deduce or at least restrict the possible identities of a user. Therefore, the unlinkability property is required, ensuring that the different uses of a service or a resource for the same user should not be linked by an adversary. On the other hand, the Cloud Service Provider (CSP) must authenticate the user to be sure that he has the right to store data on the cloud, moreover this authentication must be done without reveal any information about his identity. As a concrete example, consider an employer in an institution learning about a corruption while going through some records. He decides to send the records in question to the authority for combating corruption using a cloud storage service while retaining her anonymity, but with a proof that she indeed has access to these records. The challenge of privacy-preserving authentication of users is one of the main concern in cloud security. There are few cryptographic schemes which can be used in these situations like anonymous authentication [START_REF] Cramer | Proofs of partial knowledge and simplified design of witness hiding protocols[END_REF], group signatures [START_REF] Chaum | Group signatures[END_REF], ring signatures [START_REF] Rivest | How to leak a secret[END_REF], mesh signatures [START_REF] Boyen | Mesh signatures[END_REF] and Attribute-Based Signature (ABS) [START_REF] Maji | Attribute-based signatures: Achieving attribute-privacy and collusion-resistance[END_REF]. In a cloud environment, group signature can not be used because it assumes the preexistence of a group which is difficult in the cloud. Ring signature is not feasible not only because of a large number of users, but also the signer cannot know who these people are. Also the mesh signature can not be used since does not provide a way to convince that a message was endorsed by a single user, and so, can be endorsed by many users colluding together. ABS is the most convenient cryptographic scheme for privacypreserving authentication in the cloud. In ABS, a signer possessing a set of attributes can sign a message with a claim predicate that is satisfied by his attributes. The verifier can only check if the message is signed by an authorized user without knowing any information about its identity.

Data Privacy has been also gained research interest because only authorized users have access to sensitive data on the cloud. Data must be protected when transmitted to CSP and during the storage. The protection is against the unauthorized users as well as the CSP since the cloud is often assumed to be honest and curious, which means that the cloud can be interested by the user's information, but can not modify it [START_REF] Li | Securing personal health records in cloud computing: Patientcentric and fine-grained data access control in multiowner settings[END_REF][START_REF] Yu | Attribute based data sharing with attribute revocation[END_REF]. To ensure data privacy, several works propose the storage of data in encrypted form. Thus, if the storage is compromised, then the leaked information should be protected or at least limited. Identity-based cryptography is not feasible in this situation because the inability of users to share their encrypted data at a fine-grained level. Attribute-Based Encryption (ABE) [START_REF] Sahai | Fuzzy identity-based encryption[END_REF] solves the problem of fine-grained access control. There are two complimentary forms of ABE defined by [START_REF] Goyal | Attribute-based encryption for fine-grained access control of encrypted data[END_REF]: Ciphertext-Policy Attribute-Based Encryption (CP-ABE) and Key-Policy Attribute-Based Encryption (KP-ABE). In a CP-ABE system, the users have given a set of attributes and the data are encrypted under an access policy described as a Boolean formula. Only users having the attributes satisfying the access policy can decrypt the ciphertext. In a KP-ABE system, the situation is reversed: users are associated with access policies and ciphertexts are encrypted with sets of attributes.

Many approaches and techniques have been proposed to deal with security and privacy in cloud storage [START_REF] Huang | Service chaining for hybrid network function[END_REF][START_REF] Hosseinzadeh | Obfuscation and diversification for securing cloud computing[END_REF][START_REF] Grover | A framework for cloud data security[END_REF][START_REF] Giraud | Practical passive leakage-abuse attacks against symmetric searchable encryption[END_REF]. In addition, some works have been interested in security for mobile cloud computing and Internet of Things (IoT), e.g [START_REF] Stergiou | Secure integration of iot and cloud computing[END_REF][START_REF] Memos | An efficient algorithm for media-based surveillance system (eamsus) in iot smart city framework[END_REF][START_REF] Zkik | Secure mobile multi cloud architecture for authentication and data storage[END_REF][START_REF] Ibtihal | Homomorphic encryption as a service for outsourced images in mobile cloud computing environment[END_REF]. Taking advantages of ABS and ABE has emerged as a widely accepted approach by the cloud security community [START_REF] Dahshan | Framework for securing data in cloud storage services[END_REF][START_REF] Wang | An access control method based on cp-abe and abs algorithm in cloud storage[END_REF][START_REF] Belguith | Pabac: a privacy preserving attribute based framework for fine grained access control in clouds[END_REF][START_REF] Alsmirat | Internet of surveillance: a cloud supported large-scale wireless surveillance system[END_REF][START_REF] Shakunthala | Decentralized access control with anonymous authentication of data stored in clouds[END_REF]. The ABS is used to ensure the authentication while hiding anonymity, and the ABE allows a fine-grained access control to data. The cloud storage protocol proposed by [START_REF] Ruj | Privacy preserving access control with authentication for securing data in clouds[END_REF] is among the pioneering works to use ABS and ABE. The protocol uses the SSH protocol to secure all the communication between the users and the cloud, and it supports reading and writing data stored in the cloud. However, the security protocols are error-prone and difficult to be evaluated using simulation techniques or conventional test. This has encouraged the researchers to formally analyze security protocols [START_REF] Kremer | Analysis of an electronic voting protocol in the applied pi calculus[END_REF][START_REF] Cremers | Comparing state spaces in automatic security protocol analysis[END_REF][START_REF] Delaune | A formal analysis of authentication in the tpm[END_REF][START_REF] Chen | Design and formal analysis of a group signature based electronic toll pricing system[END_REF][START_REF] Bansal | Keys to the cloud: Formal analysis and concrete attacks on encrypted web storage[END_REF][START_REF] Puys | Formal analysis of security properties on the opcua scada protocol[END_REF]. To the best of our knowledge, there is no formal modeling yet of ABE or ABS schemes using symbolic formalism as applied π-calculus.

Contributions: In this work we enhance the security of cloud storage services based on the attribute-based cryptography, through a formal analysis of [START_REF] Ruj | Privacy preserving access control with authentication for securing data in clouds[END_REF] protocol. We consider this protocol, which we call RSN'12 protocol, because it uses both decentralized ABS and ABE schemes, which are more suitable for a large-scale environment, and it is widely accepted by the cloud security community.

• We model it in the applied π-calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], which allows us to model various cryptographic primitives with some equational theories. We use ProVerif tool [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF] which is one of the most used and efficient tools to analyze cryptographic protocols [START_REF] Puys | Evaluations of cryptographic protocols: Verification tools dealing with algebraic properties[END_REF][START_REF] Cremers | Comparing state spaces in automatic security protocol analysis[END_REF]. For sake of simplicity, we consider one attribute in our symbolic modeling of the ABE and ABS schemes, which can support more than one policy for signature and encryption.

• We formalize and verify the fundamental security properties of the protocol. In writing mode, we verify the writer authentication and writer privacy which is expressed by the anonymity of writer's identity and unlinkability, that is a user who stores data on the cloud. While in reading mode, we check the required property that is data privacy. We show that the unlinkability of a writer is not satisfied against an attack in which the adversary delays the messages of some writers. Then, we propose a fix, which prevents this attack.

• We also discuss some ambiguous aspects of RSN'12 protocol concerning the use of SSH protocol to secure connections, and the use of timestamps to prevent replay attacks.

A preliminary version of this paper appeared in [START_REF] Berrima | Formal analyze of a private access control protocol to a cloud storage[END_REF].

Outline: In Section 2, we give a description of SSH protocol, ABS and ABE schemes and RSN'12 protocol. In Section 3, we briefly introduce applied π-calculus and ProVerif tool. We model RSN'12 protocol in Section 4 and analyze the security properties in Section 5. Finally, we conclude in Section 6.

RSN'1Protocol Description

Ruj et al. [START_REF] Ruj | Privacy preserving access control with authentication for securing data in clouds[END_REF] propose a protocol for reading and writing data stored in the cloud. The protocol is based on the decentralized approach of CP-ABE [START_REF] Lewko | Decentralizing attribute-based encryption[END_REF] and ABS [START_REF] Maji | Attribute-based signatures: Achieving attribute-privacy and collusion-resistance[END_REF], where many authorities distribute secret keys associated to attribute. Using ABS the cloud verifies the authenticity of a user without knowing his identity before storing data. Using ABE only valid users are able to decrypt the stored data. The protocol makes the following assumptions:

• The CSP is honest-but-curious, i.e. the CSP is interested to view the user's information. So it tries to derive some information from the messages he learned during the execution of the protocol, but cannot modify the user's content.

• Users can have either read or write or both access to a file stored in the CSP.

• All the communication between participants are secured by SSH (Secure Shell) protocol.

Before presenting the protocol, we give some cryptographic background.

Cryptographic Background

The security of Ruj et al. protocol is based on the SSH protocol and two cryptographic schemes which are: Attribute-Based Encryption (ABE) and Attribute-Based Signature (ABS). SSH protocol:. SSH (Secure Shell) is a widely deployed secure network protocol. Currently, SSH Version 2 is the recent specification for SSH. It is composed of three subprotocols:

• Transport Protocol : It establishes session keys and ensures authentication of the server, confidentiality, and integrity of the communication. It prevents also replay attack using monotonically increasing sequence numbers.

• Authentication Protocol : It authenticates the user who is about to log in to the server.

• Connection protocol : It establishes different communication channels within an SSH session.

In SSH authentication sub-protocol there are three methods to authenticate the client [START_REF] Ylonen | The secure shell (ssh) authentication protocol[END_REF]. We consider "public key" method in which a user sends a signature created with his private key. The server must check that the key is a valid authenticator for the user and that the signature is valid.

Multi-authority ABS system:. ABS is a cryptographic scheme that allows a party, who possesses a set of attributes from an authority, to sign a message with a predicate, called claim policy, that is satisfied by his attributes. The signature reveals no more than the fact that a single user, whose his attributes satisfy the predicate, has signed the message. Moreover, the signature hides the attributes used to satisfy author the predicate. Then, ABS is used in applications requiring anonymous authentication. In a decentralized environment, there are multiple authorities for distributing attributes to users. These attribute authorities may not trust each other, nor even be aware of each other. However, a separate trusty authority is required to coordinate attribute authorities and set up the various public parameters of the ABS. The security properties of an ABS scheme are:

• Perfect privacy: The signature does not leak which attributes were used to generate it, nor any other user's identifying information.

• Collusion-resistance: Different parties cannot pool together their attributes to sign a message with a claim predicate which none of them satisfy alone.

• Unforgeability: Ensures that a signature was endorsed by one party who satisfies the condition described in the claim predicate, i.e. a party that does not possess the expected attributes, cannot generate a valid signature.

We give the formal definition of ABS. Let A be the universe of possible attributes. A claim predicate over A is a monotone Boolean function, whose input attributes are associated with attributes of A.

Multi-Authority ABS [START_REF] Maji | Attribute-based signatures: Achieving attribute-privacy and collusion-resistance[END_REF]: A multi-authority ABS scheme consists of the following algorithms:

• TSetup: Runs by the signature authority to produce a trusty public key T P K and trusty secret key T SK. The authority publishes T P K and stores T SK.

• TRegister: When a user with identity uid registers with the signature authority, the authority runs T Register(T SK, uid) which outputs a public usertoken τ . The authority gives τ to the user.

• ASetup: An attribute authority who wishes to issue attributes runs ASetup(T P K) which outputs an attribute-authority public key AP K and an attribute-authority secret key ASK. The attribute authority publishes AP K and stores ASK.

• AttrGen: When an attribute authority needs to issue an attribute u ∈ A to a user uid, first it obtains (from the user) her user-token τ , and runs the token verification algorithm T okenV erif y(T P K, uid, τ ). If the token is verified, then it runs AttrGen(ASK, τ, u) which outputs an attribute key K u . The attribute authority gives K u to the user.

• Sign: A user signs a message m with a claimpredicate Υ, only if there is a set of attributes A such that Υ(A) = 1, the user has obtained a set of keys {K u | u ∈ A} from the attribute authorities.

Then the signature σ can be generated using

Sign(T P K, {AP K auth(u) | u ∈ A Υ }, τ, {K u | u ∈ A}, m, Υ).
Here auth(u) stands for the authority who owns the attribute u, and A Υ is the set of attributes appearing in Υ. (m, Υ, σ) can be given out for verification.

• Verify: To verify a signature σ on a message m with a claim-predicate Υ, a user runs

V erif y(T P K, {AP K auth(u) | u ∈ A Υ }, m, Υ, σ)
which outputs a Boolean value, accept or reject.

Multi-authority ABE system:. CP-ABE encryption allows encrypting data under an access policy expressed as a Boolean formula over a set of attributes, so that the decryption succeeds only for the users possessing the attributes which satisfy the access policy. Decryption is performed by using secret attribute keys, associated with the attributes of the user, and issued by an attribute authority. In the Multi-Authority CP-ABE system [START_REF] Lewko | Decentralizing attribute-based encryption[END_REF], any party can act as an authority by creating a public key and issuing private keys to different users that reflect their attributes. There is no requirement for any global coordination or central authority other than the creation of an initial set of common public parameters. To ensure the property of collusion resistance, the authors use the concept of global identifiers to "link" secret attribute keys together that were issued to the same user by different authorities.

Multi-Authority CP-ABE (Lewko and Waters, 2011):

A multi-authority Ciphertext-Policy Attribute-Based Encryption system is formed of the following five algorithms:

• GlobalSetup(λ) → GP: It takes in the security parameter λ and outputs global parameters GP .

• AuthoritySetup(GP) → (SK,PK): Each authority runs the authority setup algorithm with GP as input to produce its own secret key and public key pair, (SK, P K).

• Encrypt(M, (A, ρ), GP, {P K}) → CT : It takes in a message M , an access matrix (A, ρ), the set of public keys for relevant authorities, and the global parameters. It outputs a ciphertext CT .

• KeyGen(GID, GP, i, SK) → K i,GID : It takes in identity GID, the global parameters, an attribute i belonging to some authority, and the secret key SK for this authority. It produces a key K i,GID for this attribute, identity pair.

• Decrypt(CT, GP, {K i,GID }) → M : It takes in the global parameters, the ciphertext, and a collection of keys corresponding to attribute, identity pairs all with the same fixed identity GID. It outputs either the message M when the collection of attributes i satisfies the access matrix corresponding to the ciphertext. Otherwise, decryption fails.

RSN'12 Protocol

The protocol involves a user who may be a writer or a reader or both, a trusty authority (TA) registering users, one or more Key Distribution Center (KDC) issuing the secrets keys associated with users' attributes, and the CSP. TA and KDCs are trusted entities, CSP is a semi-trusted entity. However, some users may be malicious and thus are considered as untrusted entities.

The protocol is composed of three sub-protocols. Registering and getting attribute secret keys:. In a first phase, a user gets attribute secret keys from the KDCs by presenting his token obtained from the TA:

• The user presents his identity to the TA, for instance a federal government ( 1 in Figure 1).

• The TA registers the user if he is eligible and gives him a token as described in ABS scheme ( 2 in Figure 1). The TA embeds a random value in the token. This random value will be incorporated in the attribute secret keys for signing to prevent collusion of the users.

• If a user presents the token to one or more KDCs then she receives secret attribute keys for signing and decryption ( 3 in Figure 1). The KDC checks the validity of the token using the TA's public key, and sends the corresponding keys for signing and decryption ( 4 in Figure 1).

Writing on the cloud:. To store a message M SG on the cloud, the user proceeds as follows:

• The user creates an access policy X containing all required fields, and encrypts the message M SG under X as C = Encrypt(M SG, X ) ( 1 in Figure 2).

• Then he calculates the message

C 1 = H(C) τ
where H is a hash function, τ is a timestamp and is the concatenation operation. The timestamp is used to prevent the user to use stale message back with a valid signature when his attributes have been revoked. Next, he generates the signature σ of C 1 with a claim policy Y ( 2 in Figure 2).

• Finally, the user sends c = (C, τ, σ, Y) to the CSP ( 3 in Figure 2). Then CSP verifies, using V erif y algorithm, if the message H(C) τ was signed by a user satisfying the claim policy Y.

Reading from the cloud:. A user can access at any time to the data and requests a ciphertext, then the CSP sends the requested ciphertext using SSH.

Note that, the authors do not propose any revocation model, but it is still possible to incorporate a revocation model. The protocol specification is clear but contains some ambiguities. Next, we discuss these minor problems and explain how to fix them. Timestamps: They are used to prevent the writing when the attributes and keys of a writer have been revoked, since a timestamp informs of the time when the message was created. However a writer signs its message along with a timestamp generated by himself. Then a verifier cannot really be sure, since the signer may include an arbitrary timestamp. Then in order to address this problem, we recommend the use of a trusted timestamping described in RFC 3161 [START_REF] Adams | Internet x.509 public key infrastructure timestamp protocol (tsp)[END_REF], where the writer sends the hash of its message ( 1 in Figure 3) to a trusted third party called TSA-Time-Stamping Authority ( 2 in Figure 3). Then, the TSA concatenates a timestamp τ to the hash and calculates the hash of this concatenation. This hash is then digitally signed with the private key of TSA to give the signature σ ( 3 in Figure 3). Then, the writers sends to the CSP, the message, the timestamp and the signature ( 4 in Figure 3). This role of TSA can be ensured by the trusted entity TA in the RSN'12 protocol. Writer and SSH connection to the CSP: In writing access, the protocol uses SSH connection between users and the CSP which is assumed to be semi-trusted. However, when establishing SSH connection the CSP knows the user's identity following the execution of SSH authentication sub-protocol [START_REF] Ylonen | The secure shell (ssh) authentication protocol[END_REF], which compromises the user privacy against the CSP. This ambiguity can be easily addressed by configuring the SSH server of the CSP to allow a user to login without any user authentication.

Reader and SSH connection to the CSP: In reading access the SSH connection is useless because the

author 1 C = Encrypt(M SG, X ) 2 C 1 = H(C) τ , σ, Y CSP User 3 (C, τ, σ, Y)
Figure 2: Writing on the cloud.

1 C = Encrypt(M SG, X ) 2 C 1 = H(C) 3 C 2 = H (C 1 τ ), σ CSP User TSA 4 (C, C 2 , σ)
Figure 3: Writing on the cloud with a TSA. messages are encrypted using ABE and only authorized users can decrypt them. Hence, we can drop the SSH connection between a reader and the CSP, thus helping to reduce the performance overhead due to a large number of SSH connections.

Computational complexity

The computational complexity of the protocol relies on the practical instantiations used for ABS and ABE schemes. The instantiation of ABS scheme in [START_REF] Maji | Attribute-based signatures: Achieving attribute-privacy and collusion-resistance[END_REF] requires cyclic groups of prime order equipped with bilinear pairing. Signing a message needs 2w + l(1 + 2t) + 3 exponentiation, where l and t are the dimensions of the monotone span program representing the claim policy and w is the minimum number of attributes to satisfy the claim policy. Checking a signature requires (l + 2t) pairing operation. Note that there is a probabilistic verification requiring only l + 4 pairings, at the cost of additional exponentiations and a very small probability of false positive [START_REF] Maji | Attribute-based signatures: Achieving attribute-privacy and collusion-resistance[END_REF]. The probabilistic verification is more efficiency because pairing operation is most expensive operation. The instantiation of ABE scheme in [START_REF] Lewko | Decentralizing attribute-based encryption[END_REF] works in composite bilinear groups. The encryption takes 5m exponentiations and 1 pairing operation, with m is the number of attributes. The decryption takes 2m + 1 pairing operation.

Applied π-calculus

We give a brief overview of the applied π-calculus, a language for describing concurrent processes and their interactions and handling cryptographic primitives [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF].

Syntax and Semantics

Given a signature Σ, an infinite set of names, and an infinite set of variables, the set of terms are defined by L, M, N, T, U, V ::= terms k, . . . , n, . . . , s names x, y, z variables f (M 1 , . . . , M k ) function application

An equational theory over a signature usually consists of a set of equations asserting the equality of cryptographic primitives. We usually use E to denote an equational theory. The notation M = E N means that the equation M = N holds in the theory E. A protocol is modeled as a set of processes defined by the grammar described in The null process cannot perform any actions. A parallel composition P |Q represents the combined behavior of P and Q executing in parallel. The replication !P behaves as an infinite number of copies of P running in parallel. The process new n; P generates a new name n then behaves as P. The name n is bound, i.e. it is not accessible to the environment. The process if M = E N then P else Q behaves as P if M = E N , otherwise it behaves as Q. The input process in(c, x); P is ready to input a message on the channel c, then to run P {M/x}, i.e. to run P with the message M replaced by the formal parameter x. The output process out(c, M ); P is ready to output a message M on channel c, then to run P . The active substitution {M/x} replaces the variable x with the term M . The active substitution {M/x} typically appears when the term M has been sent to the environment. A process is closed if all variables are bound either by an input or by an active substitution. We use C[ ] to denote a context (a process with a whole) and C[P ] is a process obtained by filling the whole with process P . An evaluation context is a context whose hole is not under a replication, a conditional, an input, or an output.

The operational semantics of the applied π-calculus contains structural equivalence, internal reduction (denoted as →) and labelled reduction (denoted as α -→). The structural equivalence defines the equivalence relations between two processes which differ only in structure. Internal reduction means that a process can execute an action without interaction with the environment, while labelled reduction means that a process interacts with the environment. Transition A α -→ B indicates that A executes α and then continues as B.

Many properties of security protocols are formalized in terms of observational equivalence between processes. To define it, we use A ↓ c to denote that process A can send a message on c.

Observational equivalence (≈):

As defined in [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], observational equivalence is the largest symmetric relation R between closed extended processes with the same domain such that ARB implies:

1. if A ↓ a then B ↓ a, 2. if A → * A then B → * B and ARB for some B , 3. if C[A]RC[B] for closing evaluation context C.
Moreover, we consider an active adversary who is able to access to any message sent on public channel, and also to insert, delay and remove messages. In the applied πcalculus the sender's identity of a message is unknown, unless the identity is specified explicitly in the conveyed message.

ProVerif

ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF]) is a tool for automatically proving cryptographic protocols. The input of the ProVerif is a protocol modeled in the applied π-calculus. It outputs whether this protocol satisfies or not a security property which is described as a query. ProVerif is sound but not complete, if ProVerif says that a property is satisfied, then the model really guarantees that property. However, if ProVerif detects a flaw, it might be a false attack due to the nonce approximation done in ProVerif.

ProVerif can analyze three types of security properties. The first one is the reachability. It allows evaluating the availability of a given term to an attacker. It is usually used to model the secrecy of a message. The second one is the correspondence assertion which is used to capture a relation between events. Formally, a correspondence property is an expression of the form ev(M 1 , . . . , M n ) ⇒ ev (N 1 , . . . , N k ), where M i , N j are terms with variables. The property holds if on every execution trace, each occurrence of ev(M 1 . . . , M n ) is preceded by an occurrence of ev (M 1 , . . . , M n ). To reason with correspondence the grammar of extended process of Figure 4 are enriched by events of the form event e(M 1 , . . . , M n ); P . These events mark important stages reached by the protocol but do not otherwise affect the behavior of the protocol. The third one is so-called diff-equivalence, which allows us to reason about complex properties that cannot be expressed as reachability or correspondence assertions. It is defined between two processes having the same structure but differs only in the choice of terms. Given two processes P and Q, diff-equivalence is written by the notion of biprocess that encodes both P and Q. Such a biprocess uses the construct choice[M, M ] to represent the terms that differ between P and Q. Thus, P uses the first component of the choice, M , while Q uses the second one, M . Note that diff-equivalence is stronger than the observational equivalence defined in applied π-calculus (Definition 3.1). This means that in some cases ProVerif fails to prove diff-equivalence between two processes which are observationally equivalent in the sense of Definition 3.1.

Modeling in Applied π-calculus

We define a specific equational theory with abstraction for SSH protocol, ABS and ABE schemes. Then we model the protocol in the applied π-calculus from the viewpoint of four types of principals. In our abstraction of ABS and ABE schemes, for sake of simplicity, we consider one attribute and consequently, the protocol involves one KDC. However, our modeling of the claim and access policies can be extended to consider more than one attribute, one access policy, and one claim policy.

Equational Theory

We describe the equations modeling the cryptographic primitives used within RSN'12 protocol. author Standard cryptographic primitives:. SSH protocol includes standard primitives such as symmetric and asymmetric encryption, digital signature and concatenation of messages. Symmetric encryption: A symmetric encryption scheme allows the sender to encrypt his message using a shared secret key k, whereas a symmetric decryption algorithm allows the receiver to decrypt the ciphertext using k. The functions senc and sdec model, respectively, encryption and decryption. The decryption of an encrypted message senc(k,msg) is modeled by the following equation:

sdec(k,senc(k,msg)) = msg
Asymmetric encryption: In such encryption scheme, each participant of a protocol possesses a pair of keys, one private only known by the owner and used to decrypt ciphertexts, and the other one public used to encrypt messages. To model this scheme, we consider a constant sk (function of arity 0) representing a private key and a function pk for generating public key corresponding to sk. The function adec models the decryption of an encrypted message msg represented by the term aenc(sk,msg) as described by the following equation: adec(sk,aenc(pk(sk),msg))

Digital signature: It is used in the authentication of message and thus the authenticity of participants. Nonmessage revealing digital signature is a digital signature which does not allow getting the message from the signature. In a similar way to asymmetric encryption, digital signatures rely on a private and public keys. The private key serves for computing signatures and the public key for verifying those signatures. In order to model a non-message revealing digital signatures and their verifiable, in addition to the function pk from asymmetric encryption, we use function sign for constructing signatures and the function checksign to check the signature, and returning true only when the signature is correct.

In ABE scheme each KDC has a private key and a public key derived from its secret one using the function abePk. The evaluation of access policy and the verification of attribute secret key using respectively abeEval and abeKeyCheck are similar to ABS scheme as is shown by the equations (ABE-1) and (ABE-2). An attribute secret key associated to an attribute att, and delivered by a KDC with private key ASK to a user of identity uid, is denoted by the term abeSka(ASK,uid,att). Here the uid of the user appears in the attribute keys because the technique preventing the collusion of users embeds the user's identifier uid into the attribute keys. The encryption algorithm, denoted by the function abeEnc, takes as input a plaintext, the access policy and the public key of the relevant authority, thus an encrypted message is denoted by a term like abeEnc(abePk(ASK),AccessP,msg). The equation (ABE-3) describes the decryption algorithm abeDec. It outputs the message msg only when the attribute secret key corresponds to the attribute att.

We now model the role of participants in the protocol and their interactions. We start by modeling the role of SSH client and SSH server, then we describe the processes of RSN'12 protocol and its participants.

Modeling SSH Protocol

To model the transport sub-protocol, only the symmetric encryption is considered, i.e. we ignore the MAC and compression algorithms. Therefore, our abstraction of transport sub-protocol must establish a session key and ensures authentication of the server. A possible abstraction is based on an asymmetric encryption scheme in order to establish a fresh session key for a symmetric encryption scheme and authentication of the server. First, the client creates a session key, which is the symmetric session key. Then, the session key is encrypted with the server's public key and transmitted to the server. To decrypt, the server uses its private key to obtain the session key. Since in applied π-calculus it is difficult to model the sequential numbers, we use random nonce to prevent replay attacks in SSH connections as follows: For each message sent after SSH transport subprotocol, the sender concatenates its message with a nonce previously received from the receiver. Then, the receiver can check if the message is fresh or not. For sake of clarity, we do not include this use of random value in the below process.

The processes of SSH client and SSH server are given in Figure 7 and 8 respectively. The process of SSH client (resp. SSH server) is split into two subprocess, Clt-SSH-tran (resp. Ser-SSH-tran) modeling transport sub-protocol and Clt-SSH-Auth (resp. Ser-SSH-Auth) modeling SSH authentication sub-protocol. This separation provides some modularity because the communication between a writer and the CSP involves only SSH transport sub-protocol. In the following processes, we use some classical syntactic sugar of ProVerif syntax for readability. The processes P and Q that appear in Figure 8 represent the rest of the server process.

Clt-SSH-Trans(pkS) new SK; out(c,aenc(pkS,SK)); Clt-SSH-Auth(skClt) out(c,senc (SK,(sign(skClt,SK),pk(skClt)))). Note that, in our modeling the legitimate users are identified by their public keys sent as a parameter of the Proverif processes. For instance, in Ser-SSH-Auth(pkClt) sub-protocol in Figure 8, the signature sig is checked with the key pkClt representing a valid authenticator for a legitimate user.

Modeling RSN'12 Protocol

We describe the main process modeling the RSN'12 protocol. It is specified as the parallel composition of the processes modeling the roles of writers, readers, TA, KDC and CSP. The main process. It is specified in Figure 9. First, the fresh secret keys skTA, skKDC and skCSP, used respectively by the TA, the KDC, and the CSP for asymmetric encryption and signature are generated. Their corresponding public keys are then sent on public channels, i.e. they are made available to the adversary. Moreover, the fresh secret keys TSK, absASK and abeASK used in ABS and ABE schemes, are also generated and their corresponding public keys are published. The secret keys of writer skW and reader skR are made under replication to model an infinite number of writers and readers. The processes writer and reader are under replication, because one user may establish many sessions with the CSP. Since TA and KDC processes have the public key of the user as a parameter, they are instanced twice to interact with readers and writers. Moreover, in our modeling, the public keys of asymmetric encryption are used as identities of participants. The writer process. The writer process given in Figure 10 models the role of a writer. The secret keys KWTA, KWKDC and KWCL are the secret shared keys established by SSH transport protocol respectively with the TA, the KDC and the CSP. After the receipt of a token form the TA, the writer sends a request to the KDC to get attribute secret key for signing, this request is encoded by the pair (token,write). Afterwards, the writer encrypts his message msg and signs it using the attribute secret key absSkA. Finally, it sends the signed message sigMsg to the CSP. The reader process. The role of a reader is modeled by reader process given in Figure 11. At first, a reader behaves as a writer by requesting a token from the TA and an attribute secret key for decryption from the KDC. Next, it has access to the CSP, without secure communication SSH, to read a message stored on the cloud. Finally, he decrypts the message read from the CSP using his attribute secret key abeSkA, and behaves as RestOfReader with the received message. The TA process. The trusted authority process is given in Figure 12. After the establishment of the shared key for symmetric encryption KWTA by SSH transport protocol, and the authentication of the user by SSH authentication protocol which uses the process's parameter pkClt as authenticator, the TA generates a token and sends it to the user encrypted with KWTA. The KDC process. The KDC process is given in Figure 13. When receiving a request from a user, the KDC checks the correctness of the token using the public key pkClt of the user, which was authenticated during SSH authentication protocol. If the token is valid, it issues an attribute secret key for encryption or signing following the value of AccessMode, which has two possible values: "write" or "read". KDC(skKDC,TPK,absASK,abeASK,pkClt) Ser-SSH-Trans(skKDC);( * SSH connection to a user * ) Ser-SSH-Auth(pkClt); in(ch,encToken); let (token,AccessMode)=sdec(KWKDC,encToken) in if absTokenCheck(TPK,pkClt,token)= true then if AccessMode = write then event DelivKeySign(pkClt); out(ch,senc(KWKDC,absSka(absASK, absGetBase(token),att))); else if AccessMode = read then out(ch,senc(KWKDC,abeSka(abeASK,pkClt,att))) else 0. The CSP process. The CSP which is responsible for the storage of user data is modeled by the process in Figure 14. SSH connection without user authentication is established between writers. If the signature is valid with respect to the claim policy, the CSP stores the message that becomes immediately accessible by the readers. Since in reading mode, there is no secure communication between the reader and the CSP, in our modeling the CSP outputs the incoming messages from the writers on a public channel.

Security Analysis

We analyze the security properties of the protocol, namely the authentication and privacy of a writer, and the confidentiality of the data. All proofs of our propositions are not presented because they are directly implied by our ProVerif codes.

Confidentiality

It means that a user without valid access policy cannot decrypt the data stored on the cloud. In applied πcalculus this property can be expressed as a secrecy property: it should be impossible for an adversary, interacting with the protocol and without valid attribute secret key, to learn a message which is encrypted and stored on the cloud. Definition 5.1: Given an access policy AP , a cloud storage protocol ensures confidentiality if a secret message stored on the cloud by an honest writer is not deducible by an attacker without attribute secret key satisfying AP .

Proving secrecy property is expressed by the reachability notion. We request ProVerif to check that a private message, encrypted using a public access policy AP , cannot be deduced by the attacker. The valid attribute secret key of AP abeSka(ASK,uid,att), which has been generated by the KDC, is not sent on a public channel to be not available to the adversary. ProVerif proves this property in less one minute.

Proposition 1: RSN'12 protocol ensures the confidentiality property.

This result confirms the fact that SSH communication between the CSP and a reader is useless for confidentiality, since our modeling does not use it and ProVerif is able to prove the secrecy of the message.

Writer Authentication

A user can only write in the cloud if he has the attribute validating the claim policy. Moreover, an invalid user cannot receive attribute from a KDC, if does not have the token from the TA. Authentication property can be captured as a correspondence assertion. To define the authentication of a writer, we annotate the protocol by the following events:

• AcceptSign: This event is placed inside the CSP's process and emitted if the signature is valid, i.e. absCheckSign returns true.

• DelivKeySign(pkClt): This event is placed inside the KDC's process and emitted when the KDC issues an attribute secret key for signing to a user with identity pkClt.

• DelivToken(pkClt): This event is placed inside the TA's process and emitted when the TA delivers a token to a user with identity pkClt.

Definition 5.2: A cloud storage protocol ensures the authentication of a writer with identity Id if for every execution trace of the protocol each occurrence of the event AcceptSign is preceded by an occurrence of DelivKeySign(Id) which is preceded by an occurrence of DelivT oken(Id).

This property can be expressed in ProVerif in terms of nested correspondence [START_REF] Blanchet | Automatic verification of correspondences for security protocols[END_REF] which allows us to order events. ProVerif can automatically prove the corresponding nested correspondence in less one second: event(acceptSign) ⇒ (event(DelivKeySign(pkwriter)) ⇒ event(DelivT oken(pkwriter)))

Proposition 2: RSN'12 protocol satisfies the authentication of a writer.

Writer Privacy

In the context of cloud storage, writer privacy is expressed by two properties; anonymity and unlinkability. The anonymity of a writer's identity is ensured if it is not possible for anyone, even the CSP, to learn the writer's identity of a stored message. Unlinkability means that no one can link the messages stored on the cloud, more precisely no one is able to decide if two messages were stored by the same writer, or not. Anonymity:. A cloud storage system ensures anonymity if it keeps the writer's identity secret from everyone. Hence, anonymity can be formalized as a secrecy property: no one can deduce the identity of a writer who stores a message on the cloud. Since the identities of the writers are known values, anonymity is captured by the concept of strong secrecy. Strong secrecy means that the adversary cannot distinguish two instances of the same protocol with two different values of the secret. For the precise definition, we refer the reader to [START_REF] Blanchet | Automatic proof of strong secrecy for security protocols[END_REF]. In ProVerif, strong secrecy is expressed by diffequivalence defined between processes that share the same structure and differ only in the choice of terms representing the secret values [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF]. author Definition 5.3: A cloud storage protocol ensures anonymity of a writer's identity if for any two writers with identities IdW 1 , IdW 2 and for any message msg, an adversary cannot distinguish whether msg comes from IdW 1 or IdW 2 .

We request to ProVerif to check if

C[W riter(IdW 1 , msg)] ≈ C[W riter(IdW 2 , msg)].
with C[ ] is an evaluation context modeling the whole cloud storage protocol as described in main process with a hole for a writer process, and the process W riter(IdW, msg) models a writer with identity IdW storing a message msg on the cloud. ProVerif succeeds to prove this request in 3 seconds.

Proposition 3: RSN'12 protocol preserves the anonymity of writer's identity. Unlinkability:. Informally, in cloud storage context, unlinkability holds when the different stored messages of the same writer cannot be linked by an attacker even a dishonest user (writer or reader). Thus, unlinkability can be viewed as the secrecy of link between writer and its messages stored on the cloud. The definition of unlinkability is similar to the definition of voter privacy in e-voting protocol [START_REF] Kremer | Analysis of an electronic voting protocol in the applied pi calculus[END_REF] in the sense that we must consider at least two honest writers. To understand this assumption, consider the case where all the writers are dishonest except one, as the stored messages on the cloud are published by the CSP, the dishonest writers can collude and determine the message of the honest writer.

Definition 5.4: A cloud storage protocol ensures unlinkability if for any two writers with identities IdW 1 , IdW 2 and for any two messages msg1 and msg2, an adversary cannot distinguish the situation in which IdW 1 stores msg1 and IdW 2 stores msg2 from the situation in which IdW 1 stores msg2 and IdW 2 stores msg1.

In applied π-calculus this definition can be formalized as the following equivalence:

C[W riter(IdW 1 , msg1)|W riter(IdW 2 , msg2)] ≈ C[W riter(IdW 1 , msg2)|W riter(IdW 2 , msg1)] ,
where C[ ] is an evaluation context modeling the whole protocol with a hole for two writers. In ProVerif, the above pair of processes can be expressed as single biprocess as follows:

C[W riter(IdW 1 , choice[msg 1 , msg 2 ])] | C[W riter(IdW 2 , choice[msg 2 , msg 1 ])] .
ProVerif finds an attack, in which a man-inthe-middle attacker selectively delays or delete some messages sent to the CSP by one writer until he can link a message to somebody.

Proposition 4: RSN'12 protocol does not ensure unlinkability property.

For this attack, we consider an attacker that is a semihonest reader with valid attribute secret keys, who wants link the messages to a writer. In a real cloud storage environment, to achieve the attack, an attacker performs the following steps:

• Access to the CSP and memorize all the files stored in the cloud.

• Listen to the network and wait for a message sent to the CSP.

• When a new message M SG is sent, he identifies its sender IdW and blocks all the messages sent to CSP after the message M SG. He now has just to wait until M SG becomes available on the CSP, i.e. the CSP appends M SG to the previous files.

• Then, he can access the files and then learn M SG by comparing the current contents of files with the previous contents. Thus, he concludes that M SG was sent by a writer with identity IdW and can link a file to somebody.

We illustrate this attack in Figure 15.

Fixed protocol:. The previously discovered attack against unlinkability is based on the fact that an attacker can instantaneously access to the CSP to learn a message just after it was sent by a writer. To fix this problem, a solution is that the CSP simultaneously publishes at least two incoming messages from different persons. However, the messages are accessible from a file, so if the messages are written on the file in a deterministic order, for instance following the arriving time of the messages, the adversary can link a message with its writer by inspecting the order of the sent messages to the CSP on the network. Therefore, the CSP must write the incoming messages on the files in a non-deterministic way. The new role of the CSP is given in the Figure 16 and illustrated in Figure 17.

The synchronization command sync 1 in the last line of the above process is introduced to synchronize CSP process. This means that the CSP process waits until the two sync 1 are reached before publishing the received messages. Therefore, the outputs out(ch, msg1) and out(ch, msg2) of the two received messages are executed in parallel. This parallel execution captures the non-deterministic behavior of the writing of the messages on the file, because the semantic of a parallel composition P | Q allows simultaneously and independently execution of P and Q. Moreover, in this case synchronization helps to automatically prove diff-equivalence by ProVerif, and hence the observational equivalence of applied π-calculus, because it allows swapping data between processes at the synchronization points. In fact, the diff-equivalence is stronger than observational equivalence. In particular,

Step 1 CSP Attacker reads and memorizes all stored files.

Step 2 CSP Alice writes a new file.

Attacker listens the network and waits for a message sent to CSP.

Step 3

Attacker compares the current files with the previous files.

Previous CSP

Current CSP Then, the attacker deduces which file was sent by Alice. when proving equivalence between processes that contain several parallel components, e.g., P | Q and P | Q , diff-equivalence requires that P is equivalent to P and Q is equivalent to Q . This constraint can be relaxed by swapping data between parallel processes at synchronization points. For more details, we refer the reader to [START_REF] Blanchet | Automated reasoning for equivalences in the applied pi calculus with barriers[END_REF]. Fortunately, ProVerif succeeds to prove observational equivalence with the new role of the CSP in 28 seconds, and therefore we can conclude the security of the fixed protocol.

Conclusion

In this paper, we revisit the security of the protocol of Ruj et al. [START_REF] Ruj | Privacy preserving access control with authentication for securing data in clouds[END_REF]. We propose a model for ABE and ABS in the well know applied π-calculus framework. We use ProVerif to prove automatically claimed security properties by the authors in the original paper. ProVerif helps us to discover a flaw in this protocol for the unlinkability property. We then give a correction and prove the security of the modified version with ProVerif.

The next step is to formalize and verify other properties such as accountability. A system is accountable when it is able to detect a malicious action and generates an undeniable evidence to identify the originator. It could be possible to extend RSN'12 protocol by a revocation technique and then analyze the resistance against the replay attacks. Moreover, we will use our framework to model and analyze more

Figure 1 :

 1 Figure 1: RSN'12 protocol.

Figure 4 :

 4 Figure4: Grammar of extended processes.

Figure 7 :

 7 Figure 7: SSH client.

Figure 8 :

 8 Figure 8: SSH server.

Figure 9 :

 9 Figure 9: Main process.

  Writer(skW,TPK,absAPK,abeAPK,pkTA,pkKDC,pkCSP) Clt-SSH-Trans(pkTA); ( * SSH connection to TA * ) Clt-SSH-Auth(skW); in(ch,encToken); let token = sdec(KWTA,encToken) in Clt-SSH-Trans(pkKDC);( * SSH connection to KDC * ) Clt-SSH-Auth(skW); out(ch,senc(KWKDC,(token,write))) in(ch,encAbsSkA); let absSkA = sdec(KWKDC,encAbsSkA) in let abeEncMsg = abeEnc(abeAPK,AccessP,msg) in Clt-SSH-Trans(pkCSP); ( * SSH connection to CSP * ) let sigMsg=absSign(TPK,absAPK,token,absSkA, abeEncMsg,ClaimP) in out(ch,senc(KWCSP,(abeEncMsg,sigMsg))).

Figure 10 :

 10 Figure 10: Writer process.

  Reader(skR,pkTA,pkKDC) Clt-SSH-Trans(pkTA); ( * SSH connection to TA * ) Clt-SSH-Auth(skR); in(ch,encToken); let token = sdec(KWTA,encToken) in Clt-SSH-Trans(pkKDC); ( * SSH connection to KDC * ) Clt-SSH-Auth(skR); out(ch,senc(KWKDC,(token,read))); in(ch,encAbeSkA); let abeSkA = sdec(KWKDC,encAbsSkA) in in( c,encMsg); ( * Reception of data from the CSP * ) let msg = abeDec(encMsg,abeSkA) in RestOfReader.

Figure 11 :

 11 Figure 11: Reader process.

Figure 12 :

 12 Figure 12: Trusted Authority process.

Figure 13 :

 13 Figure 13: Key Distribution Center process.

  CSP(skCSP,TPK,absAPK) Ser-SSH-Trans(skCSP); ( * SSH with a writer * ) in(ch,encMsg); let (msg,sigMsg) = sdec(KWCSP,encMsg) in if absSignCheck(TPK,absAPK,msg,ClaimP,sigMsg)= true then event AcceptSign; out(ch,msg).

Figure 14 :

 14 Figure 14: Cloud Server Porvider process.

Figure 15 :

 15 Figure 15: Attack on the unlinkability.

FixedCSPFigure 16 :

 16 Figure 16: Fixed Cloud Server Porvider process.

Proposition 5 :

 5 The revisited RSN'12 protocol ensures unlinkability property.

Then he spent six months in the cryptography department

checksign(pk(sk),sign(sk,msg),msg) = true Concatenation: Algebraic data structures such as tuples of messages appear in many protocols and are supported by ProVerif. A tuple of length n > 1 is defined as (M 1 , . . . , M n ) where M 1 , . . . , M n are terms. Given a tuple, it is possible to recover the i-th element.

ABS equational theory:. ABS scheme uses separate keys, constructed from the public parameters which are set up by TA. The equational theory modeling ABS scheme consists of five equations given in Figure 5.

The function absPK is used for deriving the public key of the TA from its private key. The term absToken(TSK,base,uid) denotes the token delivered by a TA with secret key TSK, to a user with identity uid. Any entity can check the validity of the token using absTokenCheck algorithm, and the public key absPk(TSK) as described by Equation (ABS-1). The algorithm extraction of the random value base from a token is modeled by Equation (ABS-2). A KDC extracts base value to embedded it in the attribute secret keys of the users. This allows us to link the attribute secret keys to one user and consequently, to avoid the collusion of the users. An attribute secret key corresponding to attribute att is denoted by absSka(ASK,base,att) with ASK is the private key of the issuing KDC. It can be checked for correctness using absKeyCheck algorithm as described in the equation (ABS-3). Since it is possible to have many TA, and a KDC would issue attribute keys to a user for all the TA he wishes to work with, the public key of a KDC, denoted by absPkA(absPk(TSK),ASK), is associated with its secret key ASK and the public absPk(ASK) of the TA with which the user works. The evaluation of the claim policy, which expressed by a Boolean function, is modeled by Equation (ABS-4). Given a Boolean function F , the term absEval(F, x 1 . . . , x n ) is equivalent to F (x 1 , . . . , x n ). Hence, when considering more than one attribute, absEval will be used to represent the truth table of the Boolean function. The functions absSign and absSignCheck are employed to represent respectively the signature and verification procedures. As described in Equation (ABS-5), absSignCheck returns the truth value of claim policy evaluation, which is true only if the message was signed using a valid attribute secret key.

ABE equational theory:. As ABS scheme, ABE scheme uses separate keys, but does not require a central authority. The equational theory of ABE scheme is given in Figure 6. author

Step 1

CSP

Alice sends a first message.

Attacker knows that Alice sends a message.

The CSP waits for an other writer sends a message before store any Alice's message.

Step 2

CSP

Bob sends an other message.

Attacker knows that Bob sends a message.

Step 3

The CSP writes the incoming messages on the files in nondeterministic way.

Previous CSP Current CSP Then, the attacker cannot link messages and writers. protocols using ABE and ABS (Yang andJia, 2012, 2014;[START_REF] Dahshan | Framework for securing data in cloud storage services[END_REF][START_REF] Belguith | Pabac: a privacy preserving attribute based framework for fine grained access control in clouds[END_REF], in order to discover flaws or formally prove the security of these protocols.


Rob Swart

Lenny Bernstein

Minh Ha-Duong

Arthur Petersen

Agreeing to disagree: Uncertainty management in assessing climate change, impacts and responses by the IPCC

Lexical analysis of IPCC Third Assessment Reports dealing with risk and uncertainty

Electronic supplement to Swart et al. (2006) Left, number of occurences in TAR working group. In order to correct the size bias (reports from WG I and II were about the same size, but WG III report was 34% shorter), the right side of these tables show frequencies (% text coverage times 10000, abusively rounded).

Commment : Nothing surprising here. After "Climate change", the most frequent words used in the IPCC report vary across working groups. WG I uses "model", "global" and "temperature". In WG II we read "impact" "water" and "global" . The third working group writes about "emissions", "energy" and "cost". The word "model" is frequent also in WG II and III. Comment : There is no need for statistical tests to see that each working group uses a different strategy to write about risk and uncertainty. WG I almost banished the word "risk" in favor of words in the "uncertain" and "possible" family. In contrast, WG II uses "risk" a lot. "decision" takes first place in WG III. "surpris" seems under-used compared to the real degree of concern for abrupt climate change.

Risk & uncertainty vocabulary

Vocabulary from the guidelines

Data and methods

The full TAR text was taken from the IPCC TAR CD-ROM, also available online Methods are formally defined in the attached script. Text was converted from HTML to 7-bit clean using the html2text script, and cat and sed standard Unix tools. Content was analysed using the « locate pattern » functions in UNITEX 1.2, an open-source corpus processing system based on automata-oriented technology.

Documents joints

  working paper on Uncertainty management in assessing climate change, impacts and responses : the evolution from the first to the fourth IPCC Assessment

			Mis en ligne par Minh Ha Duong
				18 juillet 2006
			Top words (>4000 uses)
	How to read : In the IPCC Third Assessment Report, Working Group III volume, the word
	"emission" is used 3967 times.
	WG I WG II WG III Total	WG I WG II WG III
	5501 11269 2586 19356 <change>	3040 5180 1890
	5947 9427 2159 17533 <climate>	3290 4330 1580
	5894 1890 1322 9106 <model>	3260 869 970
	669 4307 952	5928 <impact>	370 1980 700
	2400 2273 1151 5824 <global>	1330 1040 840
	1265 531 3967 5763 <emission>	700 240 2900
	1113 3442 169	4724 <water>	610 1580 120
	10	813 3546 4369 <cost>	10	370 2590
	228 498 3588 4314 <energy>	130 230 2620
	2305 1912 89	4306 <temperature> 1270 880 60

  This section refers toMoss and Schneider (2000) Uncertainties in the IPCC TAR : Recommendations to lead authors figures 3 and 4. The usual bias against negative results is clearly visible. WG II used vocabulary from the guidelines much more than the other two working groups. Note that these figures do NOT include text from the Technical Summaries.

	Numbers represent upper bounds, since I did not check if in context they have been used referring
	to the guidelines.
	WG I WG II WG III Total III. Guidelines vocabulary	WG I WG II WG III
	8	240 4	252 <high><confidence>	10	330 10
	0	161 1	162 <medium><confidence>	0	220 0
	3	43	6	52	<low><confidence>	0	60	10
	11	444 11	466 Total for confidence levels
	WG I WG II WG III Total		WG I WG II WG III
	9	22	12	43	<well><establish>	10	30	30
	0	27	2	29	<establish><but>	0	40	0
	10	18	8	36	<speculative>	10	10	10
	0	18	1	19	<compete><explanation>	0	20	0
	19	85	23	127 Total for qualitative uncertainty
	Comments :

of 3 20.07.2006 16:31