Michèle Sebag

Riad Akrour

Basile Mayeur

Marc Schoenauer

Anti Imitation-based Policy Learning

), aims at a pseudo-value function such that it induces the same order on the state space as a (nearly optimal) value function. By construction, the greedification of such a pseudo-value induces the same policy as the value function itself. The approach assumes that, thanks to prior knowledge, not-to-be-imitated demonstrations can easily be generated. For instance, applying a random policy on a good initial state (e.g., a bicycle in equilibrium) will on average lead to visit states with decreasing values (the bicycle ultimately falls down). Such a demonstration, that is, a sequence of states with decreasing values, is used along a standard learning-to-rank approach to define a pseudo-value function. If the model of the environment is known, this pseudo-value directly induces a policy by greedification. Otherwise, the bad demonstrations are exploited together with off-policy learning to learn a pseudo-Q-value function and likewise thence derive a policy by greedification. To our best knowledge the use of bad demonstrations to achieve policy learning is original. The theoretical analysis shows that the loss of optimality of the pseudo value-based policy is bounded under mild assumptions, and the empirical validation of AIPoL on the mountain car, the bicycle and the swing-up pendulum problems demonstrates the simplicity and the merits of the approach.

Introduction

Reinforcement learning aims at building optimal policies by letting the agent interact with its environment [START_REF] Sutton | Introduction to Reinforcement Learning[END_REF][START_REF] Szepesvári | Algorithms for Reinforcement Learning[END_REF]. Among the signature challenges of RL are the facts that the agent must sufficiently explore its environment in order to ensure the optimality of its decisions, and that the consequences of its actions are delayed. Both facts raise severe scalability issues in large search spaces, which have been addressed in two ways in the last decade (section 2). One way relies on the human expert's support to speed up the discovery of relevant behaviors, ranging from inverse reinforcement learning [START_REF] Ng | Algorithms for Inverse Reinforcement Learning[END_REF][START_REF] Abbeel | Apprenticeship Learning and Reinforcement Learning with Application to Robotic Control[END_REF] and learning by imitation [START_REF] Schaal | Computational approaches to motor learning by imitation[END_REF][START_REF] Calinon | Active Teaching in Robot Programming by Demonstration[END_REF][START_REF] Konidaris | Constructing skill trees for reinforcement learning agents from demonstration trajectories[END_REF] to learning from the expert's feedback [START_REF] Wilson | A Bayesian Approach for Policy Learning from Trajectory Preference Queries[END_REF][START_REF] Jain | Learning Trajectory Preferences for Manipulators via Iterative Improvement[END_REF][START_REF] Akrour | Programming by Feedback[END_REF][START_REF] Loftin | Learning behaviors via human-delivered discrete feedback: modeling implicit feedback strategies to speed up learning[END_REF]. Another way relies on the extensive interaction of the agent with its environment; it mostly operates in simulated environments, where the agent can interact with the environment and tirelessly evaluate and improve its policy without suffering exploration hazards; following the pioneering TD-Gammon [START_REF] Tesauro | A parallel network that learns to play backgammon[END_REF], are the Monte-Carlo Tree Search approaches [START_REF] Kocsis | Bandit based monte-carlo planning[END_REF][START_REF] Gelly | Combining Online and Offline Knowledge in UCT[END_REF][START_REF] Auer | Logarithmic Online Regret Bounds for Undiscounted Reinforcement Learning[END_REF][START_REF] Filippi | Optimism in Reinforcement Learning and Kullback-Leibler Divergence[END_REF] and Deep Reinforcement Learning [START_REF] Mnih | Human-level control through deep reinforcement learning[END_REF].

Yet another approach is investigated in this paper, taking some inspiration from the Inverse Reinforcement Learning setting, although it almost entirely relaxes the expertise requirement on the human teacher. Specifically, the proposed approach referred to as Anti Imitation-based Policy Learning (AIPoL) is based on a weak prior knowledge: when in a good state, some trivial (random or constant) policies will on average tend to deteriorate the state value, and lead to a sequence of states with decreasing value. For instance, starting from the state where the bicycle is in equilibrium, a random policy will lead the bicycle to sooner or later fall down. This knowledge provides an operational methodology to tackle RL with very limited support from the human expert: the human expert is only asked to set the agent in a target state (e.g., the car on the top of the mountain or the bicycle in equilibrium); from this initial state, the agent applies a random policy, defining a trajectory. Contrasting with the IRL setting, this demonstration is a bad demonstration, showing something that should not be done. One merit of the approach is that it is usually much easier, and requires significantly less expertise, to generate a bad demonstration than a good one. However, such bad demonstrations provide an operational methodology to derive a good value function, as follows. Assuming that the sequence of states visited by the demonstration is such that the state value likely decreases along time (the bicycle falls down and the car arrives at the bottom of the slope), a value function can thus be derived on the state space along a learning-to-rank framework [START_REF] Joachims | A support vector method for multivariate performance measures[END_REF]. If the model of the environment is known, this value function directly defines a policy, enabling the agent to reach the target state. Otherwise, the bad demonstrations are exploited together with off-policy learning to build a Q-value function. The optimality loss of the resulting policy is bounded under mild assumptions (Section 3).

The empirical validation of the approach is conducted on three benchmark problems -the mountain car, the bicycle balancing and the swing-up pendulum problems -and the performances are compared to the state of the art (section 4). The paper concludes with a discussion about the limitations of the AIPoL approach, and some research perspectives.

Notations

In the rest of the paper the standard Markov decision process notations (S, A, p, r) are used: S and A respectively stand for the state and action spaces, p : S × A × S → IR is the transition model (when known), with p(s, a, s ) the probability of reaching state s after selecting action a in state s, and r : S → IR is the deterministic, bounded reward function. At the core of mainstream RL approaches are the value functions associated to every policy π. V π : S → IR, yields for each state the expected discounted cumulative reward gathered by following π from this state, with discount factor γ in [0, 1]. Likewise, Q-value Q π : S × A → IR associates to each state-action pair s, a the expected discounted cumulative reward Q π (s, a) gathered by selecting action a in state s and following policy π ever after.

V π (s) = r(s) + IE st∼p(st-1,π(st-1),•) [ t γ t r(s t )|s 0 = s] Q π (s, a) = r(s) + γ s p(s, a, s )V π (s ) (1)
While RL traditionally relies on learning value functions [START_REF] Sutton | Introduction to Reinforcement Learning[END_REF], their learning (using dynamic programming and approximate dynamic approaches [START_REF] Bertsekas | Dynamic Programming and Optimal Control[END_REF]) faces scalability issues w.r.t. the size of state and action spaces. 1 In the meanwhile, there is some debate about the relevance of learning value functions to achieve reinforcement learning, on the ground that solving an RL problem and defining a policy only requires to associate an action with each state. Associating a value with each state or each state-action pair thus requires more effort than needed to solve the problem. Along this line, direct policy search (DPS) (see [START_REF] Deisenroth | A survey on policy search for robotics[END_REF] for a comprehensive presentation) directly tackles the optimization of the policy. Furthermore, DPS does not need to rely on the Markovian assumption, thus making it possible to deal with a more agile description of the search space. DPS faces two main difficulties: i) the choice of the parametric representation, granted that the optimization landscape involves many local optima; ii) the optimization criterion, the policy return expectation, is approximated by an empirical estimate thereof, thus defining a noisy and expensive optimization problem.

Other RL trends addressing the limitations of learning either value functions or policies are based on the expert's help. In early RL, the human expert stayed behind the stage, providing a precious and hidden help through the design of the representation space and the reward function. In inverse reinforcement learning (IRL), the expert explicitly sets the learning dynamics through demonstrating a few expert trajectories, narrowing down the exploration in the vicinity of these trajectories [START_REF] Calinon | Active Teaching in Robot Programming by Demonstration[END_REF][START_REF] Abbeel | Apprenticeship Learning and Reinforcement Learning with Application to Robotic Control[END_REF][START_REF] Konidaris | Constructing skill trees for reinforcement learning agents from demonstration trajectories[END_REF][START_REF] Ross | Reinforcement and imitation learning via interactive noregret learning[END_REF]. In preference-based reinforcement learning, the expert is on the stage, interacting with the learning agent. Constrasting with IRL, preference-based RL does not require the human expert to be able to demonstrate a competent behavior; the expert is only assumed to be able to rank state-action pairs [START_REF] Knox | Training a robot via human feedback: A case study[END_REF][START_REF] Fürnkranz | Preference-based reinforcement learning: a formal framework and a policy iteration algorithm[END_REF], fragments of behaviors [START_REF] Wilson | A Bayesian Approach for Policy Learning from Trajectory Preference Queries[END_REF], or full-length trajectories [START_REF] Jain | Learning Trajectory Preferences for Manipulators via Iterative Improvement[END_REF][START_REF] Akrour | Programming by Feedback[END_REF] while the RL agent achieves active ranking, focusing on the generation of most informative pairs of state-actions, behaviors or trajectories. In summary, RL increasingly puts the human expert in the learning loop, and relaxes the expertise requirement; in counterpart, the RL agent becomes more and more autonomous, striving to ask more informative preference queries to the expert and to best exploit her input [START_REF] Loftin | Learning behaviors via human-delivered discrete feedback: modeling implicit feedback strategies to speed up learning[END_REF]. Supervised learning-based policy learning, pioneered by [START_REF] Lagoudakis | Least-squares policy iteration[END_REF], also increasingly relies on expert knowledge. In [START_REF] Langford | Relating reinforcement learning performance to classification performance[END_REF], a sequence of reward-sensitive classification problems is built for each time step, assuming that the optimal actions will be executed in the remaining steps (akin structured learning [START_REF] Chang | Learning to search better than your teacher[END_REF]). In [START_REF] Lazaric | Analysis of a classification-based policy iteration algorithm[END_REF], Direct Policy Iteration (DPI) handles cost-sensitive classification problems where the loss function is defined from the Q-regret of the current policy. Further work on DPI [START_REF] Chemali | Direct policy iteration with demonstrations[END_REF] use expert demonstrations. In [START_REF] Farahmand | Classificationbased approximate policy iteration[END_REF], the Classification-based Approximate Policy Iteration also relies on the estimation of the Q-value based on the current policy.

As these classification-based RL approaches involve loss functions related to the value regret, they rely on the estimation of the value function, which is computationally or expertise-wise demanding. Another limitation of classificationbased RL approaches is related to the ties, that is, the fact that there might be several optimal actions in a given state. A supervised learning approach addressing the tie issue is energy-based learning (EBL) [START_REF] Lecun | A tutorial on energybased learning[END_REF]: When aiming at finding a classifier h : X → Y, mapping an instance space X onto a (possibly structured) output space Y, the EBL claim is that in some cases, learning an energy function g : X × Y → IR, and defining h(x) as arg max y∈Y g(x, y) leads to significantly more robust results than learning directly h. An appealing argument for the EBL approach is that g is only defined up to a monotonous transformation. 2 Along these lines, RL might be content with learning an energy-like value function U (s, a), such that policy π U (s) = arg max a∈A U (s, a) is a (nearly) optimal policy, regardless of whether U satisfies the Bellman optimality equation. Next section will present a methodology for learning such an energy-based value function, however with limited help from the human expert.

Overview of AIPoL

Rationale

AIPoL is based on the assumption that, while quite some expertise is required to perform an expert demonstration, it is usually very easy to generate terrible demonstrations, in a sense defined below. Let V * be the (unknown) optimal value function, satisfying the Bellman equation for some 0 < γ ≤ 1:

V * (s) = r(s) + γ arg max a∈A s ∈S p(s, a, s )V * (s ) (2)
Definition 1. A counter-demonstration (CD), is a sequence of states (s 1 , . . . s T ) with decreasing V * values, i.e., s.t.

∀ 1 ≤ i < j ≤ T, V * (s i ) > V * (s j ) Definition 2. Let E = {CD 1 , . . . CD n } be a set of n CDs, with CD i = (s i,t , t = 1 . . . T i ). The learning-to-rank problem associated to E is defined from the set of constraints s i,t ≺ s i,t ∀i in [1..n] and ∀1 ≤ t < t ≤ T i . Find U = arg min U :S →I R {L(U, E) + R(U )} (3)
with L a ranking loss function and R(U ) a regularization term.

Following the learning-to-rank setting [START_REF] Joachims | A support vector method for multivariate performance measures[END_REF] and denoting (A) + = max(0, A), the ranking loss function used in AIPoL is the sum of the hinge loss between U (s i,t ) and U (s i,t ) over all pairs (t, t ) such that 1 ≤ t < t < T i , with i = 1 . . . n:

L(U, E) = n i=1 1≤t<t ≤Ti (U (s i,t ) + 1 -U (s i,t )) + (4)
A solution U of Pb (3) (solved using e.g., [START_REF] Joachims | A support vector method for multivariate performance measures[END_REF][START_REF] Li | Mcrank: Learning to rank using multiple classification and gradient boosting[END_REF]) is thereafter referred to as pseudo-value function. Of course, it is unlikely that pseudo-value U satisfies the Bellman optimality equation ( 2). Nevertheless, it will be seen that the optimality of the policy based on U can be assessed in some cases, when V * and U define sufficiently similar orderings on the state space.

AIPoL relies on the assumption that CDs can be easily generated without requiring any strong expertise. CDs are additionally required to sufficiently visit the state space, or the interesting regions of the state space. How much does sufficient mean will be empirically assessed in section 4.

AIPoL with a known transition model

In this section, the transition model is assumed to be known. In the case of a deterministic transition model, let s s,a denote the arrival state when selecting action a in state s. Definition 3. In the deterministic transition model case, the greedy policy based on U selects the action leading to the arrival state with maximal U value:

π Û (s) = arg max a∈A U (s s,a ) (5)
It immediately follows from this definition that:

Proposition 1. In the deterministic transition setting, if U derives the same order on the state space as the optimal value function V * , i.e.,

∀(s, s ) ∈ S, ( U (s) > U (s )) ⇔ (V * (s) > V * (s ))
then greedy policy π Û is an optimal policy.

In the case of a stochastic transition model, by slight abuse of notation let s s,a denote a state drawn after distribution p(s, a, •). Definition 4. In the stochastic transition model case, the greedy policy based on U selects the action leading to the maximal U value expectation:

π Û (s) = arg max a∈A IE p(s,a,•) U (s s,a ) (6)
Some assumptions on the regularity of the transition model, on V * and U are required to establish a result analogous to Proposition 1 in the stochastic case. The main assumption regards the sub-Gaussianity of the transition model. Note that this assumption does hold, of course, for Gaussian transition models, and also in robotic settings, where the distance between two consecutive states is bounded due to physical and mechanical constraints.

A guarantee on the π Û optimality can be obtained under the following assumptions:

Proposition 2. Assuming 1) a continuous optimal value function V * on S; 2) a pseudo-value U deriving the same order on the state space as V * ; 3) a β-sub-Gaussian transition model, that is,

∀t ∈ IR + , IP(||IEs s,a -s s,a || 2 > t) < 2e -βt 2 4) U being Lipschitz with constant M , that is, ∀s, s ∈ S, | U (s) -U (s )| < L||s -s || 2 5
) for all every s, there exists a margin between the best and the second best action after U , such that:

∀a = a = π Û (s), IE U (s s,a ) > IE U (s s,a ) + M (7)
Then, if 2L < M β, π Û is an optimal policy.

Proof. The idea of the proof is the following: Consider the average value IEV * (s s,a ), where the expectation is taken over p(s, a, •). By continuity of V * there exists a state noted s s,a,V in the neighborhood of IEs s,a such that V * (s s,a,V ) = IEV * (s s,a ). Likewise there exists a state s s,a ,V such that V * (s s,a ,V ) = IEV * (s s,a ). Let us assume by contradiction that optimal policy π * is such that π

* (s) = a = a. It follows that V * (s s,a ,V ) > V * (s s,a,V )
and therefore, as U and V * define same orderings on S,

U (s s,a ,V ) > U (s s,a,V ) (8)
Let us denote K(u) = ||s s,a ,V -s s,a ,u ||. For any ε > 0, we have

| U (s s,a ,V ) -IE u U (s s,a )| = IE u | U (s s,a ,V ) -U (s s,a ,u )| = IE K(u)<ε | U (s s,a ,V ) -U (s s,a ,u )| +IE K(u)>ε | U (s s,a ,V ) -U (s s,a ,u )| ≤ Lε + L ∞ ε t • 2e -βt 2 dt ( * ) ≤ Lε + L β e -βε 2 < L(ε + 1 β )
where (*) is derived using the Lipschitz property of U and the sub-Gaussian property of the transition model.

If L(ε + 1 β ) < M/2
, then from Eq. ( 8) it comes:

IE U (s s,a ) + M/2 ≥ U (s s,a ,V ) > U (s s,a,V ) ≥ IE U (s s,a ) -M/2
which contradicts the margin assumption (Eq. 7), hence the result.

Overall, in the known transition model case, AIPoL proceeds by generating the CDs, defining the associated ranking problem, finding a solution U thereof and building policy π Û by greedification of U (Alg. 1).

Algorithm 1 Model-based AIPoL

Input: E = {CD1, . . . CDn} U = arg min {L(U, E) + R(U )} (Pb (3)) with L(U, E) (from Eq. 4) and R(U ) an L2 regularization. Return: π Û (Eq. ( 5))

AIPoL with unknown transition model

When the transition model is unknown, a pseudo Q-value Q is built from the pseudo-value U learned from the CDs using off-policy learning. The intuition is that, given U and triplets (s 1 , a

G = {(s i , a i , s i ), i = 1 . . . m}
be a set of state-action-next-state triplets. The learning-to-rank problem associated to G is defined from the set of ranking constraints (s i , a i ) ≺ (s j , a j ) for all i, j such that U (s i ) < U (s j ).

Find Q = arg min

Q:S×A →I R {L(Q, G) + R(Q)} (9)
with L a loss function and R(Q) a regularization term.

In AIPoL, the ranking loss function is set to:

L(Q, G) = m i=1 m j=1 y ij (Q((s i , a i ) + 1 -Q(s j , a j )) + (10)
with y ij = 1 iff U (s i ) < U (s j ) and 0 otherwise. Definition 6. Letting Q be a pseudo Q-value function learned from Pb (9), policy π Q is defined as:

π Q(s) = arg max a∈A Q(s, a) (11)
Some more care must however be exercized in order to learn accurate pseudo Q-value functions. Notably, comparing two triplets (s 1 , a 1 , s 1 ) and (s 2 , a 2 , s 2 ) when s 1 and s 2 are too different does not yield any useful information. Typically, when U (s 1 ) U (s 2 ), it is likely that U (s 1 ) > U (s 2 ) and therefore the impact of actions a 1 and a 2 is very limited: in other words, the learned Q does not deliver any extra information compared to U . This drawback is addressed by filtering the constraints in Pb [START_REF] Deisenroth | A survey on policy search for robotics[END_REF] and requiring that the triplets used to learn Q be such that:

||s 1 -s 2 || 2 < η (12)
with η a hyper-parameter of the AIPoL algorithm (set to 10% or 1% of the state space diameter in the experiments). Empirically, another filter is used, based on the relative improvement brought by action a 1 in s 1 compared to action a 2 in s 2 . Specifically, the constraint (s 1 , a 1 ) (s 2 , a 2 ) is generated only if selecting action a 1 in s 1 and going to s 1 results in a higher value improvement than selecting action a 2 in s 2 and going to s 2 :

U (s 1 ) -U (s 1 ) > U (s 2 ) -U (s 2 ) (13)
Overall, the model-free AIPoL (Alg. 2) proceeds by solving the model-based problem (Alg. 1), using traces (s, a, s ) to build the learning-to-rank problem (9), finding a solution Q thereof and building policy π Q by greedification of Q.

Algorithm 2 Model-free AIPoL

Input: E = {CD1, . . . CDn} Input: G = {(si, ai, s i ), i = 1 . . . m} U = arg min {L(U, E) + R(U )} (Pb (3)) with L(U, E) (Eq. 4) and R(U ) an L2 regularization. Q = arg min {L(Q, G) + R(Q)}
(Pb ( 9)) with L(Q, G) (Eq. 10) and R(Q) an L2 regularization. Return: π Q(s) (Eq. 11)

Discussion

In the model-based setting, the quality of the AIPoL policy essentially depends on sufficiently many CDs to be generated with limited expertise, and on the coverage of the state space enforced by these CDs. In many benchmark problems, the goal is to reach a target state (the car on the mountain or the bicycle in equilibrium). In such cases, CDs can be generated by simply setting the starting state to the target state, and following a random or constant policy ever after. Such a trivial policy is likely to deviate from the good state region, and visit states with lower and lower values, thus producing a CD. Additionally, the CDs will sample the neighborhood of the target state; the pseudo value function U learned from these CDs will then provide a useful guidance toward the (usually narrow) good region. The intuition behind AIPoL is similar to that of TDgammon [START_REF] Tesauro | A parallel network that learns to play backgammon[END_REF]: the value function should steadily increase when reaching the desirable states, regardless of satisfying the Bellman equation.

In the known transition model case, under the assumption that the pseudo value U induces the same ordering on the state space as V * , policy π Û is optimal in the deterministic case (Proposition 1). Under additional assumptions on the regularity of the optimal value function V * , of U and on the transition noise, the optimality still holds in the stochastic transition case (Proposition 2). This is true even though no reward is involved in the definition of U .

In the unknown transition model case, the constraints used to learn Q introduce a systematic bias, except in the case where the reward function r is equal to 0 almost everywhere. Let us consider the deterministic case for simplicity. By definition,

Q * (s 1 , a 1 ) = r(s 1 ) + γV * (s 1 )
If the reward function is equal to 0 almost everywhere, then with high probability:

(V * (s 1 ) > V * (s 2 )) ⇔ (Q * (s 1 , a 1 ) > Q * (s 2 , a 2 ))
Then, if U induces the same ordering on the state space as V * , the constraints on Q derived from the traces are satisfied by Q * , and the learning-to-rank problem ( 9) is noiseless.

Otherwise, the difference between the instantaneous rewards r(s 1 ) and r(s 2 ) can potentially offset the difference of values between s 1 and s 2 , thus leading to generate noisy constraints. The generation of such noisy constraints is alleviated by the additional requirement on the constraints (Eq. 13), requiring the U value gap between s 1 and s 1 be larger than between s 2 and s 2 .

Overall, the main claim of the AIPoL approach is that generating CDs, though requiring much less expertise than that required to generate quasi expert behavior or asking the expert to repair or compare behaviors, can still yield reasonably competent policies. This claim will be examined experimentally in next section.

Experimental Validation

This section presents the experimental setting used for the empirical validation of AIPoL, before reporting and discussing the comparative results.

Experimental Setting

The AIPoL performance is assessed on three standard benchmark problems: The mountain car problem, using SARSA as baseline [START_REF] Sutton | Generalization in reinforcement learning: Successful examples using sparse coarse coding[END_REF]; The bicycle balancing problem, using preference-based reinforcement learning as baseline [START_REF] Wilson | A Bayesian Approach for Policy Learning from Trajectory Preference Queries[END_REF][START_REF] Akrour | Programming by Feedback[END_REF]; the under-actuated swing-up pendulum problem, using [START_REF] Guez | Bayes-Adaptive Simulation-based Search with Value Function Approximation[END_REF] as baseline. In all experiments, the pseudo-value U and Q functions are learned using Ranking-SVM with Gaussian kernel [START_REF] Joachims | A support vector method for multivariate performance measures[END_REF]. The hyper-parameters used for all three benchmark problems are summarized in Table 1.

The first goal of the experiments is to investigate how much knowledge is required to generate sufficiently informative CD, enabling AIPoL to yield stateof-art performances. This issue regards i) the starting state of an CD, ii) the controller used to generate an CD, iii) the number and length of the CDs. A second goal is to examine whether and to which extent the performances obtained in the model-free setting (transition model unknown) are degraded compared to the model-based setting. A third goal is to investigate the sensitivity of the AIPoL performance w.r.t. the algorithm hyper-parameters (Table 1), including: i) the number and length of the CDs; ii) the Ranking-SVM hyper-parameters C (weight of the data fitting term) and σ (Gaussian kernel width); iii) the AIPoL parameter η used to filter the ordering constraints used to learn Q (Eq. 12).

The mountain car

Following [START_REF] Sutton | Generalization in reinforcement learning: Successful examples using sparse coarse coding[END_REF], the mountain car problem involves a 2D state space (position, speed), and a discrete action space (backward, neutral position, forward). The friction coefficient ranges in [0, .02]. AIPoL is compared to the baseline SARSA with λ = .9, α = .05/10m, ε = 0, with 9 × 9 tile coding, with 100 episodes for learning, stopping an episode whenever a terminal state is reached, or after 1000 steps. AIPoL uses 1 CD of length 1000. In the unknown transition model case, the 500 constraints are generated from random trajectories where pairs (s, a) and (s a ) were selected subject to constraints (Eq. 12) and (Eq. 13) with proximity threshold η = 10%. The performances are excellent for both known (1 CD with length 1,000) and unknown transition model cases, with negligible runtime. Fig. 3.a depicts the CD in the 2D (position, speed) space, starting from the target state and selecting the neutral action for 1,000 time steps. The pseudo-value U function learned by AIPoL and the approximation of V * learned by SARSA in two representative runs are respectively displayed in Fig. 3.b and 3.c, showing that U is very smooth compared to that approximate value. Fig. 3.e and 3.f display the policy based on Q in the model-free case, and the optimal policy learned by SARSA, suggesting that the policy learned by AIPoL is much simpler than for SARSA. Fig. 3.d shows a typical trajectory based on the AIPoL policy in the model-free case.

The sensitivity analysis shows that the main parameter governing the AIPoL performance on the mountain car problem is the friction (Fig. 1). For low friction values, the dynamics is quasi reversible as there is no loss of energy; accordingly, letting the car fall down from the target state does not generate a sequence of states with decreasing value (the value of the state intuitively increases with its energy). In the low friction region (friction in [0, .05]), AIPoL is dominated by SARSA. For high friction values (> .02), the car engine lacks the required power to climb the hill and both approaches fail. For moderate friction values (in [.01, .02]), AIPoL significantly outperforms SARSA.

The bicycle balancing

Following [START_REF] Lagoudakis | Least-squares policy iteration[END_REF], the bicycle balancing problem involves a 4-dimensional state space (the angles of the handlebar and of the bicycle and the angular velocities), and a 3-action action space (do nothing, turn the handlebar left or right, lean the rider left or right). The goal is to maintain the bicycle in equilibrium for 30,000 time steps; note that a random controller starting from the equilibrium state (0, 0, 0, 0) leads the bicycle to fall after 200 steps on average.

Known transition model case

To assess the sensitivity of the approach w.r.t. the starting state, the CDs are generated using a random starting state and a random controller. The definition of the policy π Û (Eq. 5) is adapted to account for the fact that, due to the temporal discretization of the transition model [START_REF] Lagoudakis | Least-squares policy iteration[END_REF], the effect of action a t on the angle values is only visible in state s t+2 . Some lookahead is thus required to define the greedy policy π Û . Formally, the selected action is obtained by maximization of the value obtained after two time steps:

π Û (s) = argmax a∈A {max a ∈A IE U (s s s,a ,a )}
Given this definition, AIPoL only requires 20 CD of length 5 to learn a competent policy, keeping the bicycle in equilibrium for over 30,000 time steps with high probability (in all of the 100 runs, Fig. 2). In comparison, the state of the art requires a few dozen trajectories to be ranked by the expert (15 for [START_REF] Akrour | Programming by Feedback[END_REF] and 20 for [START_REF] Wilson | A Bayesian Approach for Policy Learning from Trajectory Preference Queries[END_REF]), the starting point of which is close to the equilibrium. With same starting point, AIPoL reaches the goal (keeping the bicycle in equilibrium 100 times out of 100 runs) with a single CD of length 5.

Unknown transition model case

The ordering constraints on the state-action pairs likewise take into account the temporal discretization and the delayed impact of the actions. Formally, from sequences (s 1 , a 1 , s 1 , a 1 , s 1 ) and (s 2 ,a 2 , s 2 , a 2 , s 2 ), constraint (s 1 , a 1 ) (s 2 , a 2 ) is generated if

U (s 1 ) -U (s 1 ) > U (s 2 ) -U (s 2 )
The proximity threshold is set to η = 1%. 5,000 constraints are required to achieve the same performance as in the model-based setting.

The under-actuated swing-up pendulum

Following [START_REF] Guez | Bayes-Adaptive Simulation-based Search with Value Function Approximation[END_REF], the swing-up pendulum involves a 2-dimensional state space (s = (θ, θ)) and a 3 action space. The pendulum has two equilibrium states, a stable one and an unstable one. The goal, starting from the stable state (bottom position) is to reach the unstable one (top position). The task is underactuated since the agent has a limited torque and must gain some momentum before achieving its swing-up. The task is stopped after 20s or when the agent successfully maintains the pendulum in an up-state (θ < π/4) for 3 consecutive time steps. Only the model-based setting has been considered for the pendulum problem, with a computational cost of 3 seconds.

On the pendulum problem, the sensitivity of the approach w.r.t. the Ranking-SVM hyper-parameters is displayed in Fig. 4. Two failure regions appear when learning the pseudo-value U from a single CD of length 1,000: if the kernel width is too small, there is no generalization and the pendulum does not reach the top. If the kernel width is too large, the accuracy is insufficient and the pendulum does not decrease its speed sufficiently early: it reaches the top and falls down on the other side. For good hyper-parameter settings (C = 1 and 1/σ 2 ranging in [1.7, 2.7]; or C and 1/σ 2 very small), the pendulum reaches the target state in 3 seconds and stays there. The AIPoL performance matches the state of the art [START_REF] Guez | Bayes-Adaptive Simulation-based Search with Value Function Approximation[END_REF], which relies on a continuous variant of the Bayes-adaptive planning, and achieves the goal (staying in an up-state for 3 seconds) after on average 10 seconds of interaction.

Discussion and Perspectives

The AIPoL approach to reinforcement learning has been presented together with an analytic and empirical study of its performances. Its main novelty is twofold compared to the state of the art. On the one hand, AIPoL learns a pseudo-value function and derives a policy by greedification; computationallywise, it tackles a much less complex problem than e.g., inverse reinforcement learning [START_REF] Abbeel | Apprenticeship Learning and Reinforcement Learning with Application to Robotic Control[END_REF][START_REF] Konidaris | Constructing skill trees for reinforcement learning agents from demonstration trajectories[END_REF] (learning a reward function and solving a complete RL problem) or preference-based RL [START_REF] Akrour | Programming by Feedback[END_REF] (learning a return value and solving a difficult optimization problem). In addition, AIPoL significantly relaxes the requirements on the human teacher. She is not required to perform (nearly) optimal demonstrations as in IRL, or to compare, and possibly repair, trajectories as in preference-based learning: she is only required to know what will go wrong.

In the mountain car and the pendulum problems, AIPoL uses informed CDs (starting in the target state). In the bicycle problem however, the CD sequences start in a random state. In this latter case, the pseudo value function coarsely leads to get away from state regions with low value: the inadequacy of the pseudo value in low value regions is (almost) harmless should the learning agent spend little or no time in these regions.

A first limitation of the AIPoL approach, illustrated on the bicycle problem, is when the effect of the selected actions is fully visible after a few time steps, that is, when the transition dynamics involves some latency. This latency occurs when some coordinates of action a t (e.g. the angular speed) make no difference on state s t+1 and only influence e.g. s t+ . In this case some look-ahead is required in the greedification process. The extra computational cost is in O(|A| ), exponential in the latency and in the size of the action set. Note that this phenomenon, distinct from the delayed rewards of the actions, only concerns the transition dynamics: An alternative could be to commit to an action for a sequence of timesteps, rather than just a single step [START_REF] Mnih | Human-level control through deep reinforcement learning[END_REF]. A second limitation of the approach is that the computational cost of building the Q-value function might be high (e.g. on the swing-up pendulum) as it scales up quadratically with the number of ranking constraints. Other ranking approaches with linear learning complexity will be considered (e.g., based on neural nets [START_REF] Severyn | Learning to rank short text pairs with convolutional deep neural networks[END_REF] or ranking forests [START_REF] Clémençon | Ranking forests[END_REF]) to address this limitation. A third and most important limitation concerns the non-reversible MDP case, where the transition from s to s might take much longer than from s to s. Further work is on-going to address the non reversible case. A main theoretical perspective is to investigate the quality of the AIPoL policy in the unknown transition model case, depending on the structure of the MDP dynamics and the sparsity of the reward function.

Fig. 1 .

 1 Fig. 1. Mountain car: Number of time steps to reach the goal for AIPoL (solid blue line) and SARSA (dashed red line) vs friction value (average and standard deviation over 20 runs)

Fig. 2 .

 2 Fig. 2. Bicycle (model-based setting): Fraction of success of AIPoL w.r.t. number and length of CDs.

Fig. 3 .

 3 Fig. 3. The mountain car problem: Comparative evaluation of AIPoL and SARSA in the model-free setting, on two representative runs (friction = .01). The policy map visually displays the selected action for each state in the 2D (position, speed) space (best seen in color: red= forward, blue= backward, green= neutral).

Fig. 4 .

 4 Fig. 4. The pendulum problem: Sensitivity of AIPoL performance (average over 10 runs) w.r.t Ranking-SVM hyper-parameters C and 1/σ 2 (see text for details).

  1 , s 1 ) and (s 2 , a 2 , s 2 ), the pseudo Q-value of state-action pair (s 1 , a 1 ) is lower than for state action pair (s 2 , a 2 ) if state s 1 has a lower pseudo-value than s 2 ( U (s 1 ) < U (s 2 )).

Definition 5. With the same notations as above, let U be a pseudo value function solution of Pb (3), and let

Table 1 .

 1 AIPoL hyper parameters on the three benchmark problems: number and length of CDs, starting state and controllers used to generate the CDs; hyper parameters used to learn pseudo-value U (parameters C1 and 1/σ 2 1 ; hyper-parameters used to learn pseudo value Q (parameters C2 and 1/σ 2 2 ; # of constraints).

			Mountain car Bicycle Pendulum
	CD	number	1	20	1
		length	1,000	5	1,000
		starting state	target st random target st.
		controller	neutral	random neutral
	U	C1	10 3	10 3	10 -5
		1/σ 2 1	10 -3	10 -3	.5
	Q	nb const	500	5,000	-
		C2	10 3	10 3	-
		1/σ 2 2	10 -3	10 -3	-

A most appealing approach sidestepping these scalability issues, Deep Reinforcement Learning (see, e.g.,[START_REF] Mnih | Human-level control through deep reinforcement learning[END_REF]) requires intensive interactions between the learning agent and the environment. It is outside the scope of this paper.

For any non-decreasing scalar function f , g and f • g define the same classifier.

Acknowledgments

We wish to thank the anonymous reviewers for their insightful comments, which helped to greatly improve the paper.


Frédéric Danièle Beauquier
email: beauquier@univ-paris12.fr

Frédéric Gauche
email: gauche@univ-paris12.fr

How to Guarantee Secrecy for Cryptographic Protocols

Keywords: Security protocols, secrecy, cryptographic protocols

In this paper we propose a general definition of secrecy for cryptographic protocols in the Dolev-Yao model. We give a sufficient condition ensuring secrecy for protocols where rules have encryption depth at most two, that is satisfied by almost all practical protocols. The only allowed primitives in the class of protocols we consider are pairing and encryption with atomic keys. Moreover, we describe an algorithm of practical interest which transforms a cryptographic protocol into a secure one from the point of view of secrecy, without changing its original goal with respect to secrecy of nonces and keys, provided the protocol satisfies some conditions. These conditions are not very restrictive and are satisfied for most practical protocols.

Introduction

Cryptographic protocols are used to ensure secure communications between two or more parties in a distributed system. Among the requirements that cryptographic protocols must satisfy are the well-known authentication and secrecy or confidentiality.

Security protocol design and verification is a very hard problem. Sources of difficulty are numerous and of different types. The seminal paper for developing a model was proposed by D. Dolev and A.C. Yao. [DY83]. In recent years a lot of methods have been proposed for reasoning about cryptographic protocols. Some of them are based on the trace model [Pau98,JG02] including models with an explicit state-transition system [CDL + 99] or Horn clauses [Bla01,CCM01]. Another type of model uses processes to represent cryptographic protocols [AG00,Sch97].

Concerning secrecy there are basically two approaches, the first one reduces the secrecy property to a reachability problem, the second one defines secrecy in terms of an observability equivalence.

Most of the papers are devoted to decidability and undecidability results depending on various hypothesis related to the boundedness of nonces and sessions, the used cryptographic primitives and so on. See for example [DLMS04] for a review of these results. Surprisingly, there are very few results that give some rules to apply in order to guarantee the secrecy property. This question has already been answered in the case of cryptographic protocols using symmetric keys in [Bea04], which gives a sufficient condition for solving this problem. Here we consider a more general class of cryptographic protocols using both symmetric and asymmetric keys. We give a new sufficient condition adapted to this type of protocols and we describe an algorithm of practical interest. It transforms a cryptographic protocol (satisfying a condition which is not very restrictive) into a secure one from the point of view of secrecy, without changing its original goal with respect to secrecy of nonces and keys. In Section 2 we describe the model. Section 3 gives the sufficient condition for a secure protocol w.r.t secrecy, Section 4 is devoted to the algorithm which transforms a cryptographic protocol into a secure one w.r.t secrecy. The last section concludes. Related work As mentioned before, the security literature concentrates more on the verification of cryptographic protocols comparing to the synthesis of correct protocols. In [AN96], some prudent principles for designing protocols are given but do not guarantee the success. Several of these principles are present in our definition of well composed protocol. A sufficient condition based on typing is presented in [Aba99] but it concerns only symmetric keys and a binary view of secrecy according to which the world is divided into system and attacker. Our sufficient condition can be considered as a generalization of the sufficient condition given in [Low95]. Indeed, the protocols which are considered in this paper do not admit forwarding, which is an important restriction. At last, to our knowledge, there is no paper which describes an algorithm which transforms a protocol into a secure one w.r.t. secrecy and preserves its original goal.

The model

In this section we formalize the model we use and we specify the assumptions we make about protocols commonly referred to as the "Dolev-Yao model". Our approach is largely inspired by [Low99]. The only primitives used are pairing and encryption. We assume that pairing is associative, which corresponds to practical protocols, so the algebra of terms is the quotient of a free algebra with equations for associativity.

We are interested in the behavior of the protocol when the number of agents, nonces and sessions is unbounded. Moreover the hypothesis on the power of honest agents is as weak as possible. The knowledge of an agent is local, it does not have a global memory of all its sessions. On the contrary the power of the intruder is maximal.

Messages

Atomic values

The set Value is a set of disjoint types Agent, Nonce, Key, Cypher. Agent, Nonce, Key are sets of atomic values. Cypher is the set of values obtained by encryption. The set Agent is the set of all agent identities. It is partitioned into two subsets, honest agents and intruders: Agent = Honest ∪ Dishonest. W.l.o.g. one supposes that the set Dishonest contains a unique intruder I. Agents variables, named A, B, ..., belong to the set AgVar. Nonce is an infinite set of integers. Nonce variables named N, Na, Nb, ... , belong to the set NVar. The set Key is divided into two disjoint subsets ShKey and LKey.

-ShKey is the set of short term keys. Its elements correspond to symmetric keys used only for the current session.

-LKey is the set of long term keys. It is a disjoint union of SymKey the set of symmetric keys and AsymKey the set of asymmetric keys. The set AsymKey is a disjoint union of two subsets PubKey (public keys) and PrivKey (private keys). Short term key variables named K, K ′ , ... belong to the set KVar. Let A, B be two agent variables. We denote respectively by K priv (A), K pub (A), K(A, B), the long term private encryption key of A, the long term public encryption key of A, the long term symmetric key shared by agents A and B. Notice that in this notation K priv (A), K pub (A) are both encryption keys, and K pub (A) is NOT the inverse key of K priv (A) and vice-versa.

Symbolic terms. Symbolic terms are constructed using pairing and encryption. The pairing of terms X and Y is the term < X , Y >, the encryption of term X using the key K is {X } K , C is a set of constants. The grammar used to generate symbolic terms is : The pairing is associative, or equivalently for each n we have a primitive for n-pairing. We will consider only terms which are in a "canonical form". For example the canonical form of terms < t 1 , < t 2 , t 3 >> and << t 1 , t 2 >, t 3 > is < t 1 , t 2 , t 3 >, it means that < t 1 , < t 2 , t 3 >> and < t 1 , t 2 , t 3 > must be considered as triples and not pairs.

The set of subterms of a term τ is denoted Sub(τ ).

Concrete terms. Concrete terms are generated following the same grammar as for symbolic terms, except that variables in N V ar, KV ar, AgV ar are replaced by the values of the corresponding type.

Key ::= ShKey | K pub (Agent) | K priv (Agent) | K(Agent, Agent) conc term ::= N once | Agent | Key |< conc term, conc term >| {conc term} Key
Synthesis and Analysis. In this subsection, 'term' means 'symbolic term'. The synthesis procedure represents terms the agents can build. The analysis procedure represents terms the agents can learn.

Let T be a set of terms and A be an agent variable. The set Synth A (T ) is the least set of terms containing T and satisfying:

τ 1 , ..., τ p ∈ Synth A (T ) ⇒< τ 1 , ..., τ p >∈ Synth A (T ) (An agent can compose the terms he knows). -∀τ ∈ Synth A (T ), ∀B ∈ AgV ar

• {τ } K(A,B) ∈ Synth A (T ) (An agent can encrypt with a symmetric key he shares with another agent) • {τ } Kpriv(A) ∈ Synth A (T ) (An agent can encrypt with his own private key). • {τ } K pub (B) ∈ Synth A (T ) (An agent can encrypt with the public key of any agent). -∀τ ∈ Synth A (T ) and for all short term key variable K ∈ T , {τ } K ∈ Synth A (T ) (An agent can encrypt with all encrypting short term key he knows).

Let A be an agent variable. Let T and T ′ be two sets of terms. We have T Anal A T ′ if one of the following properties holds:

-< τ 1 , ..., τ p >∈ T , p > 1 and T ′ = (T \ {< τ 1 , ..., τ p >}) ∪ {τ 1 } ∪ ... ∪ {τ p } (An agent can decompose terms). -{τ } K ∈ T , K ∈ T is a symmetric session key variable, and T ′ = (T \ {τ } K ) ∪ {τ } (An agent can decrypt terms encrypted with a short term session key he knows).

-{τ } K(A,B) ∈ T , B ∈ T and T ′ = (T \{τ } K(A,B) )∪{τ } (An agent can decrypt
terms encrypted with a key shared with an agent he knows.) -{τ } K pub (A) ∈ T and T ′ = (T \{τ } K pub (A) )∪{τ } (An agent can decrypt terms encrypted with his own public key). -{τ } Kpriv(B) ∈ T , B ∈ T and T ′ = (T \ {τ } Kpriv (B) ) ∪ {τ } (An agent can decrypt terms encrypted with the private key of an agent he knows).

A set of terms T is told undecomposable if there does not exist any set of term T ′ such that T Anal A T ′ (An agent cannot decompose any more term). It is easy to prove that for any set of terms T , there exists a unique undecomposable set of terms T ′ such that T Anal * A T ′ . This set is denoted Anal * A (T ).

For a term τ ∈ Anal * A (T ) we define the number of steps necessary for A to learn τ from T as the number of decryption operations that A must use before obtaining τ , more precisely :

-A learns τ from T in 0 step iff some term < ..., τ, ... > is in T ( we admit here a composition of a single element τ ). (No decryption necessary). -if A learns {< ..., τ, ... >} K from T in at most p steps and K is a short session symmetric key learnt by A from T in at most q steps, then τ is learnt by A from T in at most p + q + 1 steps. -if A learns {< ..., τ, ... >} K(A,B) from T in at most p steps and B is learnt by A from T in at most q steps, then τ is learnt by A from T in at most p + q + 1 steps.

-if A learns {< ..., τ, ... >} K pub (A) from T in at most p steps then τ is learnt by A from T in at most p + 1 steps. -if A learns {< ..., τ, ... >} Kpriv(B) from T in at most p steps and B is learnt by A from T in at most q steps, then τ is learnt by A from T in at most p + q + 1 steps.

For τ, τ ′ ∈ Anal * A (T ) we define that A learns τ from T before τ ′ if A learns τ in p steps, τ ′ in p ′ steps and p < p ′ . Now, given a concrete agent a, we can define in the same way a relation Anal a on finite sets of concrete terms as well as the other notions defined above, replacing agents, and keys variables by values of the corresponding type.

Message ( Component, Protocol) -Template A component template is either a variable or an encrypted term. A message template or t-message is a tuple of the form (A, B, τ ) where A and B are distinct variables of agents representing respectively the sender and the receiver and τ is a term representing the content of the message. A concrete message is a tuple (a, b, m) where a and b are agent values and m is a concrete term. It corresponds to the informal usual notation A → B : m. A protocol template or simply protocol is a sequence of message templates. A role in a protocol template is an agent variable appearing in this protocol. Given a protocol P with a set of roles R, a session template Ses A for role A ∈ R is the subsequence of message templates of P in which role A is sender or receiver.

Our running example will be the protocol TMN [TMN90] using asymmetric keys. Brackets for pairing are omitted as usual.

Example 1. . 01 -A → S : B, {K a } K pub (S) 02 -S → B : B, A 03 -B → S : A, {K b } K pub (S) 04 -S → A : B, {K b } Ka
Ses S is the entire protocol. Ses A is the sequence:

A → S : B, {K a } K pub (S) S → A : B, {K b } Ka

Realizable protocol template

An elementary question is whether a protocol is "realizable", i.e. whether the honest agents can execute it. This notion appears in [RS03] as "well-formed" protocol. We formalize this notion in our framework and give an algorithm which checks whether a protocol is realizable or not. One can observe that as far as we are aware of, most of the undecidability proofs [DLMS99,AC02a,AC02b] are based on protocols which are not realizable, which is a weakness of these proofs. Only in [CCM01] the undecidability proof relies on realizable protocols. Let P be a protocol, and A be a role of this protocol. Consider the sequence of t-messages of the session template Ses A . The j th t-message of Ses A is of form (A, B j , τ j ) or (B j , A, τ j ) depending on A is sender or receiver of the message. We define Kn A,j as the knowledge of role A after execution of message number j. That is to say as the set of terms known by A after the execution of the first j t-messages of his session and that A can no more decompose. This knowledge can be decomposed into two subsets:

-The basic knowledge of A at step j, BasKn A,j , which contains agent, nonce and key variables. -The cryptographic knowledge of A at step j, CrKn A,j , which contains the encrypted terms known by A at step j and he cannot decrypt.

Notice that Kn A,j contains only terms which are component templates.

From the definition of synthesis, we can define Synth A (Kn A,j ) as the set of terms that A can build from his knowledge at step j.

Let us define by induction on j the set Kn A,j and the fact that the j first messages of Ses A are realizable.

The initial knowledge of A, Kn A,0 is fixed by the protocol. We need to introduce the notion of new variables appearing in a t-message of protocol P . Let (A p , B p , τ p ) be the p th t-message of P . The set of new variables of this t-message denoted N ewV ar p is defined recursively:

N ewV ar 1 = Sub(τ 1 ) ∩ (AgV ar ∪ N V ar ∪ KV ar). N ewV ar p = Sub(τ p )∩(AgV ar ∪N V ar ∪KV ar)\ (N ewV ar 1 ∪...∪N ewV ar p-1 )
for p> 1. Let j > 0 and suppose that the first (j -1) messages are realizable by A and Kn A,j-1 is defined, then:

-If in message number j, A is receiver, this message can be realized by A since A is passive in this action.

-If message number j is of the form (A, B j , τ j ), this message can be realized by A if and only if: τ j ∈ Synth A (Kn A,j-1 ∪ N ewV ar pj ) where p j is the index of the message (A, B j , τ j ) in P .

In both cases, we have : Kn A,j = {B j } ∪ Anal * A ({τ j } ∪ Kn A,j-1 ). A session template Ses A is realizable if all its t-messages in this session are realizable by role A. A protocol is realizable if all the session templates of all roles of the protocol are realizable. Clearly, the above procedure is effective so one can decide whether a protocol is realizable. For example on the TMN protocol with public key of the server, the evolution of the knowledge for each role is :

By now, we will consider only realizable protocols.

States. Transitions

We formulate now the semantics of a protocol as an infinite transition system where a state contains the set of current partial sessions of agents (it is actually

A B S Initial S, K pub (S) S, K pub (S) Step 1 B, Ka A, B, Ka Step 2 A Step 3 K b K b Step 4 K b
a multiset because the same agent may have several "identical" partial sessions at the same time) and a transition corresponds to a send or a receive event. As in [Low95] we assume that every message is intercepted by the intruder, so w.l.o.g. one consider that every sent message is sent to the intruder, and every received message is received from the intruder, so we have two types of events the send and receive ones.

States A valuation v of a set of component template T is a function that associates to each term τ ∈ T a concrete term τ = v(τ ), the value of which is in V alue (i.e. to each component template is associated its value). We consider here constants as variables for which the valuation is fixed. Let (τ j ) j=1,...,k be the list of contents of the t-messages of the session of a role A for a protocol P . Let v j be a valuation for Kn A,j . We denote τ j [v j ] the concrete term we obtain when substituting in term τ j to each maximal subterm τ ′ which is in Kn A,j the value v j (τ ′ ). One can remark that τ j is built in a unique way from its maximal subterms which are in Kn A,j .

A partial session (or simply session) σ is determined by its length l, a role A and a valuation v l (A) for the knowledge Kn A,l . The role of session σ will be denoted R σ . The role A, the length l and the valuation v l permit to define the list of the l first messages received by the agent playing this role in this session.

It is the list of concrete messages (τ j [v]) j=1,...,p≤k , where (τ j ) j=1,...,k is the list of the t-messages of the session of role A.

A state is a multiset of partial sessions like in [CDL + 99].

Transitions The formalization of the evolution of the state of the system via receive or send events is the most delicate part of the modeling. An admissible state is a state reachable from the initial state using transitions labeled by the following events:

- -→ S ′ if the following conditions are satisfied:

1. a, b ∈ Agent. 2. There exists in S a partial session σ = (A, v l ) of length l for which the next message is a send event or agent a starts a partial session for a role A in which the first message of Ses A is a message sent by A.

3. (a, b, m) = τ l+1 [v l+1
] where v l+1 is a valuation defined as follows:

(a

) (v l+1 | BasKn Rσ,l ) = (v l | BasKn Rσ,l ) (b) v l+1 | (BasKn Rσ,l+1 \ BasKn Rσ,l
) must satisfy the rules -The values are of the correct type, i.e. values for nonces, agents and short term keys belong to the respective sets respectively N once, Agent, Key.

-The valuation is injective on the set of nonces and the set of keys, and values are "fresh", i.e., if X is a variable for a nonce (resp. a key) belonging to BasKn Rσ,l+1 \ BasKn Rσ,l , then v l+1 (X) is not in the set of valuations of nonce variables (resp. key variables) for all the partial sessions of state S.

-CrKn Rσ ,l+1 = CrKn Rσ ,l and for coherence (

v l+1 | CrKn Rσ ,l+1 ) = (v l | CrKn Rσ,l+1
). 4. S ′ is the state we obtain when replacing one exemplary of session σ = (l, A, v l ) by σ ′ = (l + 1, A, v l+1 ). (It corresponds to increasing the list of concrete messages of the partial session σ with the concrete message (a, b, m)).

The knowledge of the intruder I at state S ′ is :

IntrKn S ′ = Anal * I (IntrKn S ∪ {(a, b, m)}) • Receive transitions
We consider here only the receive events where the message is accepted by the receiver. We have a transition from state S to state S ′ labeled by the receive event (a, ← , (a, b, m)), denoted by S (a,←,(b,a,m))

-→ S ′ if the following conditions are satisfied:

1. a, b ∈ Agent. 2. There exists in S a partial session σ = (l, A, v l ) for which the next message is a receive event, or (case l = 0) agent a starts a partial session for a role A in which the first message of Ses A is a message received by A.

3. (b, a, m) = τ l+1 [v l+1
] where v l+1 is a valuation defined as follows:

(a)

v l+1 | BasKn Rσ,l = v l | BasKn Rσ,l (b) v l+1 | (BasKn Rσ,l+1 \ BasKn Rσ,l
) must satisfy the rules -values belong to the set Synth I (S) defined above.

-values of agent variables belong to Agent.

(c) v l+1 | (CrKn Rσ ,l+1 ∩ CrKn Rσ ,l ) = v l | (CrKn Rσ ,l+1 ∩ CrKn Rσ ,l ). (d) v l+1 | (CrKn Rσ ,l+1 \ CrKn Rσ ,l
) has values in Synth I (S). 4. S ′ is the state we obtain when replacing an exemplary of partial session σ with σ ′ = (l + 1, A, v l+1 ). (It corresponds to increasing the list of concrete messages of the partial session σ with the concrete message (b, a, m).

The knowledge of the intruder I at state S ′ is :

IntrKn S ′ = Anal * I (IntrKn S ∪ {m})
The set Synth I (S) is the set of concrete terms that the intruder can build at state S. It is the least set containing IntrKn S and satisfying:

τ 1 , ..., τ p ∈ Synth I (S) ⇒< τ 1 , ..., τ p >∈ Synth I (S).

-Agent ⊂ Synth I (S).

-For every agent a, the long term key K(a, I) is in Synth I (S).

-For every agent a, the long term key K pub (a) is in Synth I (S).

-For every term τ ∈ Synth I (S) and for every key K ∈ (IntrKn S ∩ Key), {τ } K ∈ Synth I (S).

A trace of a protocol is a sequence S 0

e1 -→ S 1 e2 -→ ...S n-1 en -→ S n
where S 0 is the initial state and each S i-1 ei -→ S i is a transition. The initial knowledge of the intruder IntrKn S0 is given by the protocol.

Remark. One can notice that the rules applied by an honest agent in order to accept a message correspond to a very weak control of the message. The agent makes only equality tests, it has no possibility to control for example the depth of encryption, the correct type of values and so on.

Secrecy

In the literature, generally the definitions of secrecy are very dependent on the chosen model and restrictive, i.e. sufficient for the hypothesis made by the authors but not applicable in a more general context. The definition we give here seems very general, at least as far as the concern is the secrecy of values and not of properties.

Definition 1. The secret of a variable X for a nonce or a short term key can be broken from the point of view of A if there exists a reachable state S containing a partial session σ of length l for role A with valuation v l for Kn A,l such that 1. BasKn A,l contains X and the set R of roles of the protocol 2. I does not belong to the valuation v l (R) (I does not participate to the partial session σ from the point of view of A) 3. v l (X) ∈ IntrKn S .

As one can observe, the notion of secrecy implies two parameters: a variable for which the secret is broken and a role which can claim the fact. We have to justify points 1 and 2. Why should the set R be in BasKn A,l ? Because as far as the agent involved in the partial session σ does not know all its partners in this session, it cannot claim whether it is correct that the agent I knows the value v l (X). Indeed, if I participates in an honest way to the session it is normal that v l (X) ∈ IntrKn S . For the same reason the condition that I does not belong to the valuation v l (R) is required. An unsolved question is how to define secrecy in the case when the set of roles does not belong to the knowledge of each role at the end of its partial session. There is a well-known attack [LR97] on the protocol TMN of Example 1. An intruder I A acts as if it was A:

01 -I a → S :< b, {K i } K pub (S) > 02 -S → b :< a, b > 03 -b → S :< a, {K b } K pub (S) > 04 -S → I a :< B, {K b } Ki >
In this attack, the secret is broken for the variable K b from the point of view of B because the trace given here reaches a state containing a partial session for role B satisfying the above three conditions. Given a protocol, the variables which can be learnt by an external observer of the protocol are called revealed variables. The others (those which remain unaccessible to this observer) are called unrevealed variables. More precisely, given a protocol P = (A i , B i , M i ) i=1,...,k , a variable X for a nonce or a key is revealed in P if X ∈ Anal * C ({M 1 , ..., M k }) for some C not being a role of P . The set of revealed variables of a protocol is clearly computable. In an obvious way, the secret can be broken for every revealed variable from the point of view of every role. Thus, the interesting question is "can the secret be broken for an unrevealed variable". The next section answers to this question by giving a sufficient condition which guarantees that the protocol preserves the secrecy of unrevealed variables for nonces and short term key variables.

A sufficient condition for secrecy

Well-Composed Protocol

A signature of a protocol is constituted by a nonce variable which is called the session nonce and a fixed list of the agent roles < n, A 1 , ..., A p >. Definition 2. A protocol is well composed if :

1. Encryption is of depth at most two. 2. Private long term asymmetric and long term symmetric keys are never transmitted. 3. There exists a signature S such that -the content of every t-message is a term of the form : < S, {S, m} Kpriv(A) > where A is the sender of the message, -every subterm of the protocol which is an encrypted term has the form {< S, ... >} K (it contains the signature on the left inside the encryption). 4. Two different encrypted terms which are encrypted by the same type of keys (public, private, ...) must have a different number of elements. More precisely, if {< τ 1 , ...τ k >} K and {< τ ′ 1 , ..., τ ′ k ′ >} K ′ are two different subterms of a protocol P and K, K ′ are of the same type, then K = K ′ .

Let us comment the four given conditions. Condition (4) helps to prevent the intruder from passing off a term {τ } K as a term {τ ′ } K ′ while these terms are intended to be distinct terms in the specification. Another way to obtain the same effect would be to use tagging as it is done in several papers [BP03,HLS00,RS03]. In these papers, tagging is used to prove decidability of secrecy for tagged protocols, but it is not a sufficient condition for secrecy. Condition (3) is reasonable and permits to know at each moment who is supposed to be implied in the session. An attack on TMN protocol is due to the fact that this condition is not satisfied. Condition (2) is always recommended [AN96]. At last, condition (1) is not essential here. We are convinced that this hypothesis could be relaxed, but it would make the proof more complicated. The TMN protocol is not well composed. Here is a modified version which is well composed:

01 -A → S : S, {S, B, {S, K a } K pub (S) } Kpriv(A) 02 -S → B : S, {S, B, A} Kpriv(S) 03 -B → S : S, {S, A, {S, K b } K pub (S) } Kpriv(B) 04 -S → A : S, {S, B, {S, K b } Ka } Kpriv(S)
The attack presented in the previous section fails in this new version because the intruder cannot impersonate A at the first step of the attack.

Theorem 1. A well composed protocol preserves the secrecy of unrevealed variables for nonces and short term key variables.

Before giving the proof of this theorem let us recall the sufficient condition given in [Bea04] to preserve secrecy in case of symmetric encryption, and show with a counter example that this condition is not enough for protocols involving asymmetric encryption. This sufficient condition was:

1. Encryption is of depth one. 2. Long term keys are never transmitted. 3. There exists a signature S such that every subterm of the protocol which is an encrypted term has the form {< S, ... >} K (it contains the signature on the left inside the encryption).

Here is a variant of TMN protocol which satisfies this condition. Let S =< N, A, B > where N is a nonce.

01 -A → S : S, B, {S, K a } K pub (S) 02 -S → B : S, B, A 03 -B → S : S, A, {S, K b } K pub (S) 04 -S → A : S, B, {S, K b } Ka .
Clearly, an attack similar to the one given before can be repeated. The next proposition expresses the fact that a well composed protocol guarantees some authenticity: if an agent a receives in a partial session where it plays role A a message m from another agent b and a thinks that b plays role B and that m corresponds to the message number i of the protocol, indeed b has sent this message for this purpose.

Proposition 1. Let r be a trace of a well composed protocol. If r contains a transition S (a,←,(b,a,τ ))

-→ S ′ where S contains a partial session σ of length l belonging to an agent a for the role A, and σ is replaced in S ′ by a partial session σ ′ of length l + 1 where b has role B, then there is a previous transition in r of the form S 1 (b,→,(b,a,τ ))

-→

S ′ 1 where S contains a partial session σ 1 of length l 1 belonging to agent b for the role B and σ 1 is replaced in S ′ 1 by a partial session σ ′ 1 of length l 1 + 1 where the message number l + 1 of role A is exactly the message number l 1 + 1 of role B.

Proof. If a accepts the message, it means that the message is of the right form, namely : (b, a, τ ) with τ =< s 1 , {s 1 , τ ′ } Kpriv(b) >.

Actually τ must be encrypted by K priv (b) since it is supposed to have been sent by b. Moreover, a controls that the signature located in the first elements of τ is the same as the signature contained at the beginning of the encrypted element. As a consequence, b is the agent who encrypted τ . Due to the last condition of the definition of a well composed protocol, a also controls that the number of elements in τ corresponds to the number of elements awaited by a in this session, so necessarily, b built τ to send a message number l + 1 for the role A, and this role is played by a because a has in the signature the place corresponding to role A.

We now translate in an equivalent form the property of secrecy for a well composed protocol. Let r be a run with a length l, X be an unrevealed variable for a nonce or a short key, x be a value, T be a time less than or equal to l, and t be a positive integer. The tuple (r, X, x, T, t) satisfies P 1 (resp. P 2 ) iff:

-P 1 : in r at some time T ′ < T , in one of its partial sessions whose signature does not contain I, an honest agent a generates the value x to assign to the unrevealed variable X and at time T , I learns the value x in t steps. -P 2 : in r, in one of its partial sessions whose signature does not contain I, an honest agent a learns the value x of the unrevealed variable X at time T in t steps and at the end of the run r the value x belongs to the knowledge of I, i.e. x ∈ IntrKn l . Moreover, there is no tuple of the form (r, X ′ , x, T ′ , t ′ ) satisfying P 1 , in other words x is not a value generated by an honest agent to assign to an unrevealed variable.

Lemma 1. A well composed protocol preserves the secrecy of unrevealed variables for nonces and short term key variables from the point of view of every role iff there does not exist an unrevealed variable X for a nonce or a short term key, a value x, a run r with length l, a time T ≤ l and a positive integer t such that the tuple (r, X, x, T, t) satisfies P 1 ∨ P 2 .

Proof. Firstly assume that there exists an unrevealed variable X for a nonce or a short term key, a value x, a run r with length l, a time T ≤ l and a positive integer t such that the tuple (r, X, x, T, t) satisfies P 1 ∨ P 2 . If (r, X, x, T, t) satisfies P 1 then in r at some time T ′ < T , in some partial session σ for a role A, with a signature that does not contain I, an honest agent a generates the value x to assign to the unrevealed variable X and at time T ,in some state S, I learns the value x in t steps. Clearly the secret of variable X can be broken from the point of view of role A. Actually in state S, the extension of partial session σ has a length l and a valuation v l for Kn A,l such that BasKn A,l contains X and the set R of roles of the protocol, I does not belong to the valuation v l (R) and v l (X) ∈ IntrKn S .

If (r, X, x, T, t) satisfies P 2 , in the same way let A be the role played by a in its partial session. The secret of variable X is broken from the point of view of role A. The "if" part of the Lemma is proved.

Secondly assume that in a well composed protocol, the secret of a variable X can be broken from the point of view of a role A. It means there exists a reachable state S containing a partial session σ of length l ′ for role A with valuation v l ′ for Kn A,l ′ such that BasKn A,l ′ contains X and the set R of roles of the protocol, I does not belong to the valuation v l ′ (R) and v l ′ (X) ∈ IntrKn S . Let r be a run from the initial state of the protocol to state S, let l be its length and let x = v l ′ (X). Since BasKn A,l ′ contains X it means that at some moment in the partial session σ the agent a = v l ′ (A) either generates the value x to assign to the variable X (first case) or a learns it (second case).

In the first case, let T ′ be the moment when a generates the value x. Since v l ′ (X) ∈ IntrKn S , there is a time T > T ′ when the intruder learns x in t steps, more precisely, if S i denotes the i-th state of run r, there is a state S T such that x ∈ IntrKn ST and x ∈ IntrKn ST -1 . In this first case the tuple (r, X, x, T, t) satisfies P 1 .

In the second case, in the partial session σ, a has not generated x (may be a has generated x in another session) and a has learnt the value x of X at time T ≤ l in t steps. If there exists a tuple (r, X ′ , x, T ′′ , t ′ ) satisfying P 1 , we are done. If not, then the tuple (r, X, x, T, t) satisfies P 2 . The "only if" part of the Lemma is proved.

Well composed protocols have an invariant property which is stated below not very formally: Lemma 2. If in a trace r, at time T 1 , an honest agent a generates a value x to substitute to an unrevealed variable X in a message m that he sends with a signature S not including I, then, as long as I does not learn x, x has only occurrences in encrypted components τ = {S, . . . , x, . . .} K where the term τ has been encrypted by an honest agent belonging to S and put by this same agent in a message m ′ in which the place where is x inside τ is the place of X.

Proof. The property is true at t 1 . Let t > t 1 and assume I does not know x at t. If x is in an encrypted component, this one has been encrypted by an honest agent b, in some session otherwise, I knows x. The value x is by recurrence hypothesis for b the value of an unrevealed variable X, and then in the component encrypted by b to send in a message m ′ , x is in place of X.

Proposition 2. In a well composed protocol, there does not exist any tuple satisfying P 1 ∨ P 2 .

Proof. Suppose there exist tuples (r, X, x, T, t) for which P 1 ∨P 2 holds. Consider the total strict order relation: (r, X, x, T, t) < (r ′ , X ′ , x ′ , T ′ , t ′ ) iff T < T ′ or (T = T ′ and t < t ′ ) and take a minimal tuple (r, X, x, T, t) satisfying P 1 ∨ P 2 . Let us examine the two cases :

-The tuple (r, X, x, T, t) satisfies P 1 .

Let S be the signature not including I of the partial session in which at time T 1 < T , the honest agent a generates the value x to substitute to the unrevealed variable X in a message m. Let τ be the concrete term from which I learns x at time T in t steps. We consider here the term of the very last operation of decryption made by I to learn x. This term τ has a value of type Cypher and it is of the form {..., x, ...} K . This term has not been built by I in r before, otherwise I would have known x before, and (r, X, x, T, t) would not be minimal. So it has been built by an honest agent d, and for this reason, due to Lemma 2, it has been built by an honest agent d belonging to S and put by this same agent in a message m ′ in which the place where is x inside τ is the place of X. Thus the term τ is of the form {S, ..., x, ...} K , because the places of the unrevealed variable X cannot be the places of the components of S. There are 3 cases for K : 1. K is a long term symmetric key 2. K is a public long term key 3. K is a short term symmetric key. Actually, K cannot be a private key, because this private key should be K priv (d) and the component would not be in a unrevealed position. Let's go through each of the three cases : 1. Since d has built the term τ , and since the signature inside τ does not contain I, K is equal to some K(c, d) where c is a honest agent. So I cannot decrypt τ . This first case is not possible. 2. The key K cannot be the public key of I, because I is not in the signature S. So I cannot decrypt τ . This second case is also impossible. 3. In the partial session s where d builds the term τ at time T ′ < T , either d knows K or he generates it. In both cases in the message m ′ sent by d which contains τ , K is in place of an unrevealed variable Y , otherwise, x itself would be in an unrevealed place. Thus the secret is broken from the point of view of the role played by d in this partial session s and for the variable Y in the place of K in the term τ inside the message m ′ . As for K there are two possibilities. Either d has generated it or he has learnt it at time at most T ′ in in this session s. In the first case, there is a tuple (r, Y, K, T ", t ′ ) which satisfies P 1 with T " < T . In the second case there is a tuple (r, Y, K, T ", t ′ ) which satisfies P 2 with T " < T . It contradicts the minimality of (r, X, x, T, t). -The tuple (r, X, x, T, t) satisfies P 2 .

At time T , in t steps an honest agent a in a partial session s whose signature S does not contain I learns the value x. Let τ be the last encrypted concrete term from which a learns x. This term τ was contained in a message m 1 received by a at time T or before and x in this message m 1 is in place of an unrevealed variable X. This message which has been accepted by a has the form < S, {S, ..., τ, ...} Kpriv(a1) > where a 1 ∈ S or < S, τ >. Here we use the fact that the protocol has an encryption depth at most two. If m 1 was equal to < S, τ >, then we would have τ = {.., x, .} Kpriv(c) , and x would be in place of a revealed variable. So the message has the form < S, {S, ..., τ, ...} K priv(a 1 ) >. Moreover the term τ has the form {..., x, ...} K . Let us observe that, the number of components of < S, {S, ..., τ, ...} K priv(a 1 ) > permits to the agent a to identify the index i of the message. For the same reason since the term {S, ..., τ, ...} Kpriv(a1) has been built by a 1 in some partial session s 1 , a 1 has built this term in order to send the message m 1 , and the value of τ in the partial session s 1 of a 1 and in the partial session s of a are associated to the same symbolic term of the protocol. Let us come back to τ = {..., x, ...} K .

If the agent a 1 in the partial session s 1 builds the term τ by encryption with K before sending the message m 1 , it means that in this session s 1 at this moment, x is known by a 1 . So in this session s 1 , x is learnt by a 1 at a time T ′ < T in t ′ steps. Indeed, x is not generated by a 1 at least in this session because for a 1 , in this session, x is the value of X which is unrevealed, which would contradict the fact that (r, X, x, T, t) satisfies P 2 . Thus replacing a by a 1 we get a tuple (r, X, x, T ′ , t ′ ) satisfying P 2 which contradicts the minimality of (r, X, x, T, t). So the agent a 1 in the partial session s 1 does not build the term τ by encryption with K before sending the message m 1 . It means that this term τ has been obtained from a previous message m 2 that the agent a 1 received in its partial session s 1 . Thus we can iterate our reasoning for a 1 instead of a, but only a finite number of times because the run r is finite. Thus we get in any case a contradiction.

So we've proved that there cannot exist any tuple satisfying P 1 ∨ P 2 , which by induction, proves Proposition 2.

Theorem 1 is a direct consequence of Lemma 1 and Proposition 2.

A well composed version of TMN protocol would be:

Example 2. . 01 -A → S : S, {S, B, {S, K a } K pub (S) } Kpriv(A) 02 -S → B : S, {S, B 2 , A} Kpriv (S) 03 -B → S : S, {S, B 2 , A, {S, B, K b } K pub (S) } Kpriv(B) 04 -S → A : S, {S, B 5 , {S, K b } Ka } Kpriv(S) (B n means a sequence of n B)
The previous attack fails at the first step because the intruder cannot impersonate the agent a for role A in the first message of the protocol. There are other attacks on this protocol which use the algebraic properties of the XOR algorithm used for encryption, but it is out of the scope of our framework.

Remark. As noticed by M. Abadi in [Aba99], authenticity is dual to secrecy in the sense that authenticity concerns the source of the messages while secrecy concerns their destination. Nevertheless, it seems that it is hard to ensure secrecy without some phase of authentication. If we look at attacks that breach the secrecy without using specific algebraic properties of the encryption algorithms, very often the intruder exploits some weakness of the protocol with respect to authentication.

An algorithm for securing protocols

In this section we describe a very simple algorithm A which transforms a protocol P into a protocol P ′ = A(P ) which is secure w.r.t. secrecy and such that P ′ preserves the "intended goal" of P for a large class C of protocols. Surely, we have to define what means "to preserve the intended goal". We first describe the class C, secondly we give the algorithm A which can be applied to every protocol in the class C, then we define an equivalence relation over the set of protocols in C. Finally we prove that for every protocol P in C the protocol A(P ) is equivalent to P and is well composed, so, A(P ) is secure w.r.t. secrecy.

4.1

The class C and the algorithm A Definition 3. A protocol is in C if it satisfies the following conditions:

-Encryption is of depth at most two.

-If in a template message (A, B, τ ) there is a subterm of τ with an encryption depth equal to two, then τ ′ = {τ ′′ } Kpriv(A) . -Private long term asymmetric and long term symmetric keys are never transmitted.

A lot of protocols belong to the class C : ISO/IEC 11770-3 Key Transport Mechanisms (1,2,3,4,5,6), Helsinki Protocol, TMN with public key protocol, Blake-Wilson-Menezes Secure Key Transport Protocol, Needham-Schroeder Public Key Protocol X.509 one-pass, two-pass, three-pass authentication, . . . The algorithm A is the following :

1. Introduce a new variable N for a session nonce, and define a signature S =< N, R 1 , R 2 , ..., R k > where R 1 , R 2 , ..., R k are the roles of the protocol P . 2. Transform the content m of each template message (A, B, m) according to the type of m : * If m is a tuple of n elements (n ≥ 1) and none of them is encrypted by K priv (A), replace m with {m} Kpriv(A) . * If m =< τ 1 , ..., τ n > (n ≥ 1) and at least one of the τ i is encrypted by K priv (A), replace m with {m ′ } Kpriv (A) where m ′ is the term we get, replacing each term τ i = {τ ′ i } Kpriv(A) with τ ′ i . In other terms, the encryption with K priv (A) is done over the tuple instead of some of its elements. 3. Replace in each template message, each subterm of the form {τ } K by the subterm {< S, τ >} K . Notice that, by associativity we have < S, τ >=< N, R 1 , R 2 , ..., R k , τ > 4. Replace each content m with < S, m >. 5. If several terms of the protocol encrypted by the same type of key namely long term public type, long term private type, long term symmetric type or short term symmetric type have the same number of elements, add inside the term, after the signature, occurrences of the last role in order to get different numbers of elements for all the encrypted terms of the same type.

The well composed protocol of Example 2 is obtained applying this algorithm to Example 1. We now prove that the protocol P ′ one obtains applying the algorithm A to a protocol P ∈ C is in some sense equivalent to P , i.e. the new knowledge of each role is essentially the same as before, at least from the point of view of the nonces and the session keys appearing in the protocol P .

Definition 4. Let P be a protocol in the class C and P ′ = A(P ). The protocol P ′ is said weakly equivalent to P if for each role R i for each step j, BasKn Ri,j (P ′ ) = BasKn Ri,j (P ) ∪ {R 1 , ..., R n } ∪ {n} and CrKn Ri,j (P ′ ) = σ(CrKn Ri,j (P )) where the σ({τ } k ) = {< S, τ >} k for every term τ . (Notice that terms of CrKn Ri,j have an encryption depth equal to 1 for protocols in the class C).

In other terms, at every step, the basic knowledge is only increased by the set of roles and the nonce which is added, and the encrypted knowledge is the same except that the signature in inserted in the encrypted term.

Theorem 2. Let P be a protocol in the class C and P ′ = A(P ). The protocol P ′ is weakly equivalent to P and is well composed.

Proof. Recall that for every role A, Kn A,j (P ) = {B j } ∪ Anal * A ({τ j } ∪ Kn A,j-1 ) for role A if the j-th template message of his partial session is (A, B j , τ j ) or (B j , A, τ j ).

Let (A, B j , < S, {S, τ ′ j } Kpriv(A) >) resp. (B j , A, < S, {S, τ ′ j } Kpriv(Bj ) >) be the corresponding message in P ′ . We have Kn A,j (P ′ ) = {B j } ∪ Anal * A (< S, {S, τ ′ j } Kpriv (A) >) ∪ Kn A,j-1 (P ′ ), where τ ′ is obtained from τ essentially by adding the signature in every encrypted term. So by induction on j, Kn A,j (P ′ ) = BasKn A,j (P ) ∪ {R 1 , ..., R n } ∪ {N } ∪ σ(CrKn A,j (P )) where S =< N, R 1 , ..., R n >.

Remark

The condition concerning the number of elements inside encrypted terms of the same type can be obtained more simply by adding different integers inside the encrypted terms which permit to identify them. Proceeding in this way, the messages will be shorter.

Conclusion

We have given a simple sufficient condition to guarantee the secrecy for cryptographic protocols which use pairing and symmetric and/or asymmetric encryption. Secrecy is ensured for an unbounded number of agents, nonces, sessions, without assuming any typing of terms. Moreover, for a large class of protocols we provide an algorithm which transforms a protocol into a secure one w.r.t. secrecy and preserves the "intended goal" of the original protocol. To our knowledge it is the first result of this type.

We have limited our work to protocols of depth at most two, which is reasonable from a practical point of view. It seems that we could get rid of this restriction easily, but the proof would be more technical. A drawback of our sufficient condition is that the systematic signature of messages with the private key of the sender increases the size of the message. It would be better to replace < S, {S, m} Kpriv (A) > with < S, m, {H(S, m)} Kpriv (A) > where H is a hash function. We propose to extend our study with more primitives, in particular with hash functions.

  key ::= C | KV ar | K pub (AgV ar) | K priv (AgV ar) | K(AgV ar, AgV ar) symb term ::= N V ar | AgV ar | key |< symb term, symb term >| {symb term} key

  send event : tuple (a, -→, (a, b, m)) where a, b are agents and (a, b, m) is a concrete message. It corresponds to the event "agent a sends (intentionally to agent b) the message m and this message is received by the intruder". -receive event : tuple (a, ←-, (a, b, m)) where a, b are agents and (a, b, m) is a concrete message. It corresponds to the event "The intruder sends to agent b a message m and agent b believes that this message has been sent by agent a".The knowledge of the intruder denoted IntrKn, is the set of values known by the intruder and that he cannot decompose more. It will be described more precisely below.• Send transitions We have a transition from state S to state S ′ labeled by the send event (a, →, (a, b, m)), denoted by S (a,→,(a,b,m))