Tigran Avanesov
email: tigran.avanesov@uni.lucontraintesde

Yannick Chevalier
email: ychevali@irit.fr

Michaël Rusinowitch

Mathieu Turuani
email: turuani@inria.fr

Intruder deducibility constraints with negation. Decidability and application to secured service compositions. *

Keywords: Web services, orchestration, security policy, separation of duty, deducibility constraints, cryptographic protocols, formal methods, tool Services Web, orchestration, politique de sécurité, séparation des tâches, contraintes de deducibilité, protocoles de sécurité, méthodes formelles, util

The problem of finding a mediator to compose secured services has been reduced in our former work to the problem of solving deducibility constraints similar to those employed for cryptographic protocol analysis. We extend in this paper the mediator synthesis procedure by a construction for expressing that some data is not accessible to the mediator. Then we give a decision procedure for verifying that a mediator satisfying this non-disclosure policy can be effectively synthesized. This procedure has been implemented in CL-AtSe, our protocol analysis tool. The procedure extends constraint solving for cryptographic protocol analysis in a significative way as it is able to handle negative deducibility constraints without restriction. In particular it applies to all subterm convergent theories and therefore covers several interesting theories in formal security analysis including encryption, hashing, signature and pairing.

Introduction

Context

Trust and security management in distributed frameworks is known to be a non-trivial critical issue. It is particularly challenging in Service Oriented Architecture where services can be discovered and composed in a dynamic way. Implemented solutions should meet the seemingly antinomic goals of openness and flexibility on one hand and compliance with data privacy and other regulations on the other hand. We have demonstrated in previous works [START_REF] Chevalier | Automatic composition of services with security policies[END_REF][START_REF] Chevalier | Orchestration under security constraints[END_REF][START_REF] Avanesov | Web services verification and prudent implementation[END_REF] that functional agility can be achieved for services with a message-level security policy by providing an automated service synthesis algorithm. It resolves a system of deducibility constraints by synthesizing a mediator that may adapt, compose and analyze messages exchanged between client services and having the functionalities specified by a goal service. It is complete as long as the security policies only apply to the participants in the orchestration and not on the synthesized service nor on who is able to participate. However security policies often include such non-deducibility constraints on the mediator. For instance an organisation may not be trusted to efficiently protect the customer's data against attackers even though it is well-meaning. In this case a client would require that the mediator synthesized to interact with this organization must not have direct access to her private data, which is an effective protection even in case of total compromise. Also it is not possible to specify that the mediator enforces e.g. dynamic separation of duty, i.e., restrictions on the possible participants based on the messages exchanged.

Since checking whether a solution computed by our previous algorithm satisfies the non-deducibility constraints is not complete, we propose in this paper to solve during the automated synthesis of the mediator both deducibility and non-deducibility constraints. The former are employed to specify a mediator that satisfies the functional requirements and the security policy on the messages exchanged by the participants whereas the latter are employed to enforce a security policy on the mediator and the participants to the orchestration.

Original contribution. We have previously proposed decision procedures [START_REF] Chevalier | Automatic composition of services with security policies[END_REF][START_REF] Chevalier | Orchestration under security constraints[END_REF][START_REF] Avanesov | Web services verification and prudent implementation[END_REF] for generating a mediator from a high-level specification with deducibility constraints of a goal service. In this paper we extend the formalism to include non-deducibility constraints in the specification of the mediator and provide a decision procedure synthesizing a mediator for the resulting constraint systems.

Related works. In order to understand and anticipate potential flaws in complex composition scenarios, several approaches have been proposed for the formal specification and analysis of secure services [START_REF] Armando | The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures[END_REF][START_REF] Costa | Secure service orchestration in open networks[END_REF]. Among the works dedicated to trust in multi-agent systems, the models closest to ours are [START_REF] Herzig | A logic of trust and reputation[END_REF][START_REF] Lorini | Trust and norms in the context of computer security: A logical formalization[END_REF] in which one can express that an agent trusts another agent in doing or forbearing of doing an action that leads to some goal. To our knowledge no work has previously considered the automatic orchestration of security services with policies altogether as ours. However there are some interesting related attempts to analyze security protocols and trust management [START_REF] Martinelli | Towards an integrated formal analysis for security and trust[END_REF][START_REF] Frau | Integrated specification and verification of security protocols and policies[END_REF]. In [START_REF] Martinelli | Towards an integrated formal analysis for security and trust[END_REF] the author uniformly models security protocols and access control based on trust management. The work introduces an elegant approach to model automated trust negotiation. We also consider an integrated framework for protocols and policies but in our case i) policies can be explicitly negative such as non-disclosure policies and separation-of-duty ii) we propose a decision procedure for the related trust negotiation problem iii) we do not consider indistinguishability properties. In [START_REF] Frau | Integrated specification and verification of security protocols and policies[END_REF] security protocols are combined with authorization logics that can be expressed with acyclic Horn clauses. The authors encode the derivation of authorization predicates (for a service) as subprotocols and can reuse in that way the constraint solving algorithm from [START_REF] Millen | Constraint solving for boundedprocess cryptographic protocol analysis[END_REF] to obtain a decision procedure. In our case we consider more general intruder theories (subterm convergent ones) but focus on negation. We conjecture that our approach applies to their authorization policies too.

Our decision procedure for general (negative and positive) constraints extend [START_REF] Corin | A logic for constraint-based security protocol analysis[END_REF] where negative constraints are limited to have ground terms in right-hand sides, and the deduction system is Dolev-Yao system [START_REF] Dolev | On the security of public key protocols[END_REF], a special instance of the subterm deduction systems we consider here. In [START_REF] Kähler | Infinite state amc-model checking for cryptographic protocols[END_REF] the authors study a class of contract signing protocols where some very specific Dolev-Yao negative constraints are implicitly handled.

Finally one should note that the non deducibility constraints we consider tell that some data cannot be disclosed globally but they cannot express finergrained privacy or information leakage notions relying on probability such as for instance differential privacy.

Paper organization. In Subsection 1.2 we introduce a motivating banking application and sketch our approach to obtain a mediator service. To our knowledge this application is out of the scope of alternative automatic methods. In Section 2 we present our formal setting. A deduction system (Subsection 2.2) describes the abilities of the mediator to process the messages. The mediator synthesis problem is reduced to the resolution of constraints that are defined in Subsection 2. In Section 3 we recall the class of subterm deduction systems and their properties. These systems have nice properties that allow us to decide in Section 4 the satisfiability of deducibility constraints even with negation. Finally we conclude in Section 5.

Synthesis of a Loan Origination Process (LOP)

We illustrate how negative constraints are needed to express elaborated policies such as Separation of Duty by a classical loan origination process example. Our goal is to synthesize a mediator that selects two bank clerks satisfying the Separation of Duty policy to manage the client request. Such a problem is solved automatically by the decision procedure proved in the following sections. Let us walk through the specification of the different parts of the orchestration problem.

Inria

Formal setting. Data are represented by first-order terms defined on a signature that comprises binary symbols for symmetric and assymetric encryptions (resp. {|_|} _ , {_} _ ), signature ({_} sig _ ), and pairing (pair). Given a public key k we write inv (k) its associated private key. For example {a} sig inv(k) is the signature of a by the owner of public key k. For readability we write a.b.c a term pair (a, pair (b, c)). The binary symbol rel expresses that two agents are related and is used for defining a Separation of Duty policy. A unary symbol g is employed to designate participants identity in the "relatives" database.

Client and clerks. The client and the clerks are specified by services with a security policy, specifying the cryptographic protections and the data and security tokens, and a business logic that specify the sequence in which the operations may be invoked. These are compiled into a sequence of protected messages each service is willing to follow during the orchestration (Fig. 1 and2).

Client C wants to ask for a loan from a service P , but for this he needs to get an approval from two banking clerks. He declares his intention by sending to mediator M a signed by him message containing service name P and the identity of the client g(C). The mediator should send back the names of two clerks A and B who will evaluate his request. The client then sends to each clerk a request containing amount Amnt, his name C and a fresh key N k which should be used to encrypt decisions. Each request is encrypted with a public key of the corresponding clerk (pk(A) or pk(B)). Then the mediator must furnish the decisions (R a and R b ) of two clerks each encrypted with the proposed key N k and also their signatures. Finally, the client uses these tokens to ask his loan from P , where pk(P ) is a public key of P .

Clerk A receives a request to participate in a LOP which is conducted by mediator M . If he accepts, he returns his identity and public key. Then Clerk receives the client's request for a loan to evaluate: amount Amnt, client's name C and a temporary key K for encrypting his decision. The last is sent back together with a signature certifying the authenticity of this decision on the given request.

The client's non-disclosure policy is given in Fig. 2 and is self-explanatory. Let us explain the services' non-disclosure policy. The Clerk's decision (its last message) should be unforgeable, thus, it should not be known by the Mediator before it was sent by the Clerk (first non-disclosure constraint of Fig. 1). The role clerk played by A can be used by the mediator only if the constraint g(A) is satisfied, showing that A is not a relative with any other actor of the protocol, as client and the other clerk (second non-disclosure constraint of Fig. 1).

Goal service. In contrast with the other services and clients, the goal service is only described in terms of possible operations and available initial data. Initial data. Beside his private/public keys and the public keys of potential partners (e.g. pk (P )) the goal service has access to a relational database rel(g(a), g(c)), rel(g(b), g(c)), . . . for storing known existing relations between agents to be checked against conflict of interests.

Clerk's (A) communications:

1 * ⇒ A : request.M A ⇒ M : g(A). pk (A) M ⇒ A : {Amnt.C.K} pk(A) A ⇒ M : m 1 (A, Resp A , K, C, Amnt)
Non-disclosure constraints:

1. M cannot deduce the fourth message before it is sent by A.

2. M cannot deduce g(A) before the second message is sent by A.

M ⇒ C : A.B C ⇒ M : m 2 (A, Amnt).m 2 (B, Amnt) M ⇒ C : m 3 (A, R a ).m 3 (B, R b ) C ⇒ P : m 4 (pk (P ) , A, B, R a , R b )
Non-disclosure constraints:

1. M cannot deduce the amount Amnt. Deduction rules. The access to the database as well as the possible operations on messages are modeled by a set of deduction rules (formally defined later). We anticipate on the rest of this paper, and present the rules specific to this case study grouped into composition and decomposition rules in Fig. 3.

M cannot deduce

A's decision R a . 3. M cannot deduce B's decision R b .
Mediator synthesis problem. In order to communicate with the services (here the client, the clerks and the service P ), a mediator has to satisfy a sequence of constraints expressing that (i) each message m expected by a service (denoted ?m) can be deduced from all the previously sent messages m (denoted !m ) and the initial knowledge and (ii) each message w that should not be known or disclosed (denoted w and called negative constraint) is not deducible.

The orchestration problem consists in finding a satisfying interleaving of the constraints imposed by each service. For instance, clerk's and client's constraints Inria extracted from Fig. 1 and Fig. 2 are:

             Client(C) ∆ = ! M {g(C).loan.P } sig inv(K C ) ? M A.B ! M m 2 (A, Amnt).m 2 (B, Amnt) ? M m 3 (A, R a ).m 3 (B, R b ) M Amnt M R A M R B ! P m 4 (pk (P ) , A, B, R a , R b ) Clerk(A) ∆ = ?request.M M g(A) ! M g(A). pk (A) ? M {Amnt.C.K} pk(A) M m 1 (A, Resp A , K, C, Amnt) ! M m 1 (A, Resp A , K, C, Amnt)
If it exists our procedure outputs a solution which can be translated automatically into a mediator. Note, for example, that without the negative constraint g(A) a synthesized mediator might accept any clerk identity and that could violate the Separation of Duty policy.

Derivations and constraint systems

In our setting messages are terms generated or obtained according to some elementary rules called deduction rules. A derivation is a sequence of deduction rules applied by a mediator to build new messages. The goal of the synthesis is specified by a constraint system, i.e. a sequence of terms labelled by symbols !,? or , respectively sent, received, or unknown at some step of the process.

Terms and substitutions

Let X be a set of variables, F be a set of function symbols and C a set of constants. The set of terms T is the minimal set containing X , C and if t 1 , . . . , t k ∈ T then f (t 1 , . . . , t k ) ∈ T for any f ∈ F with arity k. The set of subterms of a term t is denoted Sub(t) and is the minimal set containing t such that f (t 1 , . . . , t n ) ∈ Sub(t) implies t 1 , . . . , t n ∈ Sub(t) for f ∈ F. We denote Vars (t) the set X ∩ Sub(t). A term t is ground is Vars (t) = ∅. We denote T g the set of ground terms.

A substitution σ is an idempotent mapping from X to T . It is ground if it is a mapping from X to T g . The application of a substitution σ on a term t is denoted tσ and is equal to the term t where all variables x have been replaced by the term xσ. We say that a substitution σ is injective on a set of terms T , iff for all p, q ∈ T pσ = qσ implies p = q. The domain of σ (denoted by dom (σ)) is set:

{x ∈ X : xσ = x}. The image of σ is img (σ) = {xσ : x ∈ dom (σ)}.
Given two substitutions σ, δ, the substitution σδ has for domain dom (σ) ∪ dom (δ) and is defined by xσδ = (xσ)δ. If dom (σ) ∩ dom (δ) = ∅ we write σ ∪ δ instead of σδ.

A unification system U is a finite set of equations {p i = ? q i } 1≤i≤n where p i , q i ∈ T . A substitution σ is an unifier of U or equivalently satisfies U iff for 1 We have employed the following abbreviations for messages:

                 m 1 (A, Resp, K, Ct, S) = {h(A.S.Ct.Resp)} sig inv(pk(A)) .{|Resp|} K m 2 (A, S) = {S.C.N k } pk(A) m 3 (A, R) = m 1 (A, R, N k , C, Amnt) m 4 (K 0 , A, B, R 1 , R 2 ) = {Amnt.C.A.R 1 .B.R 2 } K 0 .m 3 (A, R 1 ).m 3 (B, R 2 )

RR n°8017

all i = 1, . . . , n, p i σ = q i σ. Any satisfiable unification system U admits a most general unifier mgu (U ), unique modulo variable renaming, and such that for any unifier σ of U there exists a substitution τ such that σ = mgu (U ) τ . Wlog we assume in the rest of this paper that Vars (img (mgu (U ))) ⊆ Vars (U ), i.e., the most general unifier does not introduce new variables.

A sequence s is indexed by [1, . . . , n] with n ∈ N. We write |s| the length of s, ∅ the empty sequence, s[i] the ith element of s, s[m : n] the sequence s[m], . . . , s[n] and s, s the concatenation of two sequences s and s . We write e ∈ s and E ⊆ s for, respectively, ∃i : s[i] = e and ∀e ∈ E, e ∈ s.

Deduction systems

The new values created by the mediator are constants in a subset C med of C. We assume that both C med and C \ C med are infinite. Given l 1 , . . . , l n , r ∈ T , the notation l 1 , . . . , l n → r denotes a deduction rule if Var(r)

⊆ n i=1 Var(l i ).
A deduction is a ground instance of a deduction rule. A deduction system is a set of deduction rules that contains a finite set of deduction rules in addition to all nonce creation rules → n (one for every n ∈ C med ) and all reception rules ?t (one for every t ∈ T ). All rules but the reception rules are called standard rules. The deduction system describes the abilities of the mediator to process the messages. In the rest of this section we fix an arbitrary deduction system D. We denote by l * → r any rule and l → r any standard rule.

Derivations and localizations

A derivation is a sequence of deductions, including receptions of messages from available services, performed by the mediator. Given a sequence of deductions E = (l i * → r i ) i=1,...,m we denote R E (i) the set {r j : j ≤ i}.

Definition 2.1 (Derivation). A sequence of deductions D = (l i * → r i ) i=1,...,m is a derivation if for any i ∈ {1, . . . , m}, l i ⊆ R D (i -1).
Given a derivation D we define Next D (i) = min({|D| + 1} ∪ {j : j > i and D[j] =?t j }). The explicit knowledge of the mediator is the set of terms it has already deduced, and its implicit knowledge is the set of terms it can deduce. If the former is K we denote the latter Der(K). A derivation D is a proof of s ∈ Der(K) if ?r ∈ D implies r ∈ K, and D[|D|] = l * → t. Thus, we have:

Der(K) = {t : ∃D derivation s.t. ?r ∈ D implies r ∈ K, and D[|D|] = l → t}

Constraint systems

Definition 2.2 (Constraint system). A constraint system S is a sequence of constraints where each constraint has one of three forms (where t is a term):

1. ?t, denoting a message reception by an available service or a client, 2. !t, denoting a message emission by an available service or a client, and that satisfies the following properties for any 1 ≤ i ≤ |S|:

Inria

Origination: if S[i] =!t i then Vars (t i ) ⊆ j<i Vars ({t j : S[j] =?t j }); Determination: if S[i] = t i then Vars (t i ) ⊆ j Vars ({t j : S[j] =?t j }).
Origination means that every unknown in a service's state originates from previous input by the mediator. Determination means that negative constraints are on messages determined by a service's state at the end of its execution.

In the rest of this paper S (and decorations thereof) denotes a constraint system. An index i is a send (resp. a receive) index if S[i] =!t (resp. S[i] =?t) for some term t. If i 1 , . . . , i k is the sequence of all send (resp. receive) indices in S we denote Out(S) (resp. In(S)) the sequence S[i 1 ], . . . , S[i k ]. We note that the origination and determination properties imply Var(S) = Var(In(S)). Given 1 ≤ i ≤ |S| we denote prev S (i) to be max({0} ∪ {j : j ≤ i and S[j] =!t j }). Definition 2.3 (Solution of a constraint system). A ground substitution σ is a solution of S, and we denote σ |= S, if dom (σ) = Var(S) and 1. if S[i] =?t then tσ ∈ Der({t j σ : j ≤ prev S (i) and S[j] =!t j })

if S[i] = t then tσ /

∈ Der({t j σ : j ≤ prev S (i) and S[j] =!t j }) Definition 2.4 (Compliant derivations). Let σ be a ground substitution with dom (σ) = Var(S). A derivation D is (S, σ)-compliant if there exists a strictly increasing bijective mapping α from the send indices of S to the set {j :

D[j] =?r} such that S[i] =!t implies D[α(i)] =?tσ.
An example of (S, σ)-compliant derivation is shown in Figure 4. Since a sequence of receptions is a derivation, we note that for every ground substitution σ with dom (σ) = Var(In(S)) there exists at least one compliant derivation D. In Figure 4, if σ is a solution of S and, for example, t 1 σ = r 2 , t 2 σ / ∈ Der(∅), t 4 σ = r 4 , t 6 σ / ∈ Der({r 3 , r 6 }) and t 7 σ = r 8 then D is a proof of σ |= S. Let us prove that if σ |= S then there is a proof D, σ, α S. Definition 2.6 (Maximal derivation). Let T be a finite set of terms and σ be a ground substitution with dom (σ) = Var(T ).

A derivation D is (T, σ)-maximal iff for every t ∈ Sub(T ), tσ ∈ Der(R D (i)) implies tσ ∈ R D (Next D (i) -1).
First we prove that maximal derivations are natural proof candidates of σ |= S.

Lemma 1. Let σ be a ground substitution with dom (σ) = Var(S) and D be a (S, σ)-compliant (Sub(S), σ)-maximal derivation. Then σ |= S iff for all i

• if S[i] =?t then there exists j < Next D (α(prev S (i))) : D[j] = l * → tσ and • if S[i] = t then for all j < Next D (α(prev S (i))) : D[j] = l * → tσ.
In the next lemma we show that any (T, σ)-maximal derivation D may be extended into a (T , σ )-maximal derivation for an arbitrary extension T , σ of T, σ by adding into D only standard deductions. Lemma 2. Let σ be a ground substitution with dom (σ) = Var(S). Let T 1 , T 2 be two sets of terms such that T 1 ⊆ T 2 , and σ 1 , σ 2 be two substitutions such that dom (σ 1 ) = Var(T 1 ) and dom (σ 2 ) = Var(T 2 ) \ Var(T 1 ). If D is a (T 1 , σ 1 )maximal (S, σ)-compliant derivation in which no term is deduced twice by a standard rule, then there exists a (T 2 , σ 1 ∪σ 2 )-maximal (S, σ)-compliant derivation D in which no term is deduced twice by a standard rule such that every deduction whose right-hand side is in Sub(T 1 )σ 1 occurs in D iff it occurs in D.

Proof. Let i 1 , . . . , i k be the indices of the non-standard rules in D, let D[i j ] = ?t ij , and let for 0

≤ j ≤ k D j = D[i j +1 : i j+1 -1] with i 0 = 0 and i k+1 = |D|+1. That is, D = D 0 , !t i1 , D 1 , !t i2 , D 2 , . . .!t i k , D k . Noting that dom (σ 1 )∩dom (σ 2 ) = ∅ let σ = σ 1 ∪ σ 2 .
For each t ∈ Sub(T 2 ) such that tσ ∈ Der(t i1 , . . . , t i k ) let i t be minimal such that tσ ∈ Der(t i1 , . . . , t it ), and let E 0 t be a proof of this fact, and E t be a sequence of standard deductions obtained by removing every non-standard deduction from E 0 t . For 0 ≤ j ≤ k let D j be the sequence of standard deduction steps D j , E s1 , . . . , E sp for all s m ∈ Sub(T 2 )σ \ Sub(T 1 )σ such that i sm = j in which every rule of E s1 , . . . , E sp that deduces a term previously deduced in the sequence or for some m ≤ j deduced in D m or in D[i m ] is removed.

Let D = D 0 , ?t i1 , D 1 , . . . , ?t i k , D k . We have deleted in each E 0 t only deductions whose right-hand side occurs before in D , and thus D is a derivation. Since the D i contains only standard deductions, we can see that D is (S, σ)compliant.

Since D is (T 1 , σ 1 )-maximal and no term is deduced twice in D we note that, for t ∈ T 1 , no standard deduction of tσ 1 from a sequence D j is deleted. Furthermore we note that standard deductions of terms T 2 σ 2 that are also in Inria T 1 σ 1 are deleted by construction and by the maximality of D. Thus a deduction whose right-hand side is in Sub(T 1 )σ 1 is in D iff it occurs in D.

By construction D is (T 2 , σ )-maximal and no term is deduced twice by standard deductions.

Taking T 1 = ∅, T 2 = Sub(S), and σ 2 = σ, Lemma 2 implies that for every substitution σ of domain Var(S) there exists a (S, σ)-compliant (Sub(S), σ)maximal derivation D. By Lemma 1 if σ |= S then D is a proof of σ |= S. Since the converse is trivial, it suffices to search proofs maximal wrt T ⊇ Sub(S).

Subterm deduction system

Definition and main property

We say that a deduction system is a subterm deduction system whenever each deduction rule which is not a nonce creation or a message reception is either:

1. x 1 , . . . , x n → f (x 1 , . . . , x n ) for a function symbol f ; 2. l 1 , . . . , l n → r for some terms l 1 , . . . , l n , r such that r ∈ n i=1 Sub(l i ). A composition rule is either a message reception, a nonce creation, or a rule of the first type. A deduction rule is otherwise a decomposition rule. Reachability problems for deduction systems with a convergent equational theory are reducible to the satisfiability of a constraint system in the empty theory for a deduction system in our setting [START_REF] Lynch | On the relative soundness of the free algebra model for public key encryption[END_REF][START_REF] Kourjieh | Logical Analysis and Verification of Cryptographic Protocols[END_REF]. If furthermore the equational theory is subterm [START_REF] Baudet | Deciding security of protocols against off-line guessing attacks[END_REF] the reduction is to a subterm deduction system as just defined above.

Now we show that if D, σ, α S, a term s ∈ Sub(D) is either the instance of a non-variable subterm of Out(S) or deduced by a standard composition. Lemma 3. Let σ be a ground substitution such that σ |= S. If D is a proof of σ |= S such that no term is deduced twice in D by standard rules and s is a term such that s ∈ Sub(D) and s / ∈ (Sub(Out(S)) \ X )σ then there exists an index i in D such that D[i] = l → s is a composition rule and s / ∈ Sub(R D (i -1)).

Proof. First we note that by definition of subterm deduction systems for any decomposition rule l → r we have a) r ∈ Sub(l), and b) for any composition rule l → r we have l ⊂ Sub(r) and Sub(r) \ Sub(l) = {r}.

Let D be a proof of σ |= S, and let i be minimal such that

D[i] = l r * → r with s ∈ Sub(r). Since l r ⊆ R D (i -1), the minimality of i implies s ∈ Sub(r) \ Sub(l r ).
Thus by a) D[i] cannot be a decomposition.

If D[i] =?r then by the (S, σ)-compliance of D we have S[α -1 (i)] =!t with tσ = r. We have s ∈ Sub(r) = Sub(tσ) = Sub(t)σ ∪ Sub(Vars (t) σ).

If s ∈ (Sub(Out(S)) \ X )σ we are done, otherwise there exists y ∈ Vars (t) with s ∈ Sub(yσ). By the origination property, there exists k < α -1 (i) such that S[k] =?t with y ∈ Vars (t ). Since D, σ, α S and k < α -1 (i) there exists j < i such that D[j] = l j → t σ. The minimality of i is contradicted by s ∈ Sub(t σ). Therefore, D[i] = l r → r is a standard composition rule. As a consequence, Sub(r) \ Sub(l r ) = {r}. Since s ∈ Sub(r) \ Sub(l r ), we finally obtain s = r.

Locality

Subterm deduction systems are not necessarily local in the sense of [START_REF] Mcallester | Automatic recognition of tractability in inference relations[END_REF]. However we prove in this subsection that given σ, there exists a finite extension T of Sub(S) and an extension σ of σ of domain Var(T ) and a (T, σ )-maximal derivation D in which every deduction relevant to the proof of σ |= S is liftable into a deduction between terms in T . Let us first precise the above statements.

≤ i ≤ m if D[i]
is a standard rule and there exists t ∈ Sub(T ) \ X such that tσ = r i , there exists t 1 , . . . , t n ∈ Sub(T ) such that {t 1 σ, . . . , t n σ} ⊆ R D (i -1) and t 1 , . . . , t n → t is the instance of a standard deduction rule.

First, we prove that for subterm deduction systems, every proof D of σ |= S is localized by a set T of DAG size linear in the DAG size of S. Proof. By Lemma 2 applied with T 1 = ∅, T 2 = Sub(S), σ 1 = ∅, σ 2 = σ, and D 0 the (S, σ)-compliant derivation that has no standard deductions, there exists a (Sub(S), σ)-maximal (S, σ)-compliant derivation D in which no term is deduced twice by a standard deduction. From now on we let T 0 = Sub(S).

Let {l i → r i } 1≤i≤n be the set of decompositions in D, and {(L i → R i , τ i )} 1≤i≤n be a set of decomposition rules and ground substitutions such that for all 1 ≤ i ≤ n we have L i τ i → R i τ i = l i → r i . Since no term in D is deduced twice by a standard deduction, by Lemma 3 we have n ≤ |Sub(Out(S))|.

Modulo variable renaming we may assume that i = j implies dom (τ i ) ∩ dom (τ j ) = ∅, and thus that τ

= n i=1 τ i is defined on T 1 = n i=1 (Sub(L i ) ∪ Sub(R i )). Note that the size of T 1 is bounded by M × |Sub(Out(S))|,
where M is the maximal size of a decomposition rule belonging to the deduction system.

Let T = T 0 ∪ T 1 and, noting that these substitutions are defined on nonintersecting domains, let

σ = σ ∪ τ . By construction |T | ≤ (M + 1) × |Sub(S)|.
By Lemma 2 there exists a (S, σ)-compliant derivation D which is (T, σ )maximal and such that every deduction of a term in T 0 σ that occurs in D also occurs in D and no term is deduced twice in D by a standard deduction.

Let l → r be a deduction in D which does not appear in D. Since D is (T 0 , σ)-maximal we have r / ∈ Sub(T 0 )σ, and thus r / ∈ Sub(Out(S))σ. Since no term is deduced twice in D by Lemma 3 this deduction must be a composition.

Let us prove D is (T, σ )-localized. By definition of composition rules, every composition that deduces a term tσ with t ∈ Sub(T ) \ Var(T ) has a left-hand Inria side t 1 σ , . . . , t k σ with t 1 , . . . , t k ∈ Sub(T ) and t 1 , . . . , t k → t is an instance of a composition rule. By the preceding paragraph every decomposition in D occurs in D and thus by construction has its left-hand side in T 1 σ which was previously built in D and is an instance of some

L i → R i such that Sub(L i ∪ {R i }) ⊆ T 1 ⊆ T .
Thus every deduction whose right-hand side is in (Sub(T ) \ Var(T ))σ has its left-hand side in Sub(T )σ , and thus D is localized by T for σ .

We prove now that to solve constraint systems one can first guess equalities between terms in T and then solve constraint systems without variables. The guess of equalities is correct wrt a solution σ if terms in T that have the same instance by σ are syntactically equal. We characterize these guesses as follows.

Definition 3.2 (One-to-one localizations). A set of terms T one-to-one localizes a derivation D for a ground substitution σ if σ is injective on Sub(T ) and T localizes D for σ.

In Lemma 7 we prove that once equalities between variables are correctly guessed there exists a one-to-one localization of a maximal proof D. Lemma 5. Let T be a set of terms such that T = Sub(T ), σ be a ground substitution defined on Vars (T ), U = {p = ? q : p, q ∈ T ∧ pσ = qσ} be a unification system and θ be its most general idempotent unifier with Vars (img (θ)) ⊆ Vars (U ). Then for any term t, tθσ = tσ. Since U contains all equations p = ? p for p ∈ Sub(T ) = T , we have Sub(T ) = Sub(U ). From the idempotency of θ (∀y ∈ Vars (U ) , yθθ = yθ), we get ∀y ∈ Vars (img (θ)) , yθ = y.

As σ is evidently a unifier of U , there exists a substitution τ such that σ = θτ Therefore, yσ = yθτ = yτ , i.e. yσ = yτ for all y ∈ Vars (img (θ)). Thus, for any

x ∈ Vars (T ), xθσ = xθτ = xσ.
Consequently, for any term t we have tσ = tθσ. we have v i θ = u i θ. It is enough to prove that v i θ = u i θ . Let us prove this case by induction on min(ht (u) , ht (v)). For the basis of induction, we have that either u i ∈ X or v i ∈ X (otherwise the basis is not minimal) and we have proved already that v i θ = u i θ =⇒ v i θ = u i θ . Suppose the statement is true for min(ht (u) , ht (v)) ≤ n. For min(ht (u) , ht (v)) = n + 1 we have ht (u i θ) ≤ n, ht (v i θ) ≤ n and u i θ = v i θ for all i. Then by induction supposition and two cases considered before we have u i θ = v i θ .

Thus, ∀u, v ∈ Sub(U )uθ = vθ =⇒ uθ = vθ , i.e. θ is a unifier of U . Moreover, for all x ∈ dom (θ) , xθ = (xθ )γ, where γ = {z → p}.

Since θ is a most general unifier, we have p ∈ X which contradicts to p ∈ Sub(xθ|x ∈ dom (θ)) \ X . Let U = {t = ? t : t, t ∈ Sub(T 0 ) and tσ = t σ }. The unification system U has a unifier σ and thus has a most general solution θ. By Lemma 5, σ = θσ .

Let T = Sub(T 0 )θ. Since Sub(S) ⊆ T 0 we have Sub(Sθ) ⊆ Sub(T 0 θ). Since θ is a most general unifier of U and Sub(U) = Sub(T 0 ) we have Sub(T 0 θ) = Sub(T 0 )θ by Lemma 6. This implies (i) Sub(Sθ) ⊆ T , (ii) θ is of linear size on |Sub(T 0 )| and thus on |Sub(S)|, and (iii) T is of linear size on |Sub(S)|. Moreover, as σ = θσ we have Sub(T )σ = Sub(T 0 )σ and thus from D is (T 0 , σ )-maximal follows D is (T, σ )-maximal.

Assume there exists t, t ∈ Sub(T ) such that tσ = t σ but t = t . Since T = Sub(T 0 θ) there exists t 0 , t 0 ∈ Sub(T 0 ) such that t 0 θ = t 0 θ but t 0 θσ = t 0 θσ . From σ = θσ we have an existence of t 0 , t 0 ∈ Sub(T 0 ) such that t 0 θ = t 0 θ but t 0 σ = t 0 σ . This contradicts the fact that θ satisfies U.

Inria

Finally, from D is (S, σ)-compliant and σ = θσ we have D is (Sθ, σ)compliant.

Milestone sequence

In addition to retrace the deduction steps performed in D we want to track which terms relevant to S are deduced in T , and in which order. Definition 3.3 (Milestone sequence). Let T be a set of terms and σ be a ground substitution. We say that T is the (T, σ)-milestone sequence of a derivation D = (l i → r i ) 1≤i≤m if T = t 1 , . . . , t n is a sequence of maximal length in which each t i is either of the form → t or of the form ?t, with t ∈ Sub(T ) and there exists a strictly increasing function α : {1, . . . , n} → {1, . . . , m} such that for every 1 ≤ i ≤ n we have:

1. if T [i] =?t then D[α(i)] =?tσ; 2. if T [i] =→ t then D[α(i)] = l i → tσ

Deciding constraint systems

From now we suppose that the considered subterm deduction system contains a rule x 1 , x 2 → f (x 1 , x 2 ), where f is a function symbol with arity 2 that does not occur in any other rule.

Theorem 1. Let σ such that σ |= S, T such that T ⊇ Sub(S) and σ an extension of σ on Vars (T ). Let D be a (T, σ )-maximal derivation one-to-one localized by T for σ in which no term is deduced twice by a standard rule.

Then there exists a solution τ of S of size polynomial in |Sub(T )|.

Proof. First let us define a replacement of a term q by term p in t denoted as t| q← p as follows: t| q← p is the term is obtained from t by simultaneous replacing all occurrences of q in t by p. For a substitution σ = {x → t x : x ∈ dom (σ)} we define σ| q← p = {x → (t x | q← p ) : x ∈ dom (σ)} Let T be a (T, σ )-milestone sequence for D.

→ t first appears in T k . Since t is a variable, the last rule of E is also a composition, more precisely

t m k τ , n t → f (t m k τ , n t ). If k ≤ j, by construction of τ , tσ must be in R D (m). Thus, k > j. Since D [1 : m ], E is a derivation, either t m k τ ∈ R E (|E | -1) or t m k τ ∈ R D (m ).
[i] =→ o • If E [i] is another composition, then E [i] = t 1 , . . . , t v → h(t 1 , . . . , t v ).
Since t / ∈ X and E [1 : |E | -1] does not deduce terms from Sub(T )τ we have h(t 1 , . . . , t v ) = xτ for any x ∈ Vars (T ). Thus, h(t 1 , . . . , t v )δ = h(t 1 δ, . . . , t v δ) and we have t 1 δ, . . . , t v δ → h(t 1 δ, . . . , t v δ) is a composition rule.

• If E [i] is a decomposition, then since no decomposition rule contains f , the value of xτ (which is a fresh nonce or has f as a root symbol) may be replaced with any other term and we still obtain an instance of the same decomposition rule, i.e. E [i]δ is an instance of a decomposition rule.

As noted above, since ∀r ∈ Sub(T ), (rτ )δ = rσ and D 0 δ = D 0 by construction we have R D (m ) δ ⊆ R D (m) ∪ xτ : x ∈ X . Thus, D[1 : m], D 0 , E is a derivation deducing tτ δ = tσ , i.e. tσ ∈ Der(t i1 σ , . . . , t ij σ ). Contradiction.

Therefore, D is (T , τ )-maximal.

Conclusion.

Since Sub(S) ⊆ T , and τ is injective on Sub(T ), we have that by construction of D , for any term t ∈ Sub(S), tσ is deduced before j-th non-standard rule of D (resp. deduced in D) if and only if tτ is deduced before j-th non-standard rule of D (resp. deduced in D ). Therefore, since σ |= S and D is (S, σ)-compliant and (Sub(S), σ)-maximal and since D is (S, τ )-compliant and (Sub(S), τ )-maximal we may use twice Lemma 1 and obtain that τ satisfies S.

Corollary 1. Let S be a constraint system. S is satisfiable, if and only if there exists a solution σ of S with polynomial size w. From the previous result we can directly derive an NP decision procedure for constraint systems satisfiability: guess a substitution of polynomial size in |Sub(S)| and check whether it satisfies S in polynomial time (see e.g. [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]).

Conclusion

We have obtained the first decision procedure for deducibility constraints with negation and we have applied it to the synthesis of mediators subject to nondisclosure policies. It has been implemented as an extension of CL-AtSe [START_REF] Turuani | The CL-Atse Protocol Analyser[END_REF] for the Dolev-Yao deduction system. On the Loan Origination case study, the prototype generates directly the expected orchestration. Without negative constraints undesired solutions in which the mediator impersonates the clerks were found. More details, including problem specifications, can be found at http://cassis.loria.fr/Cl-Atse. As in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Baudet | Deciding security of protocols against off-line guessing attacks[END_REF] our definition of subterm deduction systems can be extended to allow ground terms in right-hand sides of decomposition rules even when they are not subterms of left-hand sides and the decidability result remains valid with minor adaptation of the proof. A more challenging extension would be to consider general constraints (as in [START_REF] Avanesov | Satisfiability of general intruder constraints with and without a set constructor[END_REF]) with negation.

Figure 1 :

 1 Figure 1: Clerk's communications and non-disclosure constraints

Figure 2 :Figure 3 :

 23 Figure 2: Client's Communications and non-disclosure constraints Composition rules Decomposition rules x, y → pair (x, y) pair (x, y) → x pair (x, y) → y x, rel(x, y) → y x, y → {|x|} y y, {|x|} y → x y, rel(x, y) → x x, y → {x} y inv (y) , {x} y → x x, inv (y) → {x} sig inv(y)

Figure 4 :

 4 Figure 4: A constraint system and a compliant derivation

Definition 2 . 5 (

 25 Proof of a solution). Let σ be a ground substitution. A derivation D is a proof of σ |= S, and we denote D, σ, α S, if:1. D is (S, σ)-compliant with the mapping α and 2. if S[i] =?t there is j < Next D (α(prev S (i))) such that D[i] = l * → tσ and 3. if S[i] = t then tσ / ∈ Der({t j σ : j ≤ prev S (i) and S[j] =!t j }).

Definition 3 . 1 (

 31 Localization set). A set of terms T localizes a derivation D = (l i * → r i ) 1≤i≤m for a substitution σ of domain Var(T ) if for every 1

Lemma 4 .

 4 If σ is a ground substitution such that σ |= S there exists T ⊇ Sub(S) of size linear in |Sub(S)|, a substitution τ of domain Var(T ) \ Var(S) and a (T, σ∪τ )-maximal and (S, σ)-compliant derivation localized by T for σ∪τ .

Proof.

  Let us show ∀x ∈ Vars (T ) , xσ = xθσ. Note that this trivially holds if xθ = x. Thus we consider case xθ = x.

Lemma 6 .

 6 Let U be a unification system and θ = mgu (U ) an idempotent most general unifier with Vars (img (θ)) ⊆ Vars (U ). Then ∀p ∈ Sub(img (θ)) ∃q ∈ Sub(U ) : p = qθ.Proof. The case where p ∈ X is trivial, since Vars (img (σ)) ⊆ Vars (U ) and we can take q = p. Otherwise, suppose that p ∈ Sub(xθ|x ∈ dom (θ)) \ X is such that ∀q ∈ Sub(U ) p = qθ. Let z be a fresh variable. Let θ = {x → (xθ)| p← z : x ∈ dom (θ)}. Let us denote the height of a term t by ht (t), and a subterm of t at position l by t[l] and the set of all positions in t by t[].Let us prove that ∀u, v ∈ Sub(U ) uθ = vθ =⇒ uθ = vθ .• If u, v ∈ X then the statement is true by definition.• If, w.l.o.g., u ∈ X but v / ∈ X . Then for any l ∈ v[] we have (uθ)[l] = (v[l])θ. Since v[l] ∈ Sub(U )we get (uθ)[l] = p (as we took such p that ∀q ∈ Sub(U ) p = qθ), and therefore, (v[l])θ = p. Thus, (vθ)| p← z = vθ . Therefore, uθ = (uθ)| p← z = (vθ)| p← z = vθ . • If u = f (u 1 , . . . , u k )∧v = g(v 1 , . . . , v m ) then f = g, m = k and for all i ≤ k

Lemma 7 .

 7 Let S be a constraint system, σ be a ground substitution such that σ |= S.Then there exists a set of terms T , a substitution τ of domain Var(T ) \ Var(S), a substitution θ and a (Sθ, σ)-compliant derivation D such that • D is (T, σ ∪ τ )-maximal and one-to-one localized by T for σ ∪ τ• σ ∪ τ = θ(σ ∪ τ ) • Sub(Sθ) ⊆ T • T and θ of size linear in |Sub(S)|Proof. Under the same assumptions, by Lemma 4, there exists T 0 ⊇ Sub(S) of size linear in |Sub(S)| and τ of domain Var(T 0 ) \ Var(S) such that there exists a (T 0 , σ ∪ τ )-maximal and (S, σ)-compliant derivation D which is localized by T 0 for the same substitution σ = σ ∪ τ .

Lemma 8 .

 8 is a standard deduction rule; Let σ |= S, T ⊇ Sub(S) and σ be an extension of σ on Vars (T ). Let D be (T, σ )-maximal derivation one-to-one localized by T for σ . Let T be a (T, σ )-milestone sequence. Then for any i for any x ∈ Vars T [i] there exists j < i such that T [j] =→ x. Proof. If x ∈ Vars T [i] then there exists corresponding deduction D[j] that deduces term T [i]σ . Then by Lemma 3 there exists k < j such that D[j] deduces by a standard rule xσ . From the injectivity of σ follows that x is the only term of Sub(T ) having σ image equal xσ . Thus, by definition of milestone sequence, there exists m < i such that T [m] =→ x.

  r.t. |Sub(S)|. Proof. (⇐) is trivial, since σ |= S. Consider (⇒). Let σ |= S. By Lemma 7 there exists a set of terms T , a substitution θ both with the size linear in |Sub(S)| Inria and an extension γ of σ and (T, γ)-maximal (Sθ, σ)-compliant derivation D oneto-one localized by T for γ. We also have γ = θγ (which implies σ = θσ). Thus σ satisfies Sθ. From the same lemma we have Sub(Sθ) ⊆ T . By Theorem 1 there exists a substitution τ of size polynomial in |Sub(T )| (and consequently, polynomial in |Sub(S)|) such that τ |= Sθ. From this we have θτ |= S. Moreover, since both θ and τ are of polynomial size on |Sub(S)|, σ = θτ is also of polynomial size on |Sub(S)| and σ |= S.

  The former contradicts the choice of E . The latter case implies t m k σ ∈ R D (m) ⊆ Der(t m1 σ , . . . , t mj σ ) and thus, as j < k we have that Der(t m1 σ , . . . , t m k σ ) = Der(t m1 σ , . . . , t m k-1 σ ). Thus, T k must be empty, otherwise it contradicts the maximality of D and that no term is deduced twice by a standard rule in D. This contradicts that → t appears first in T k . Thus, t / ∈ X . Let us build a sequence of rules E such thatE[i] = E [i]δ and show that D[1 : m], D 0 , E is a proof of tσ ∈ Der(t m1 σ , . . . , t mj σ ).Let us show that E [i]δ is a rule.• If E [i] =→ o is a nonce generation, then o / ∈ img (τ ) due to the minimality of E and since all variables of T that are mapped to nonces by τ are deduced in D before the first non-standard rule. Thus oδ = o and we have E

RR n°8017

Let M = m 1 , . . . , m n be the maximal increasing sequence such that for any i = 1, . . . , n, T [m i ] =?t mi . We put also m 0 = 0 and

Goal. We will prove the existence of a ground substitution τ , set of terms T ⊇ T and a derivation D which is (S, τ )-compliant, (T , τ )-maximal (where τ = τ | Vars(S) is of a linear size on Sub(T )) and is one-to-one localized by T with τ such that its (T, τ )-milestone sequence coincides with T .

If it is proved, by Lemma 1 we can show that τ |= S.

Build T . Let X be the set of variables of T whose σ -instance are not derivable from the empty knowledge. By Lemma 8 each variable x of Vars T appears first as → x in T . Therefore, we may put X = {x 1 , . . . , x u } = Vars T \ x :→ x ∈ T 0 . Let for each x ∈ X, let x be a new fresh variable (corresponding to x) and let X = {x : x ∈ X}. Finally, we put T = T ∪ X.

Build τ . Let τ be a ground substitution defined as follows:

• for any x ∈ X, xτ is a nonce n x and xτ = f (t mi τ , n x ), where → x appears first in T i (note that by Lemma 8 for any y ∈ Vars (t mi ), → y appears first time at position before m i in T and thus τ is correctly defined); • for any y ∈ Vars T 0 , yτ = n y ;

• 2 for any z ∈ Vars (T ) \ Vars T , zτ = a z , where a z is a fresh constant from A \ C med not appearing in Sub(T ).

We can see that xτ is of polynomial size on |Sub(S)| for any x ∈ Vars (T ). Show τ is injective on Sub(T ). Suppose the contrary, let p, q ∈ Sub(T ) be a pair with minimal size of pτ and having pτ = qτ , while p = q. If neither p nor q is a variable, then this contradicts the minimality of pτ (we can choose subterms of p and q satisfying the choice criteria). If both are variables, then it is not possible by the construction of τ . W.l.o.g. let p ∈ X and q / ∈ X . The case where pτ is a nonce or another constant is impossible; thus pτ = f (t ij , n x ) and q = f (u, x) (since by construction for every nonce n x there exists only one variable x such that xτ = n x and n x / ∈ Sub(T )). But again, by construction (note that x was a fresh variable), the only term in Sub(T ) having x as a subterm is x, thus q ∈ X : contradiction.

=→ t and t / ∈ X then since D is one-to-one localized by T , there exists t 1 , . . . , t k such that ?t j ∈ T [1 : i -1] or →t j ∈ T [1 : i -1] for j = 1, . . . , k and t 1 , . . . , t k → t is a deduction rule. Thus, we put

T [1 : i]τ . Thus, by the construction D is a derivation which is (S, τ )-compliant and localized by T for τ . Moreover, it is one-to-one localized since τ is injective on Sub(T ).

We have by construction of D that its

The case t ∈ X is trivial, since Xτ is deduced at the very beginning of D . Suppose that there an exists index j and term t ∈ Sub(T ) such that tτ ∈ Der(t m1 τ , . . . , t mj τ ) but tτ / ∈ R D (u + m j+1 -1), i.e. tτ is not deduced before the next to j non-standard rule in D . In this case, tσ / ∈ Der(t m1 σ , . . . , t mj σ ), otherwise by maximality tσ would be deduced before (j + 1)-th non-standard rule of D and by construction, tτ would also appear in D before (j + 1)-th nonstandard rule of D .

Let j be such a minimal index. Note that Vars (t) ⊆ Vars T , otherwise by construction tτ would contain some fresh constants from A \ C med and thus would not be derivable from t i1 τ , . . . , t ij τ . Let m (resp. m) be the maximal index such that D Let S be a constraint system obtained from S by removing all constraints after j-th !-constraint and removing all -constraints. By construction, D [1 : m ], E is a proof of τ |= S and thus we can apply Lemma 3, i.e. all rules of E [1 : |E | -1] are compositions.

Suppose that t is a variable. Note that tτ is not a nonce, otherwise by definition of τ , t ∈ T 0 and thus tσ ∈ R D (m). Therefore, tτ = f (t m k τ , n t ), where


Romain Lafay
email: romain.lafay@ujf-grenoble.fr

German Montes-Hernandez
email: german.montes-hernandez@obs.ujf-grenoble.fr

Emilie Janots

Rodica Chiriac

Nathaniel Findling

Francois Toche

Keywords: A1. Serpentinization, A1. Mineral replacement rate, B1. Alkaline medium, B2. Chrysotile nanotubes, A1. TG analyses

Olivine mineral replacement by serpentine is one major alteration reaction of oceanic hydrothermalism. In the present experimental study, olivine grains were replaced by chrysotile and brucite under high alkaline conditions. In our study, olivine replacement implied a spatial and temporal coupling of dissolution and precipitation reactions at the interface between olivine and chrysotile-brucite minerals. Coupled dissolution-precipitation led to the alteration of starting olivine grains (so-called primary or parent mineral) to a porous mineral assemblage of chrysotile and brucite with preservation of the initial olivine morphology. This mineral replacement reaction of olivine (serpentinization) has been characterized using XRD, FESEM and FTIR measurements. Moreover, a simple and novel method is here proposed to quantify the mineral replacement rate (or serpentinization rate) of olivine by using thermogravimetric (TG) and differential TG (DTG) analyses.

Serpentinization extent depends on the grain size: it is complete after 30 days of reaction for the smallest olivine grains (<30µm), after 90 days of reaction for the intermediate olivine grains (30 µm-56 µm) and reaches 55% of olivine replacement after 90 days for the largest fraction (56-150 µm). Based on the fitting of the serpentinization extent ( t ) versus time (t) by using a kinetic pseudo-second-order model, the serpentinization rates vary from 3.6x10 -6 s - 1 to 1.4x10 -7 s -1 depending on the olivine grain size. An additional correlation between FTIR spectra analysis and TG measurements is proposed. The mineral replacement reactions frequently observed in natural alteration processes could be a powerful synthesis route to design new porous and/or nanostructured materials.

Introduction

Serpentine minerals (chrysotile, lizardite and antigorite) are widespread in Earth oceanic lithosphere and are frequently found in chondrites and other extraterrestrial objects.

Serpentine mineralization is of great interest in several fields of research. Serpentinized rocks present a great enrichment in trace elements compared to primary mantle rocks [START_REF] Deschamps | In situ characterization of serpentinites from forearc mantle wedges: Timing of serpentinization and behavior of fluid-mobile elements in subduction zones[END_REF][START_REF] Hattori | Volcanic fronts form as a consequence of serpentinite dehydration in the forearc mantle wedge[END_REF][START_REF] Hattori | Geochemical character of serpentinites associated with high-to ultrahigh-pressure metamorphic rocks in the Alps, Cuba, and the Himalayas: Recycling of elements in subduction zones[END_REF][START_REF] Lee | Internal distribution of Li and B in serpentinites from the Feather River Ophiolite, California, based on laser ablation inductively coupled plasma mass spectrometry[END_REF][START_REF] Mccollom | Fluid-rock interactions in the lower oceanic crust: Thermodynamic models of hydrothermal alteration[END_REF][START_REF] Vils | The Lithium, Boron and Beryllium content of serpentinized peridotites from ODP Leg 209 (Sites 1272A and 1274A): Implications for lithium and boron budgets of oceanic lithosphere[END_REF].

Serpentine appears as a vector for trace elements between crustal and mantle reservoirs [START_REF] Hattori | Volcanic fronts form as a consequence of serpentinite dehydration in the forearc mantle wedge[END_REF][START_REF] Mccollom | Fluid-rock interactions in the lower oceanic crust: Thermodynamic models of hydrothermal alteration[END_REF][START_REF] Deschamps | Serpenttines act as sponges for Fluid-Mobile-Elements in abyssal and subduction zone environments[END_REF][START_REF] Guillot | Evidence of hydration of the mantle wedge and its role in the exhumation of eclogites[END_REF]. Experimental studies have tested the influence of major (e.g. Fe, Ni) and/or trace elements (e.g. Li) on the growth of serpentine [START_REF] Bloise | Influence of synthesis conditions on growth of Ni-doped chrysotile[END_REF][START_REF] Bloise | Synthesis of Fe-doped chrysotile and characterization of the resulting chrysotile fibers[END_REF][START_REF] Bloise | Hydrothermal alteration of Ti-doped forsterite to chrysotile and characterization of the resulting chrysotile fibers[END_REF][START_REF] Korytkova | Influence of iron on the kinetics of formation of chrysotile nanotubes of composition (Mg, Fe) 3 Si 2 O 5 (OH) 4 under hydrothermal conditions[END_REF][START_REF] Mcdonald | Hydrothermal preparation of nanotubular particles of a 1:1 nickel phyllosilicate[END_REF][START_REF] Wunder | The effect of chrysotile nanotubes on the serpentine-fluid Li-isotopic fractionation[END_REF]. This kind of synthesis experiments presents a great interest in medical research due to the asbestos toxicity that can be induced by inhalation of magnesium silicates fibers including chrysotile [START_REF] Falini | Interaction of Bovine Serum Albumin with Chrysotile: Spectroscopic and Morphological Studies[END_REF][START_REF] Gualtieri | In situ ESEM study of the thermal decomposition of chrysotile asbestos in view of safe recycling of the transformation product[END_REF][START_REF] Foresti | Asbestos health hazard: A spectroscopic study of synthetic geoinspired Fe-doped chrysotile[END_REF][START_REF] Sabatino | Synthetic chrysotile nanocrystals as a reference standard to investigate surface-induced serum albumin structural modifications[END_REF]. Serpentine minerals are also crucial for sequestration of CO 2 due to its availability and sequestration capacity [START_REF] Beinlich | CO2 sequestration and extreme Mg depletion in serpentinized peridotite clasts from the Devonian Solund basin, SW-Norway[END_REF][START_REF] Larachi | Fixation of CO2 by chrysotile in low-pressure dry and moist carbonation: Ex-situ and in-situ characterizations[END_REF][START_REF] Mccollom | A reassessment of the potential for reduction of dissolved CO2 to hydrocarbons during serpentinization of olivine[END_REF] . Indeed a lot of studies are looking for technologies that could possibly contribute to reduce carbon dioxide emissions. Geological sequestration and ex-situ mineralization of CO 2 using serpentine could be one of the most efficient methods considering the enormous quantity of serpentine on Earth [START_REF] Yajima | Field study on CO2 fixation by serpentinite rock-bed[END_REF].

In meteorites, serpentine minerals are directly linked to aqueous alteration processes and reaction conditions (e.g. [START_REF] Beck | Hydrous mineralogy of CM and CI chondrites from infrared spectroscopy and their relationship with low albedo asteroids[END_REF] and references therein). In the oceanic lithosphere, serpentines result from interaction between mantle rocks (peridotite composed by olivine and pyroxenes) and hydrothermal fluids, generally with high fracturation dynamic [START_REF] Andreani | A microstructural study of a « crack-seal » type serpentine vein using SEM and TEM techniques[END_REF][START_REF] Andreani | Dynamic control on serpentine crystallization in veins: Constraints on hydration processes in oceanic peridotites[END_REF]. Olivine alters along grain boundaries and fractures to produce a mesh texture that preserves the original olivine morphology at the grain scale [START_REF] Wicks | Serpentine textures and serpentinization[END_REF][START_REF] Evans | The serpentinite multisystem revisited: Chrysotile is metastable[END_REF]. This olivine replacement by serpentine is best explained by coupled dissolution-precipitation processes [START_REF] Putnis | Mineral Replacement Reactions[END_REF][START_REF] Putnis | The mechanism of reequilibration of solids in the presence of a fluid phase[END_REF][START_REF] Putnis | Mineral replacement reactions: from macroscopic observations to microscopic mechanisms[END_REF]. This reequilibration process leads to the replacement of one pristine mineral by a secondary mineral (or assemblage) with a lower solubility in the fluid. Replacement occurs at the fluid/solid interface maintaining the original external grain shape (pseudomorphism). During alteration, a secondary porosity is commonly produced due to volume difference between pristine and secondary minerals, material loss during dissolution and grain fracturation [START_REF] Andreani | A microstructural study of a « crack-seal » type serpentine vein using SEM and TEM techniques[END_REF][START_REF] Andreani | Dynamic control on serpentine crystallization in veins: Constraints on hydration processes in oceanic peridotites[END_REF]. Secondary porosity enables the fluid to move interstitially towards the reaction front until the complete mineral replacement reaction. In oceanic lithosphere, peridotite replacement, and consequent element redistribution associated with this alteration, is primarily controlled by the physic-chemical conditions of the hydrothermal fluid (Temperature, Pressure, fluid speciation, pH). Fluids escaping from deep sea hydrothermal vents show a large variety of composition and pH, reflecting a large range of possible physic-chemical conditions. Amongst them, alkaline fluids with high pH were collected in some hydrothermal fields (e.g., [START_REF] Kelley | An off-axis hydrothermal vent field near the Mid-Atlantic Ridge at 30[deg] N[END_REF][START_REF] Ludwig | Formation and evolution of carbonate chimneys at the Lost City Hydrothermal Field[END_REF]).

Numerous experimental studies were conduct to reproduce serpentinization in hydrothermal context [START_REF] Allen | Compositional controls on vent fluids from ultramafichosted hydrothermal systems at mid-ocean ridges: An experimental study at 400°C, 500 bars[END_REF][START_REF] Macdonald | Rate of serpentinization in seafloor environments[END_REF][START_REF] Marcaillou | Mineralogical evidence for H2 degassing during serpentinization at 300 °C/300 bar[END_REF][START_REF] Martin | Some experimental and theoretical observations on the kinetics of hydration reactions with particular reference to serpentinization[END_REF][START_REF] Seyfried | Seawater-peridotite interaction at 300°C and 500 bars: implications for the origin of oceanic serpentinites[END_REF][START_REF] Seyfried | Redox evolution and mass transfer during serpentinization: An experimental and theoretical study at 200 °C, 500 bar with implications for ultramafic-hosted hydrothermal systems at Mid-Ocean Ridges[END_REF][START_REF] Wegner | Experimentally determined hydration and dehydration reaction rates in the system MgO-SiO2-H2O[END_REF][START_REF] Yada | Growth and microstructure of synthetic chrysotile[END_REF] and explain serpentine growth [START_REF] Baronnet | Topology and crystal growth of natural chrysotile and polygonal serpentine[END_REF]. Kinetic appears faster under alkaline conditions [START_REF] Yada | Growth and microstructure of synthetic chrysotile[END_REF][START_REF] Yada | Serpentine minerals hydrothermally synthesized and their microstructures[END_REF] but few recent studies have addressed the role of pH on serpentinization kinetic, particularly in alkaline conditions.

In the present experimental study, we have investigated the process and kinetics of olivine serpentinization in alkaline hydrothermal conditions (pH = 13.5, measured at 25°C).

Experimental products were characterized using XRD, FESEM and FTIR. The serpentinization rate was determined using a simple and novel method based on thermogravimetric analyses (TGA/DTGA). This demonstrates that serpentinization is much faster under alkaline conditions refering to previous study at comparable conditions [START_REF] Marcaillou | Mineralogical evidence for H2 degassing during serpentinization at 300 °C/300 bar[END_REF][START_REF] Martin | Some experimental and theoretical observations on the kinetics of hydration reactions with particular reference to serpentinization[END_REF][START_REF] Seyfried | Redox evolution and mass transfer during serpentinization: An experimental and theoretical study at 200 °C, 500 bar with implications for ultramafic-hosted hydrothermal systems at Mid-Ocean Ridges[END_REF] and can lead to total replacement of <30µm olivine in less than 30 days and 90 days for 30<particle size<56 µm.

Materials and Methods

Millimetric grains of olivine San Carlos (Fo 90 ) were crushed by using a Fritsh Pulverisette 7 micro-crusher. Three classes of grain/particle size (particle size<30µm, 30<particle size<56µm and 56<particle size<150µm) were isolated by sieving. The samples were washed three times using high-pure water in order to remove the ultrafine particles that possibly stuck at grain surfaces during crushing step. Optical and electron microscopy was performed to control the initial state/appearance of olivine surfaces.

Alteration experiments

1.5ml of high alkaline solution (1M of NaOH, pH≈13.5 at 25°C) and 100mg of San Carlos olivine at a given class of particle size were placed in a Teflon cell reaction (cap-cell also in Teflon). Cell reaction and cap-cell were previously washed by an acidic treatment followed by washing with high-pure water. This cell reaction was immediately assembled into a steel autoclave without agitation, referred as "static batch reactor" and the closed autoclave was placed in a multi-oven (ten independent-temperature compartments) and heated to 150°C or 200°C (P sat ~0.5Mpa and P sat ~1.6Mpa). Various olivine-alkaline solution reaction times from 3h to 90 days were considered in order to determine the mineral replacement rate (or serpentinization rate) of olivine at the investigated hydrothermal conditions. Particularly, the effect of initial particle size (three different classes: particle size<30µm, 30<particle size<56µm and 56<particle size<150µm) on the serpentinization rate of olivine was tested.

All experimental conditions are summarized in table 1.

At the end of the experiment, the autoclave was quenched in cold water. This manipulation avoids precipitation during cooling with no perturbation of the reaction products. Then, the autoclave was disassembled and the fluid was collected for pH and major elements concentration (Mg, Fe and Si) measurements (not shown in this study). After all experiments, pH of the experimental fluid is still around 13.5 (measured at 25°C). The solid product was dried directly in the Teflon cell at 80°C for 24h. The dry solid product was recovered for further solid characterizations described below.

X-Ray diffraction measurements

X-Ray diffraction (XRD) analyses were performed in the ISTerre laboratory. All samples were crushed manually. The powders were carefully placed and manually compacted in borosilicated capillaries of 500µm of diameter, this corresponds to about 5 mg of sample.

XRD patterns were recorded with a Bruker D8 powder diffractometer equipped with a SolX Si (Li) solid state detector from Baltic Scientific Instruments using CuKα1-Kα2 radiation and a Göbel mirror. Intensities were recorded for an 2 interval from 5 to 80° with an 8 s counting time per 0.024° 2 step for bulk mineralogy determination.

FESEM observations

Grain size and morphology of the experimental products were characterized using secondary or backscattering electrons. Micro-imaging was obtained using Zeiss Ultra 55 Field emission gun scanning electron microscopy (FESEM). This enables a spatial resolution of approximately 1nm at 15 kV. Samples were dispersed by ultrasonic treatment in absolute ethanol for at least 5mn in order to disaggregate the particles. One or two drops of dispersion were placed onto an aluminium support and coated with a thin film of platinium for SEM observation.

Thermogravimetric analyses (TGA)

TGA for experimental solid products were performed with a TGA/SDTA 851 e Mettler Toledo instrument under the following conditions: sample mass of about 10 mg, platine crucible of 150 µl with a pinhole, heating rate of 10 °C min -1 , and inert N 2 atmosphere of 50 ml min -1 .

Sample mass loss and associated thermal effects were obtained by TGA/DTGA in a temperature range from 30°C to 1200°C. In order to identify the different mass loss steps, the TGA first derivative (rate of mass loss) was used. TGA apparatus was calibrated in terms of mass and temperature. Calcium oxalate was used for the sample mass calibration. The melting points of three compounds (indium, aluminium and copper) obtained from the DTGA signals were used for the sample temperature calibration. The temperature accuracy of the TGA/SDTA system is about ± 0.25°C. The weighting accuracy is around 0.1µg, which correspond to 0.01% for a 10mg sample.

FTIR measurements

FTIR measurements (in transmission mode) were performed using an IR microscope Bruker Hyperion 3000. The IR beam was focused through a 15x lens and the typical size of infrared aperture is 50*50 µm². The light source is a Globar(TM) and the beam splitter is in KBr. The spectra were measured from 700 to 4000 cm -1 (4cm -1 resolution) with a MCT monodetector cooled by liquid nitrogen.

Samples must be thin (less than 100 µm) and flat to avoid absorption band saturation or scattering effects. Sample preparation has involved a careful crushing of samples in mortar and manual compaction of fine crushed particles between two K-Br windows. Five spectra per samples were realized; they were fitted using OPUS software.

Results and discussion

Serpentinization reaction under alkaline conditions

Secondary minerals were identified by XRD and FESEM (Figs. 1 and2) and they were quantified by TGA (Fig. 3). Under alkaline conditions, olivine is replaced by chrysotile and brucite, independently on the starting grain size of olivine. No other minerals were detected and/or observed during this alteration reaction.

FESEM micro-imaging has revealed a clear evolution of particle size and morphology of crystal faces during serpentinization advancement (Fig. 2). Serpentine nucleation at olivine-alkaline solution interfaces is observable by FESEM after only few hours of reaction when the starting grain size is <30µm (Fig. 2a). These occur as nanosized nodules forming irregular sub-micrometric rods. They are still observed onto olivine surfaces after few days of reaction and a more advanced serpentinization reaction (Fig. 2c). The irregular submicrometric rods were identified as chrysotile and brucite "nucleates" from TGA/DTGA in the solid product (Fig. 3). While brucite is detected by XRD in the first stages of replacement (e.g. 3 hours of reaction for <30µm grains), chrysotile was not detected by XRD , possibly due to its poor crystallinity and/or nanometric size. Chrysotile was detected by XRD after 16h of reaction for the smallest starting grains (<30µm), however, several days of olivine-fluid interactions are required when the starting grain size is >30µm (Fig. 1a,b). At advanced alteration stages, serpentinized samples consist of tubular, conical and cylinder-in-cylinder chrysotile with nanometric diameter and microsized hexagonal brucite were clearly observed (Fig. 2e,g,h). Diameter of secondary products depends of the starting material grain size. It increases from ~50 nm for the <30 µm, to 200-300 nmfor 30-56 µm and 56-150 µm fractions.

Lizardite was not observed. Previous study suggested that lizardite crystallized at lower levels of supersaturation than chrysotile [START_REF] Normand | Hydrothermal alteration of olivine in a flow-through autoclave: Nucleation and growth of serpentine phases[END_REF]. Here, we confirm that high alkaline pH favors chrysotile precipitation [START_REF] Yada | Growth and microstructure of synthetic chrysotile[END_REF][START_REF] Yada | Serpentine minerals hydrothermally synthesized and their microstructures[END_REF].

In natural samples, olivine replacement in mesh texture is commonly described as an assemblage of serpentine±brucite±magnetite. Typically, the magnetite amount depends on the Mg# (Mg# = Mg / (Mg +Fe)) in primary olivine. Neither iron oxides (ex. magnetite or hematite) nor oxyhydroxides (ex. goethite) were observed in our experiments. Semiquantitative EDS analyses have revealed that the initial iron contained in olivine was preferentially incorporated as Fe 2+ into brucite (Mg# brucite =0.84), and slightly sequestered into/onto chrysotile (Mg# chrysotile =0.95) compared to starting San-Carlos olivine. In our conditions a part of Fe 3+ (not determined) might substitute to Si into the chrysotile. In our experiments, one general reaction of San Carlos olivine alteration can be written as: follows:

2Mg 1,8 Fe 0,2 SiO 4 + 3H 2 O = (Mg 1-Z Fe Z )(OH) 2 +(Mg 1-X Fe X ) 3 Fe Y Si 2-Y (OH) 4 (1)
with X+Y ~0.05 and Z~0.16

This isochemical reaction implies a volume increase of ~25% (see discussion below).

On the XRD patterns (Fig. 1), characteristic peaks of chrysotile appear in the first hours or days of reaction, depending on the initial particle size of olivine (Fig. 1a,b). Secondary product growth rate is related to the variation of the crystal size with time. On the XRD patterns the full width at half maximum (FWHM) parameter for specific peaks, corresponding to a crystalline compound, can be directly associated to its coherent domain size when instrumental resolution function (IRF) and strain contribution are known. In our case, the FWHM for the plane (002) of chrysotile was used to obtain an estimation of the chrysotile size variation during the serpentinization process. Here, a decrease of FWHM implies an increase of coherent domain size as specified in the Scherrer equation. The FWHM variation with the reaction time reported in figure 1c shows a fast crystal growth step followed by a slow crystal growth step for chrysotile from 3h to 30 days when starting grain size is <30µm.

Conversely, chrysotile coherent domain varies only moderately from 20 to 90 days for starting grain size > 30 µm (Fig. 1c). In this latter case, two explanations are possible: firstly, a preferential growth of other(s) crystal plane(s) than plane (002) is involved, secondly, a dominant nucleation events promoting an increase of particle number concentration with time during mineral replacement of olivine can occur. FESEM observations support the first assumption because they have revealed a higher radial growth of tubular chrysotile for larger starting grain size (30-56µm and 56-150 µm) at similar reaction time (Fig. 2f,h).

Determination of serpentinization rate

The time for complete olivine-to-serpentine transformation or complete serpentinization process depends on the starting grain size. For example, 30 days were required when starting grain size was <30µm while about 90 days were required for the 30-56µm fraction (Fig. 1a,b). For 56-150µm starting grain size, around 55% of mineral replacement was reached after 90 days of experiments.

Serpentinization rate of olivine was determined by using a simple and novel method combining TGA and DTGA. TGA/DTGA were performed to quantify the molecular water (adsorbed or confined in pores) and hydroxyl groups (-OH) (incorporated in brucite and chrysotile) as illustrated in figure 3. In general, molecular water (H 2 O) adsorbed or confined in pores onto mineral assemblage, was released at moderate temperature (<200°C).

Conversely, the brucite and chrysotile minerals were dehydroxylated at higher temperatures.

Here, a dehydroxylation peak closed to 370°C was associated to brucite. This peak was shifted towards lower temperature, compared to the dehydroxylation of pure brucite peaking at 430°C. This change of thermal stability was related to a significant incorporated amount of iron (Fe 2+ ) into brucite structure as recently claimed by Okamoto et al. [START_REF] Okamoto | Progress of hydration reactions in olivine-H2O and orthopyroxenite-H2O systems at 250 °C and vapor-saturated pressure[END_REF]. Additionally we observed that weight loss ratio between serpentine and brucite is not constant following reaction advancement. Regarding the chrysotile, it was observed that it starts to be dehydroxylated at about 400°C and it was completely dehydroxylated at approximately 700°C for most of the experiments. In several cases, two typical dehydroxylation episodes were measured at 515 and 600 °C, respectively. We note that the starting dehydroxylation step for chrysotile can be overlapped with residual -OH from dehydroxylation of brucite, possibly producing a slight over-estimation of incorporated -OH into the chrysotile phase. This direct measurement was used to calculate the serpentinization extent (%) at a given reaction time as follows:

ξ t =((-OH) measured /(-OH) theoretical )*100 (2)
where (-OH) theoretical is the theoretical weigh (in %) of hydroxyl groups incorporated in chrysotile (400°C to 700°C) with a chemical formula simplified to Mg 3 Si 2 O 5 (OH) 4 for the (-OH) theoretical considered. Then, the serpetinization extent was correlated with reaction time (ξ t vs. t). These experimental-calculated data is displayed in figure 3. As previously stated, a complete serpentinization extent was determined after 30 days for smaller olivine grains (<30µm) and after 90 days for intermediate olivine grains (30<grain size<56). These results

clearly show that the serpentinization rate strongly depends on the starting grain size of olivine. This explains why for larger olivine grains (56<grain size<150µm), about 55% of serpertinization extent was only reached after 90 days of olivine-fluid interactions.

Experimental data reported in figure 4 were fitted by using a kinetic pseudo-secondorder model. This simple kinetic model describes a fast serpentinization step followed by a slow serpentinization step until an asymptotic maximum with time. Its integrated form can be expressed as follows:

(

) 3
where  t , is the serpentinization extent for a given reaction time t,  max , the maximum serpentinization extent (close to 100% for a complete serpentinization) and t 1/2 the half serpentinization time. The fast serpentinization step can be associated to the fast dissolution of smaller olivine grains initially far from equilibrium, but the dissolution process was spatially and temporally coupled to a fast precipitation of chrysotile and brucite. For this reason, the external shape of starting olivine grains (primary or parent mineral) was preserved, leading to a porous granular material composed of chrysotile and brucite minerals when complete mineral replacement of olivine was reached. Finally, the mineral replacement initial-rate v 0

(or serpentinization initial-rate) was defined as the slope of the tangent line when time t tends toward zero on the r vs t curve. Analytically, v 0 =(ξ max /t 1/2 ) and it varies from 3.6x10 -6 s -1 to 1.4x10 -7 s -1 respectively for <30µm grain size and 56-150µm grain size. Full serpentinization was not obtain experimentally on 56<particle size<150 µm but the theoretical model presented predict a close to complete serpentinization (>90%) around 2 years.

Indeed, the fluid/olivine interface depending of the initial olivine grain size is the main factor controlling the initial rate. These kinetic parameters concerning the three different size classes of olivine and respective correlation factors are summarized in table 2.

The uncertainties of the TG-method result from the calculation method. The main approximation is the systematic consideration of the same temperature range (400-700°C).

Refering to all the experiments, a variation of the temperature range of ± 50°C will only induce a difference of 1-5% for the final serpentinization advancement calculated. Based on this calculation we assure that the maximum uncertainty of the proposed methods is around 5% as reported in figure 4. The uncertainty on the calculated initial rate is directly depending on the standard deviation obtained for t 1/2 and ξ max (Table 2).

In a complementary way, the transmission FTIR spectra were obtained. Characteristic stretching bands for hydroxyl group (-OH) in chrysotile-brucite and for Si-O group in olivinechrysotile were used. Particularly, the relative (-OH)/(Si-O) ratio using integrated bands intensities or maximum band intensities was correlated with the serpentinization extent deduced from TG/DTG analyses (Fig. 5). This gives two calibration curves that can be used to determine serpentinization rate using FTIR measurements. However, FTIR measurements should be taken with caution because of the overlapping of -OH (for brucite and serpentine)

and Si-O groups (for serpentine and olivine). We could overcome this problem if serpentine/brucite produced molar ratio stayed constant following reaction time, but as described before it is not the case. Here, we conclude that the TG/DTG analyses are a powerful tool to determine the mineral replacement rate of olivine by chrysotile-brucite mineral assemblage. For this specific case, the FTIR measurements provide a first information about the olivine serpentinization extent.

This study confirms that the serpentinization rate is enhanced by high alkaline conditions. Serpentinisation rate has been studied for a large variety of experimental conditions under neutral conditions [START_REF] Allen | Compositional controls on vent fluids from ultramafichosted hydrothermal systems at mid-ocean ridges: An experimental study at 400°C, 500 bars[END_REF][START_REF] Macdonald | Rate of serpentinization in seafloor environments[END_REF][START_REF] Marcaillou | Mineralogical evidence for H2 degassing during serpentinization at 300 °C/300 bar[END_REF][START_REF] Martin | Some experimental and theoretical observations on the kinetics of hydration reactions with particular reference to serpentinization[END_REF][START_REF] Seyfried | Seawater-peridotite interaction at 300°C and 500 bars: implications for the origin of oceanic serpentinites[END_REF][START_REF] Seyfried | Redox evolution and mass transfer during serpentinization: An experimental and theoretical study at 200 °C, 500 bar with implications for ultramafic-hosted hydrothermal systems at Mid-Ocean Ridges[END_REF][START_REF] Wegner | Experimentally determined hydration and dehydration reaction rates in the system MgO-SiO2-H2O[END_REF][START_REF] Yada | Growth and microstructure of synthetic chrysotile[END_REF][START_REF] Bentabol | Hydrothermal synthesis (200°C) of Cokaolinite and Al-Co-serpentine[END_REF]. For comparison, serpentinization extent of 50-100 µm starting grain size at 200°C reached only ~20% after ~4 months under neutral conditions (Seyfried et al., 2007). This corresponds to a kinetic 5 times slower to our results on the largest starting grain size (56-150 µm).

Serpentinization steps and reaction mechanism

Contemporaneously, the first steps of reaction in alkaline medium are characterized by a fast dissolution of olivine associated to the formation of preferential dissolution figures as notches and etch pits (Fig. 6a,b,c) [START_REF] Normand | Hydrothermal alteration of olivine in a flow-through autoclave: Nucleation and growth of serpentine phases[END_REF][START_REF] Okamoto | Progress of hydration reactions in olivine-H2O and orthopyroxenite-H2O systems at 250 °C and vapor-saturated pressure[END_REF][START_REF] Bentabol | Hydrothermal synthesis (200°C) of Cokaolinite and Al-Co-serpentine[END_REF]. Conjointly, precipitation of the first nucleates of brucite and chrysotile occur at the olivine surface. FESEM observations have revealed the preservation of olivine shape after complete serpentinization (Fig. 7). This suggests that olivine alteration invokes coupled dissolution-precipitation processes [START_REF] Putnis | Mineral Replacement Reactions[END_REF]. Despite ultrasonic treatment and dispersion on ethanol (up to 1h30), which can easily break up the new brucite/chrysotile mineral assemblage, the shape and size of olivine grains are always preserved regardless the completion of the reaction. The few scattered chrysotile grains observed are the result of tearing from olivine grain surfaces and are not the result of precipitation from saturated solution away from olivine grain. Based on these results, we assume a higher super-saturation of solution with respect to chrysotile tubes at the olivinesolution interfaces. Supersaturation at olivine-alkaline solution interfaces allows rapid heterogeneous serpentine nucleation as small nodules of chrysotile and brucite (Fig. 2a). This nucleation phase is followed by a phase of epitaxial growth of chrysotile and brucite forming a porous medium (Fig. 6d,e,f). Chrysotile grows as elongated tubes with various morphology (conical, cylinder in cylinder) with a size depending on starting olivine grain size. Largest starting grain size induces smallest reacting surface and thus slower kinetic of alteration and formation of largest chrysotiles particles. Olivine grain size influenced initial dissolution rate v 0 , passivation state and general kinetic of alteration.

Serpentinization reaction is then favored by the formation of notches connected to a micro-fracturing network inside olivine (e.g. 32 days of reaction for >30 µm grains; Fig. 6b,c). This micro-fracturing network might start following ordered families of fine-scale fractures from olivine grains [START_REF] Normand | Hydrothermal alteration of olivine in a flow-through autoclave: Nucleation and growth of serpentine phases[END_REF]. In the oceanic crust, the microfracturing may be attributed to the stress generated by the volume increase during olivine serpentinization [START_REF] Putnis | Mineral Replacement Reactions[END_REF]. In our free fluid system, there is no evident expansion during olivine replacement. Volume increase due to olivine serpentinization (25%) is likely accounted by material loss in solution, but it could also cause the microfracturing [START_REF] Putnis | Mineral Replacement Reactions[END_REF][START_REF] Putnis | Fluid-induced processes: metasomatism and metamorphism[END_REF]. With the formation of smaller sub-grains, microfracturing allows an easier fluid percolation and increase the total reaction-surface (Fig. 6e,f). This process permits a continuous and total replacement of olivine by chrysotile and brucite as summarized in figure 8. This is in agreement with natural observation and development of mesh type texture described in natural rocks [START_REF] Wicks | Serpentine textures and serpentinization[END_REF][START_REF] Evans | The serpentinite multisystem revisited: Chrysotile is metastable[END_REF][START_REF] Putnis | Mineral Replacement Reactions[END_REF][START_REF] Putnis | Fluid-induced processes: metasomatism and metamorphism[END_REF][START_REF] Wicks | An idealized model for serpentine textures after olivine[END_REF][START_REF] Moody | Serpentinization: a review[END_REF]. Fluid can percolate everywhere without formation of a passivation layer at grain surface. The formation of a protective layer would induce a non-continuous passivation process by blocking intraparticles diffusion [START_REF] Montes-Hernandez | In situ kinetic measurements of gas-solid carbonation of Ca(OH)2 by using an infrared microscope coupled to a reaction cell[END_REF]. Mass transfer will play a major role for the preservation of volume and shape of starting olivine grain.

Conclusion

Olivine alteration was investigated under alkaline conditions for different starting grain sizes at 200 °C. In this study, we were able to follow complete olivine replacement by an assemblage of chrysotile and brucite.

Thermogravimetric analyses were used to investigate the dehydroxylation of hydrated phases and thus the serpentinization extent as a function of time. Based on this innovative approach, we were able to estimate punctually the serpentinization advancement and a kinetic pseudo-second-order model was used to describe experimental data. This could allow a prediction of reaction advancement for the largest starting grain size.

We also established two calibration curves between the -OH/Si-O bands measured in FTIR and the degree of serpentinization. This enables to have an estimation of the kinetic rates of serpentinization directly from the FTIR spectra analysis. This must be considered with caution because of the overlapping of -OH bands between brucite and serpentine.

Under our experimental conditions, olivine is replaced by chrysotile and brucite by coupled dissolution-precipitation processes. Fast dissolution of olivine, preferential dissolution features formation and process of grain subdivisions by fracturing are involved to explain a complete mineral replacement of olivine. This implies the preservation of external shape of olivine grains as typically observed in natural systems.

Figure Captions:

Table 1: Summary of the experimental conditions.

Table 2: Summary of kinetic parameters obtained from the pseudo-second-order model.

Figure 1 :

 1 Figure 1: XRD patterns following reaction advancement, a) with starting grain size <30µm, b) with starting grain size 30-56 µm, c) example of plot for the peak corresponding to bragg angle (2θ) of 12.1° and miller indice (002) with a gaussian deconvolution and plot of FWHM following reaction time for this peak. O: olivine, B: Brucite and S: serpentine.

Figure 2 :

 2 Figure 2: Scanning electron microscope imaging of the experimental products. All shown experiments have been performed at pH=13.5 (at 25°C) and 200°C, for <30 µm (a, b, c and e), 30-56 µm (d, f, g) and 56-150µm (h) grains size. a) chrysotile and brucite nodules after 3hours of reaction (run no.1), b) chrysotile tube after 30 days of reaction (run 8) and c)nodules aggregated in a tubular shape after 3 days of reaction (run no.5), d) chrysotiles "bunch" at olivine grain surface after 10 days of reaction (run no.13), e) characteristic brucite/chrysotile assemblage after 30 days of reaction (run no.6), f,g) characteristic brucite/chrysotile assemblage and thick cylinder-in cylinder chrysotile after 90 days of reaction (run no.18), and h) characteristic brucite/chrysotile assemblage after 32 days of reaction (run no.20). Bru: brucite, Ctl: chrysotile, Ol: olivine.

Figure 3 :

 3 Figure 3: a) Thermogravimetric analyses (TGA) for experiments of 3 hours to 30 days (run no. 1,3,5,6,7and 8) with fraction grains <30 µm, b) focus and decomposition of TGA and DTG corresponding spectra after 10 days of reaction.

Figure 4 :

 4 Figure 4: Serpentinization degree versus time for the hydration reaction at different grain sizes for T=200°C, P sat =1.6Mpa and fluid/solid=15. Maximum error bars corresponding to 5% of the serpentinization extent calculated was also reported. Data were fitted by using a kinetic pseudo-second-order model.

Figure 5 :

 5 Figure 5: a) Transmission spectra (in absorbance) for starting grain size <30µm after 3 hour

Figure 6 :

 6 Figure 6: Scanning electron microscope imaging of the experimental products for starting grain size <30 µm (a), 30-56 µm (c-f) and 56-150 µm (b). a) etch pits at olivine grain surface after 3 days (run no.5), b) dissolution notches after 32 days of reaction (run no. 20), c)dissolution notches after 24 days of reaction (run no. 14), d) chrysotile micro-tubes at olivine grain surface after 3 days of reaction (run no.12), e) contact between two olivine grains and f) microfracturing in section after 10 days of reaction (run no.13). Red dotted lines represent initial border of the supposed crack. Ctl: chrysotile, Ol: olivine.

Figure 7 :

 7 Figure 7: XRD pattern and corresponding scanning electron microphotography from pure starting San Carlos olivine to close to 100% of replacement by serpentine and brucite. Note the preservation of the olivine grains dimension and shape. S: serpentine, B: brucite, O: olivine.

Figure 8 :

 8 Figure 8: Schematic synthesis presenting the different steps of olivine replacement by chrysotile and brucite.

  Figure 1

Figure 8 582

 8 Figure 8

Table 1 556

 1 RunAll experiments have been performed at pH 13.5 (measured at 25°C). Saturated pressure is 557 constant: 1.6MPa for 200°C and 0.5 MPa for 150°C reactions. Fluid/rock ratio is always ~15.

	no.	T (°C)	Time	grain size (µm)	Olivine to Chrysotile conversion (%)	products starting-material
	1	200	3 h	<30 µm	10.3	O>C>B
	2	200	16 h	<30 µm	21.7	O>C>B
	3	200	24 h	<30 µm	24.6	O>C>B
	4	200	48 h	<30 µm	37.5	O>C>B
	5	200	72 h	<30 µm	51.7	O≈C>B
	6	200	10 day	<30 µm	73.8	C>O>B
	7	200	20 day	<30 µm	88.8	C>B>O
	8	200	30 day	<30 µm	98.0	C>B
	9	200	90 day	<30 µm	98.2	C>B
	10	150	30 day	<30 µm	49.5	O≈C>B
	11	150	66 day	<30 µm	not determined	C>O>B
	12	200	3day	30-56 µm	19.6	O>C>B
	13	200	10 day	30-56 µm	26.2	O>C>B
	14	200	24 day	30-56 µm	46.2	O≈C>B
	15	200	41 day	30-56 µm	77.1	C>O>B
	16	200	51 day	30-56 µm	71.1	C>O>B
	17	200	72 day	30-56 µm	88.9	C>B>O
	18	200	90 day	30-56 µm	94.4	C>B>O
	19	200	13 day	56-150 µm	10.7	O>C>B
	20	200	32 day	56-150 µm	26.6	O>C>B
	21	200	60 day	56-150 µm	44.2	O>C>B
	22	200	90 day	56-150 µm	55.4	C>O>B

558

O: olivine, C: chrysotile, B: brucite. 559

Table 2

 2

	Initial particule size of olivine	Exp.	Smax (%) Calc.	t ½ (days)	Initial rate (1/s)	fitting r²
	<30 µm	97.96	100±1.7	3.2±0.3	3.62-06±0.35E-06	0.989
	30-56 µm	94.35	100±8.5	23.1±5.3	5.01E-07±0.9E-07	0.947
	56-150 µm	55.4	100±16	79±21	1.46E-07±0.2E-07	0.981

Acknowleggements

The authors are grateful to French National Center for Scientific Research (CNRS and University Joseph Fourier (UJF) in Grenoble for providing the financial support. R. Lafay was supported by a Ph.D grant from French education ministry. The authors are grateful to IPAG institute where infrared measurements where performed.