We provide a composition framework together with a variety of composition theorems allowing to split the security proof of an unbounded number of sessions of a compound protocol into simpler goals. While many proof techniques could be used to prove the subgoals, our model is particularly well suited to the Computationally Complete Symbolic Attacker (ccsA) model. We address both sequential and parallel composition, with state passing and long term shared secrets between the protocols. We also provide with tools to reduce multi-session security to single session security, with respect to a stronger attacker. As a consequence, our framework allows, for the first time, to perform proofs in the CCSA model for an unbounded number of sessions. To this end, we introduce the notion of O-simulation: a simulation by a machine that has access to an oracle O. Carefully managing the access to long term secrets, we can reduce the security of a composed protocol, for instance P || Q, to the security of P (resp. Q), with respect to an attacker simulating Q (resp. P) using an oracle O. As demonstrated by our case studies the oracle is most of the time quite generic and simple. These results yield simple formal proofs of composed protocols, such as multiple sessions of key exchanges, together with multiple sessions of protocols using the exchanged keys, even when all the parts share long terms secrets (e.g. signing keys). We also provide with a concrete application to the SSH protocol with (a modified) forwarding agent, a complex case of long term shared secrets, which we formally prove secure.

B) G ' G′ G{A 7→ B(A)} ' G′{A 7→ B(A)} B is a valid simulator for G and G’ Figure 4. Simplified fragment of the AutoG&P logic H1 = (a : Fq, b : Fq.A(g, g, g)) ' H2 = (a : Fq, b : Fq, c : Fq.A(g, g, g) Figure 5. The DDH assumption complex rules, RND allow for instance to replace a uniformly distributed variable by some uniformly distributed expression. Finally, the last rules corresponds to the application of an assumption. Let us consider once again the DDH assumption in figure 5. Applying this assumptions to a game means that if in the game there is a call to an attacker with expressions of the form (gx, gy, gxy) with x and y random variables, then you can replace xy by a fresh random variable. Example 4. Let us assume the DDH assumption of figure 5, we want to prove the 3-PDDH assumption : G1 = (a : Fq, b : Fq, c : Fq.A(g, g, g, g)) ' G2 = (a : Fq, b : Fq, c : Fq, d : Fq.A(g, g, g, g) We obtain the following proof tree : TRANS(G′) ABSTRACT(B) DDH H1 ' H2 G1 ' G′ RND(d, d c ) Deq G2 ' G2 G′ ' G2 (G1 ' G2) with G′ = (a : Fq, b : Fq, c : Fq, d : Fq.A(g, g, g, g) B = λ(A), λe1, e2, e3, d : Fq, A(e1, e2, g, e3) The difficult part of the proof is to find the valid simulator for the Abstract rule. Given B, it is easy to check if the application is correct : H1{A 7→ B(A)} = a : Fq, b : Fq.(λ(A), λe1, e2, e3, d : Fq, A(e1, e2, gd, e3))(A)(g, gb, gab) = a : Fq, b : Fq.(λe1, e2, e3, d : Fq,A(e1, e2, gd, e3))(g, gb, gab) = a : Fq, b : Fq.(d : Fq,A(g, gb, gd, gabd)) = G1 H2{A 7→ B(A)} = a : Fq, b : Fq, c : Fq.(λ(A), λe1, e2, e3, d : Fq, A(e1, e2, gd, e3))(A)(g, gb, gc) = a : Fq, b : Fq, c : Fq.(λe1, e2, e3, d : Fq,A(e1, e2, gd, e3))(g, gb, gc) = a : Fq, b : Fq, c : Fq.(d : Fq,A(g, gb, gd, gcd)) = G′ However, the converse is not true, because we need to check alpha renaming and deducibility in order to know if there is a simulator. Given a game G, one can apply the DDH assumption by using the rule ABSTRACT, which requires to find a simulator B such that G = H1{A 7→ B(A)}. Basically, the idea is to abstract away some part of the game G by saying that those operations can be made by an attacker that we must give explicitly. The simulator is then a valid simulator if it corresponds to an actual attacker : it cannot guess any secret value and every expression that it contains must be computed from its input parameters. It then introduces the classical problem of deducibility in the symbolic setting. Given a set of terms, can an attacker deduce another term ? More formally, we write Γ |= e `E e′ if there exists a context C such that Γ |= C[e] =E e′ . We see here that we have a sufficient condition in order to have a valid simulator. Indeed, if every expression in the simulator can be deduced from its inputs we then have contexts that allows us to construct the expressions. Therefore, we can construct the simulator using these contexts. 3. Unrestricted decidability of axiomatized deducibility constraints Existing work concerning equational theories with Diffie-Hellman exponentiation always have some restriction. For instance, in [9] they only consider products in the exponents and in [11] they only considers polynomials with maximum degree of 1 (linear expressions). Here, we try to capture the most general possible instance of this problem, without any restriction on the terms known to the attacker and allowing the equational theory to be extended with axioms that are either equalities or inequalities between terms. Adding inequalities is an important generalization, because in order to deduce the variable b from the set {a ∗ b, a}, we need the assumption a 6= 0. In our case, when x is in Fq \ 0 we insert the assumption x 6= 0 in the context. Let X be a set of public names sampled in Fq , Y be a set of private names sampled in Fq, f1, ...fk, h ∈ K[X,Y ] be a set of polynomials over both public and secret names and Γ be a coherent set of axioms. Our deducibility problem is then to decide if : Γ |= X, g1 i1 , ..., g fk ik `E g t We solve this problem in two steps, first by reducing to terms that are only in the target group, and then solving the problem using Groebner basis techniques. Without loss of generality, we consider here the case of a bilinear map, to simplify the writing, but the proofs scale up to multilinear maps. Saturation into the target group. First, we reduce our problem to the case of a single group. This result comes from the Proposition 1 of [15]. Their constructive proof can be used to obtain the following proposition. Proposition 5. For any sets X and Y , polynomials f1, ...fn, h ∈ K[X,Y ] and groups elements g1 i1 , ..., g fn in ,if we denote (gi t ) = {ê(gij , gik)|1 ≤ j ≤ k ≤ n, gij ∈ G1, gik ∈ G2}∪{ê(gij , 1)|1 ≤ j ≤ n, gij ∈ G1, }∪{ê(1, gij )|1 ≤ j ≤ n, gij ∈ G2, }, then : Γ |= X, g1 i1 , ..., g fn in `E g t ⇔ Γ |= X, g e1 t , ..., g eN t `E−ê g t We obtain a problem where we only have elements in the target group, we can therefore reduce the general problem to the single group case. Reduction to polynomials. The problem at hand is now reduced to solving a non linear multi-variate polynomial equation, as shown by the following proposition : Lemma 6. For any sets X and Y , polynomials w1, ...wN , h ∈ K[X,Y ] Γ |= X, g1 t , ..., g wN t `E g t ⇔ ∃(ei, gi) ∈ K[X], (∀i,Γ |= gi 6= 0) ∧ ∑

Security protocols are short programs that aim at securing communication over a public network. Their design is known to be error-prone with flaws found years later. That is why they deserve a careful security analysis, with rigorous proofs. Two main lines of research have been (independently) developed to analyse the security of protocols. On the one hand, formal methods provide with symbolic models and often automatic proofs. On the other hand, cryptographic models propose a tighter modeling but proofs are more difficult to write and to check. An approach developed during the last decade consists in bridging the two approaches, showing that symbolic models are sound w.r.t. symbolic ones, yielding strong security guarantees using automatic tools. These results have been developed for several cryptographic primitives (e.g. symmetric and asymmetric encryption, signatures, hash) and security properties. While proving soundness of symbolic models is a very promising approach, several technical details are often not satisfactory. Focusing on symmetric encryption, we describe the difficulties and limitations of the available results. 1998 ACM Subject Classification F.3.1 Specifying and Verifying and Reasoning about Programs

We set up a framework for the formal proofs of RFID protocols in the computational model. We rely on the so-called computationally complete symbolic attacker model. Our contributions are: i) To design (and prove sound) axioms reflecting the properties of hash functions (Collision-Resistance, PRF); ii) To formalize computational unlinkability in the model; iii) To illustrate the method, providing the first formal proofs of unlinkability of RFID protocols, in the computational model.

We consider security properties of cryptographic protocols that can be modelled using trace equivalence, a crucial notion when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability. Infinite sets of possible traces are symbolically represented using deducibility constraints. We describe an algorithm that decides trace equivalence for protocols that use standard primitives and that can be represented using such constraints. More precisely, we consider symbolic equivalence between sets of constraint systems, and we also consider disequations. Considering sets and disequations is actually crucial to decide trace equivalence for processes that may involve else branches and/or private channels (for a bounded number of sessions). Our algorithm for deciding symbolic equivalence between sets of constraint systems is implemented and performs well in practice. Unfortunately, it does not scale up well for deciding trace equivalence between processes. This is however the first implemented algorithm deciding trace equivalence on such a large class of processes. (C) 2017 Elsevier Inc. All rights reserved.

Cryptographic protocols are successfully analyzed using formal methods. However, formal approaches usually consider the encryption schemes as black boxes and assume that an adversary cannot learn anything from an encrypted message except if he has the key. Such an assumption is too strong in general since some attacks exploit in a clever way the interaction between protocol rules and properties of cryptographic operators. Moreover, the executability of some protocols relies explicitly on some algebraic properties of cryptographic primitives such as commutative encryption. We first give an overview of the existing methods in formal approaches for analyzing cryptographic protocols. Then we describe more precisely the results obtained by the partners of the RNTL project PROUVÉ.

Recently, we proposed a technique [1] to define a computationally complete symbolic attacker for the verification of security protocols. Such a symbolic attacker can do everything computational attackers can, and hence it is possible to avoid the numerous usual restrictions computational soundness theorems require; in other words, unconditional soundness can be achieved. The main idea is that instead of listing all capabilities of the symbolic attacker (as the DolevYao technique does), we list all properties (called axioms) the attacker is not allowed to violate. The attacker wins if the negation of the security property of the protocol is consistent with the axioms and agent checks of the protocol. In followup works (e.g. [2]), we created a small library of axioms, and illustrated that the technique is suitable for proving actual protocols. Construction of an automated tool is also under way [5]. However, these earlier works considered reachability properties only. In this work we make the technique suitable for proving equivalence properties as well. We discuss some of the difficulties that made this step non-trivial and how we solved them. We also present an example protocol and its verification with this technique. In the Dolev-Yao approach, indistinguishability of protocols is defined via trace equivalence. Namely, two protocols are equivalent if the execution traces of one of the protocols are in correspondence with the execution traces of the other protocol (interacting with the same adversary) such that the corresponding traces are statically equivalent. It is easy to see however that this delivers attacks that computationally do not exist even in very simple situations. Consider for example the two processes νn′. out(n′) νb.νn.if b = 0 then out(1 · n) else out(0 · n) where n is drawn uniformly at random in {0, 1} , n′ is drawn uniformly at random in {0, 1} and b is drawn uniformly at random in {0, 1}. That is, the first process generates a nonce in {0, 1} and outputs it. The second generates a bit b and a nonce in {0, 1} , checks the value of the bit b, then outputs its opposite concatenated with n. Both processes are indistinguishable, since they output a random bitstring of length η+1. Symbolically, the first process has only one branch, while the second has two branches, all three inequivalent, they cannot be matched. The first idea would be to split the branch of the first process based on the value of the first bit. But it is unclear how to perform such a splitting automatically in general. Instead of trying to match the execution branches in the two protocols, we fold the protocols, including the control structure into the message terms so that each protocol has only one trace. This trick is inspired by [3]. The branches of the process are merged such that at each step, instead of numerous possible outputs, a single term is produced, which (instead of the control structure of the original process) contains all the conditional branching leading to that point. For instance, the second process above is folded into νb.νn.out(if b = 0 then 1 · n else 0 · n ) introducing if then else as a function symbol on terms. This way, we are left to check the equivalence on terms: n′ ∼ if b = 0 then 1 · n else 0 · n where ∼ is indistinguishability (of terms), the single predicate we introduce in our language. While axiomatizing computational security notions such as CPA in this framework turned out to be rather straightforward, it was more challenging to introduce convenient and computationally sound axioms for the relationship of ∼ and the function symbol if then else . We present some of our axioms, and show how our technique works by verifying (but first correcting) the simple private authentication protocol from [4] on which these basic difficulties can be illustrated.

The design of automated security proofs is a topic extensively studied for over 20 years. One problem that was raised about 12 years ago is the validity (or the scope) of such proofs. Symbolic models are quite far from the implementation. In contrast, modern cryptography typically considers more powerful attackers. This includes of course some computations that are not explicitly specified. This issue has been first addressed by M. Abadi and P. Rogaway [1], followed by many authors. The idea is to prove that the symbolic formal model is sound with respect to the more concrete computational model: if there is no attack in the symbolic model, then there is no attack in the computational model. There are several such soundness proofs, for various primitives and in various contexts (see e.g. [10], [2], [9] to cite only a few). However, all these results require heavy proofs and assume strong hypotheses, some of which are not quite realistic. Typical examples of unrealistic assumptions include: a key cycle is never created, or the attacker does use the key generation algorithm to build his own keys.

We consider the problem of computational indistinguishability of protocols. We design a symbolic model, amenable to automated deduction, such that a successful inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. We follow the idea we introduced earlier for reachability properties, axiomatizing what an attacker cannot violate. This results a computationally complete symbolic attacker, and ensures unconditional computational soundness for the symbolic analysis. We present a small library of computationally sound, modular axioms, and test our technique on an example protocol. Despite additional difficulties stemming from the equivalence properties, the models and the soundness proofs turn out to be simpler than they were for reachability properties.

Deducibility constraints represent in a symbolic way the infinite set of possible executions of a finite protocol. Solving a deducibility constraint amounts to finding all possible ways of filling the gaps in a proof. For finite local inference systems, there is an algorithm that reduces any deducibility constraint to a finite set of solved forms. This allows one to decide any trace security property of cryptographic protocols. We investigate here the case of infinite local inference systems, through the case study of blind signatures. We show that, in this case again, any deducibility constraint can be reduced to finitely many solved forms (hence we can decide trace security properties). We sketch also another example to which the same method can be applied.

The main contribution of the paper is a PTIME decision procedure for the satisfiability problem in a class of first-order Horn clauses. Our result is an extension of the tractable classes of Horn clauses of Basin & Ganzinger in several respects. For instance, our clauses may contain atomic formulas S⊢t where ⊢ is a predicate symbol and S is a finite set of terms instead of a term. ⊢ is used to represent any possible computation of an attacker, given a set of messages S. The class of clauses that we consider encompasses the clauses designed by Bana & Comon-Lundh for security proofs of protocols in a computational model. Because of the (variadic) ⊢ predicate symbol, we cannot use ordered resolution strategies only, as in Basin & Ganzinger: given S⊢t, we must avoid computing S′⊢t for all subsets S′ of S. Instead, we design PTIME entailment procedures for increasingly expressive fragments, such procedures being used as oracles for the next fragment. Finally, we obtain a PTIME procedure for arbitrary ground clauses and saturated Horn clauses (as in Basin & Ganzinger), together with a particular class of (non saturated) Horn clauses with the ⊢ predicate and constraints (which are necessary to cover the application).

State of the art Formal methods have been used in the past decades for the verification of security protocols. Such formal mehods necessarily rely on formal models of the protocols, typically process algebras. In such formal models, the security primitives are idealized: the messages are represented by terms in a formal algebra and the possible operations on these messages are specified using equations. For instance, we could specify the decryption as dec(k, enc(x, k)) = x. Unfortunately, these models (so-called “Dolev Yao”) are not necessarily fully abstract: it happened (and will happen) that a protocol is formally proved in such a model and later an attack is found (in a more accurate model). It is embarrassing. We therefore need to prove that our formal model is adequate (or fully abstract) w.r.t a concrete model. This is what is called computational soundness. Since the landmark work of M. Abadi and Ph. Rogaway [1], several computational soundness proofs have been proposed. However, they alwas assume hypotheses that are often considered as unrealistic. Moreover, these results only apply to a fixed set of cryptographic primitives. Finally, the soundness proofs are usually very long and complex.

Logic plays an important role in formal aspects of computer security, for instance in access control, security of communications or even intrusion detection. The peculiarity of security problems is the presence of an attacker, whose goal is to break the intended properties of a system/database/protocol... In this tutorial, we will consider several attacker's models and study how to find attacks (or to get security guarantees) on communication protocols in these different models.

Rewriting theory is becoming of increasing interest to security researchers. Rewriting logic is a form of logic which has the advantage of being straightforward to automate, thus making it useful not only for specifying security properties of systems, but verifying that these properties hold. One particular application in which rewriting is making important contributions is the verification of security protocols that are used to protect communication in networks. Security protocols are used now in more and more applications as the extent of our networked environment grows. Since the early 1980s, a growing effort has been put into the automated verification of such protocols. Following Dolev and Yao (1983), the most popular model of protocols relies on a representation of messages as terms: each cryptographic primitive is a function symbol. Variables usually represent parts of the messages that cannot be analysed, hence that could be replaced by an attacker who intercepts and forges new messages. That is why, since this area of research started, term unification plays an important role in the automated verification of security protocols. Until ten years ago, only a few security primitives were considered. More recently, several other primitives were introduced, for instance exclusive or. For most examples, the free term algebra is too rough for a faithful abstraction of the cryptographic primitives. Thus it is necessary to require that the function symbols used in specifying the cryptosystems satisfy some algebraic properties: the messages are now member of a quotient term algebra. This quotient structure is specified by a set of equations. Many of these equations can be specified as rewrite rules, which allows us to bring rewriting theory to bear on the problem.

We consider the question of the adequacy of symbolic models versus computational models for the verification of security protocols. We neither try to include properties in the symbolic model that reflect the properties of the computational primitives nor add computational requirements that enforce the soundness of the symbolic model. We propose in this paper a different approach: everything is possible in the symbolic model, unless it contradicts a computational assumption. In this way, we obtain unconditional soundness almost by construction. And we do not need to assume the absence of dynamic corruption or the absence of key-cycles, which are examples of hypotheses that are always used in related works. We set the basic framework, for arbitrary cryptographic primitives and arbitrary protocols, however for trace security properties only.

We provide a symbolic model for protocols using public-key encryption and hash function, and prove that this model is computationally sound: if there is an attack in the computational world, then there is an attack in the symbolic (abstract) model. Our original contribution is that we deal with the security properties, such as anonymity, which cannot be described using a single execution trace, while considering an unbounded number of sessions of the protocols in the presence of active and adaptive adversaries. Our soundness proof is different from all existing studies in that it does not require a computable parsing function from bit strings to terms. This allows us to deal with more cryptographic primitives, such as a preimage-resistant and collision-resistant hash function whose input may have different lengths.