Yannick Chevalier

Finitary Deduction Systems

Cryptographic protocols are the cornerstone of security in distributed systems. The formal analysis of their properties is accordingly one of the focus points of the security community, and is usually split among two groups. In the first group, one focuses on trace-based security properties such as confidentiality and authentication, and provides decision procedures for the existence of attacks for an on-line attackers. In the second group, one focuses on equivalence properties such as privacy and guessing attacks, and provides decision procedures for the existence of attacks for an offline attacker. In all cases the attacker is modeled by a deduction system in which his possible actions are expressed.

We present in this paper a notion of finitary deduction systems that aims at relating both approaches. We prove that for such deduction systems, deciding equivalence properties for on-line attackers can be reduced to deciding reachability properties in the same setting.

Introduction

Context. Security protocols, i.e. protocols in which the messages are cryptographically secured, are a cornerstone of security in distributed applications. The need for optimizing resource utilization and their distributed nature make their design error prone, and formal methods have been applied successfully to detect errors in the past [START_REF] Lowe | Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR[END_REF][START_REF] Armando | Formal analysis of saml 2.0 web browser single sign-on: breaking the saml-based single sign-on for Google Apps[END_REF]. But they are limited in expressiveness since in most cases authors either were focused on the resolution of reachability problems, or considered models in which the attacker could not interfere with the on-going communications among the honest agents. In contrast we consider in this paper the general case of equivalence properties w.r.t. an on-line attacker.

Formal models of cryptographic protocols usually present the reader with a dichotomy between the honest agents-translated into a constraint system [START_REF] Amadio | On the reachability problem in cryptographic protocols[END_REF][START_REF] Millen | Constraint solving for boundedprocess cryptographic protocol analysis[END_REF][START_REF] Rusinowitch | Protocol insecurity with finite number of sessions is NP-complete[END_REF] or a frame [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF]-, and the attacker-modeled by a deduction system expressing its possible actions. In contrast we have introduced in [START_REF] Chevalier | Towards an automatic analysis of web service security[END_REF] a notion of symbolic derivation that unifies the honest and dishonest agent models: the actions of all agents are represented by a sequence of deductions, nonce creation, and communication actions. The notion of equivalence considered in this paper is the one of symbolic derivations representing honest agents.

Intuition. First, a trivial remark: since one can construct deduction systems for which reachability is decidable but static equivalence is not, it is clear that generally speaking being able to decide reachability does not imply being able to decide symbolic equivalence. However, in most cases, one can model reachability as the satisfiability of a constraint system, and describe the decision procedure using constraint transformation rules. A solved form is defined as a constraint system in which the attacker just has to instantiate variables by any term he can construct. In practice, the proof of completeness of the procedure consists in assuming the existence of a sequence of deduction steps that satisfies the constraint system, and in proving that as long as one such sequence exists, either the constraint system is in solved form or there exists a transformation rule applicable on the constraint system. Then, an argument is given to prove that there is no infinite sequence of transformations. Using König's lemma, the finiteness (also to be proved) of the number of possible successors of each constraint system implies termination of the procedure.

Our motivation was that such procedures actually do much more than simply deciding reachability, as they end with a set of constraint systems in solved form that, as long as the completeness proof is along the lines given above, cover all possible attacks. Formalizing this argument is however not trivial, since

• not all instances of the variables occurring in a constraint system in solved form correspond to attacks; and

• when testing the equivalence of two protocols, we have to take into account the equality tests the attacker can perform to analyze the responses of the honest agents.

We have bypassed the first difficulty by imposing that the attacker instantiates the first-order variables in a constraint system in solved form with constants, and proved that replacing these constants by any possible construction yields another attacks. This replacement is formalized by on ordering on the attacks, the attacks corresponding to solved forms being the minimal ones. Finitary deduction systems are those for which the set of minimal attacks is always finite. The second difficulty is solved by first proving that it suffices to consider an attacker that performs at most one test, and then proving that this test can be guessed before the computation of solved forms. Finally and implementationwise, we consider effective finitary deduction system, for which we assume that this finite set is computable.

Applications. The symbolic equivalence notion we consider in this paper has three straightforward applications, related respectively to on-line guessing attacks, to proving cryptographic properties in a symbolic setting, and to privacy. We have proved, in collaboration with M. Rusinowitch [START_REF] Chevalier | Compiling and securing cryptographic protocols[END_REF] that every protocol narration (for any deduction system) can be compiled into an active frame, which is a simplified form of symbolic derivations with a total ordering on states and no intermediate computations between communications.

Guessing attacks. Introduced by Schneier [START_REF] Schneier | Applied cryptography[END_REF] under the name of dictionary attacks, they consist in guessing a secret piece of data, and then being able to check whether the guess is correct. They can be offline, in which case the attacker observes interactions between honest participants and has to decide whether the guessed piece of data has been employed, or on-line, in which case the intruder can interact with the honest participants.

Guessing attacks have been formalized thanks to the concept of indistinguishability (see e.g. [START_REF] Abadi | Guessing attacks and the computational soundness of static equivalence[END_REF]). We can say now that a protocol is vulnerable to undetectable on-line guessing attacks whenever (i) the honest agents cannot distinguish between a session with the right piece of data and one involving a wrong guess, whereas (ii) the intruder can distinguish the two executions. We model the first point by stating that the tests performed by the honest agents succeed in both cases, and the second point by saying that the two executions are not equivalent.

Cryptographic properties. A line of works initiated by [START_REF] Abadi | Reconciling two views of cryptography (the computational soundness of formal encryption)[END_REF] showed that computational proofs of indistinguishability ensuring the security of a protocol can be derived, under some natural hypothesis on cryptographic primitives, from symbolic equivalence proofs. This has opened the path to the automation of computational proofs. It was shown by [START_REF] Comon | Computational soundness of observational equivalence[END_REF] that in presence of an active attacker observational equivalence of the symbolic processes can be transferred to the computational level.

Privacy. Symbolic equivalence is a crucial notion for specifying security properties such as anonymity or secrecy of a ballot in vote protocols [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF]. More generally, the analysis of privacy, e.g. client's identity in an anonymization protocol such as IDEMIX [START_REF] Mödersheim | A formal model of identity mixer[END_REF][START_REF] Camenisch | A formal model of identity mixer[END_REF], in communication protocols is inherently an equivalence problem. One has to prove that a protocol preserves the strong secrecy of an attribute, i.e. that an observer cannot distinguish the execution of a protocol transmitting this attribute's value, be it a vote or her identity, from one in which a random piece of data is exchanged.

Related works. We believe that Mathieu Baudet's modeling of attacks by instantiation of second-order variables [START_REF] Baudet | Deciding security of protocols against off-line guessing attacks[END_REF] is the real breakthrough that enabled the formal analysis of the equivalence problem in the on-line attacker setting. Indeed, it was the first-time that the actions of the attacker were represented explicitly in solutions, instead of just keeping track (with a substitution on the first-order variables of the constraint system) of their interaction with the honest participants.

In collaboration with M. Rusinowitch [START_REF] Chevalier | Compiling and securing cryptographic protocols[END_REF] we have given another proof of Baudet's result in the setting of symbolic derivations. We believe that this setting is more complex but introduces a langage fit to prove decidability and complexity results. Also it possesses a symmetry between honest participants and the attacker that permits to greatly simplify otherwise redundant proofs. We consider in this paper a setting in which the actions of the honest agents are represented by one Honest symbolic derivation (HSD) and those of a unique intruder by one Attacker Symbolic Derivation (ASD). Symbolic derivations can be seen as standing between symbolic traces [START_REF] Baudet | Deciding security of protocols against off-line guessing attacks[END_REF] and the simple cryptographic processes of [START_REF] Cortier | A method for proving observational equivalence[END_REF]: the sequence of messages is not totally ordered as it is the case in [START_REF] Baudet | Deciding security of protocols against off-line guessing attacks[END_REF], but there is no branching but for termination on error nor any recursive process.

Few decidability results are available. In the article [START_REF] Hüttel | Deciding framed bisimilarity[END_REF] Hüttel proves decidability for a fragment of the spi-calculus without recursion for framed bisimilarity. Since, the only original decidability result on the equivalence of symbolic traces1 we are aware of is for the class of subterm deduction systems and was given by M. Baudet [START_REF] Baudet | Deciding security of protocols against off-line guessing attacks[END_REF][START_REF] Baudet | Sécurité des protocoles cryptographiques : aspects logiques et calculatoires[END_REF]. We have recently given another proof of this result [START_REF] Chevalier | Decidability of equivalence of symbolic derivations[END_REF], on which this paper elaborates. Implementation-wise, an efficient procedure is presented in [START_REF] Cheval | Automating security analysis: symbolic equivalence of constraint systems[END_REF] in which one considers only the Dolev-Yao deduction system. In spite of the relevance of this problem, we are not aware of any extension of Baudet's decidability results to other classes of deduction systems.

In [START_REF] Tiu | Automating open bisimulation checking for the spi calculus[END_REF] the authors consider, as Hüttel [START_REF] Hüttel | Deciding framed bisimilarity[END_REF], the same problem in the simpler case of the standard Dolev-Yao syntactic deduction system (with no equational theory). They employ the notion of solved form as introduced in [START_REF] Amadio | On the reachability problem in cryptographic protocols[END_REF], and more specifically that solved forms cover all possible attacks. The existence of such a finite set of solved forms corresponds exactly to our notion of finitary deduction system.

However, we note that their setting enforces a strict separation between the values of the first order variables and the observer process. This has in our opinion two negative side-effects. First, it is well-known that not all instances of the first-order substitutions constructed are instances of attacks. Second, given that the authors of [START_REF] Tiu | Automating open bisimulation checking for the spi calculus[END_REF] only keep track of the constraints that remain to be solved, the attacks themselves are not represented explicitly in the solution. Hence it is not possible to reason on all first-order instances of a solved form (since they are not all attacks) nor on the observer processes (since only their interaction with the processes under scrutiny is recorded). This is the reason why we believe that the symbolic derivation setting adopted in this paper, while more cumbersome at first, is better suited to reason on sets of solutions, and therefore on process equivalence.

Many works have been dedicated to proving correctness properties of cryptographic protocols using equivalences on process calculi. In particular framed bisimilarity has been introduced by Abadi and Gordon [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF] for this purpose, for the spi-calculus. Another approach that circumvents the context quantification problem is presented in [START_REF] Boreale | Proof techniques for cryptographic processes[END_REF] where labeled transition systems are constrained by the knowledge the environment has of names and keys. This approach allows for more direct proofs of equivalence.

In [START_REF] Cortier | A method for proving observational equivalence[END_REF] the authors show how to apply the result by Baudet on S-equivalence to derive a decision procedure for symbolic equivalence for subterm convergent theories for simple processes. Since [START_REF] Cortier | A method for proving observational equivalence[END_REF] relies on the proof of Baudet's result, that is long and difficult [START_REF] Baudet | Sécurité des protocoles cryptographiques : aspects logiques et calculatoires[END_REF], we believe that providing a simple criterion will be useful to derive other decidability results in process algebras.

To the best of our knowledge, the only tool (besides [START_REF] Cheval | Automating security analysis: symbolic equivalence of constraint systems[END_REF]) capable of verifying equivalence-based secrecy is the resolution-based algorithm of ProVerif [START_REF] Blanchet | Automatic proof of strong secrecy for security protocols[END_REF] that has been extended for handling equivalences of processes that differ only in the choice of some terms in the context of the applied π-calculus [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF]. This allows to add some equational theories for modeling properties of the underlying cryptographic primitives.

Example finitary deduction systems. We remark that the standard Dolev-Yao deduction system [START_REF] Dolev | On the Security of Public-Key Protocols[END_REF] is finitary, since for every attack one can guess a subsequence of deduction steps which is itself an attack [START_REF] Chevalier | Verifying cryptographic protocols with subterms constraints[END_REF]. In this regard, this work extends [START_REF] Tiu | Automating open bisimulation checking for the spi calculus[END_REF] to other deduction systems such as subterm deduction systems (the proof that from every attack one can guess a sequence of deductions bounded by the size of the input protocol is given e.g. in [START_REF] Kourjieh | Logical Analysis and Verification of Cryptographic Protocols[END_REF]). We leave to future work the extension to contracting saturated deduction systems, also defined in [START_REF] Kourjieh | Logical Analysis and Verification of Cryptographic Protocols[END_REF].

Organization of this paper. We reuse in this paper the notions and notations for terms, equational theories, deduction systems, and symbolic derivations introduced in earlier papers (sections 2-3). We give in Section 4 a few properties of symbolic derivations, and define finitary deduction systems accordingly. We present in Section 5 a sketch of the proof the symbolic equivalence is decidable for finitary deduction systems, and conclude in Section 6. This document is the version of an article submitted to ACM CCS 2011 with the addition of the proofs of all statements.

2 Formal setting

Term algebra

We consider a countable set of free constants C, a countable set of variables X , and a signature F (i.e. a set of function symbols with arities). We denote by T (F ) (resp. T (F , X ) ) the set of terms over F ∪ C (resp. F ∪ C ∪ X ). The former is called the set of ground terms over F , while the latter is simply called the set of terms over F . Variables are denoted by x, y, terms are denoted by s, t, u, v, . . ., and decorations thereof, respectively.

A constant is either a free constant in C or a function symbol of arity 0. Given a term t we denote by Var(t) the set of variables occurring in t and by Const(t) the set of constants occurring in t. We denote by atoms(t) the set Var(t) ∪ Const(t). We denote by A the set of all constants and variables. A substitution σ is an idempotent mapping from X to T (F , X ) such that Supp(σ) = {x|σ(x) = x}, the support of σ, is a finite set. The application of a substitution σ to a term t is denoted tσ and is equal to the term t where all variables x have been replaced by the term xσ. A substitution σ is ground w.r.t. F if the image of Supp(σ) is included in T (F ).

The set of the subterms of a term t, denoted Sub(t), is defined inductively as follows. If t is a constant or a variable then Sub(t) = {t}. Otherwise, t must be of the form f (t 1 , . . . , t n ), and we define Sub(t) = {t} ∪ n i=1 Sub(t i ). The positions in a term t are defined recursively as usual (i.e. as sequences of integers), ǫ being the empty sequence. We denote by t |p the subterm of t at position p. We denote by t[p ← s] the term obtained by replacing in t the syntactic subterm t |p by s.

Equational theories and Unification

We consider in this paper an equational theory E that defines a congruence on the terms in T (F , X ) . We assume it is consistent, i.e. that it has a model with more than one element. Ordered rewriting [START_REF] Dershowitz | Rewrite systems[END_REF] then permits us to employ the unfailing completion procedure of [START_REF] Hsiang | A new method for establishing refutational completeness in theorem proving[END_REF] to produce a (possibly infinite) set of equations for which ordered rewriting is convergent on ground terms, its ocompletion. In turn, this convergence permits us to constructively choose one element in the congruence class of each ground term t, called its normal form, and denoted (t)↓. We use in this paper the fact that since ordered rewriting is a relation on ground terms, if a term t is ground then the term (t)↓ is also a ground term.

This construction relies on the assumption that the ground terms are totally ordered by a simplification ordering, and that the minimum for this ordering is a free constant c min .

Unification and equational theory type

Our result on deduction systems may seem vacuous as the definitions-based on an ordering on the "attacks" on a protocol-are not constructive. They however follow a classical line of definitions in the context of unification and equational theories. We present in this subsection these classical notions (and refer the reader e.g. to [START_REF] Kirchner | Unification[END_REF] for a more complete overview) in order to hilight the similitudes between our definitions and the classical ones for unification.

Definition 1 (E-unifiers) Let E be an equational theory. We say that two terms t and s are E-equal, and denote s = E t, if E |= = t = s. We say that a substitution σ is a E-unifier of s and t if E |= = tσ = sσ.

We say that two terms that have a E-unifier are E-unifiable. We denote Σ E (t, t ′ ) the set of all unifiers of t and t ′ . This set is not empty if, and only if, t and t ′ are unifiable. We extend the notion of unifier to conjunctions of equations as follows.

Definition 2 (Unification systems) Let E be an equational theory. An E-Unification system S is a finite set of equations denoted by {u i ? = v i } i∈{1,...,n} with terms u i , v i ∈ T (F , X ). It is satisfied by a substitution σ, and we note σ |= E S, if for all i ∈ {1, . . . , n} u i σ = E v i σ.

One defines an instantiation ordering on unifiers by setting σ ≤ i τ whenever there exists a substitution θ such that σθ = E τ . Equational theories are classified [START_REF] Schmidt-Schauß | Unification under associativity and idempotence is of type nullary[END_REF] w.r.t. the possible cardinalities of complete sets of unifiers. Definition 3 (Complete set of unifiers) Let E be an equational theory and t, t ′ be two terms. We say that a subset S of Σ E (t, t ′ ) is a complete set of unifiers of t and t ′ if, for every substitution σ ∈ Σ E (t, t ′ ) there exists a substitution τ ∈ S and a substitution θ such that τ θ = E σ.

Or, using the instantiation ordering terminology, a complete set of unifiers is a set of minimal unifiers for the instantiation ordering such that every unifier is an instance of a unifier in this set. Finally, we define a set of most general unifiers to be a minimal set, for standard set inclusion, among the complete sets of unifiers. The rationale for this definition is that modulo an equational theory, two substitutions may be non-trivial instances one of the other. In this case one of the two is redundant and can be removed, hence the following definition.

Definition 4 (Most general E-unifiers) Let E be an equational theory. We call a set of most general E-unifiers of t and t ′ , and denote mgu E (t, t ′ ), a minimal (for set inclusion) complete set of unifiers of two terms t and t ′ .

In the rest of this paper, and as long as there is no ambiguity, we simply refer to such sets as sets of most general unifiers, or sets of mgu. Also, the notion of mgu is extended as usual to unification systems. One proves the next lemma by constructing explicitly an injection from each complete set of unifiers to the other.

Lemma 1 Let E be an equational theory, t, t ′ be two terms, and S, S ′ be two sets of most general unifiers of t and t ′ . Then S and S ′ have the same cardinality.

The finiteness or even the existence of a minimal complete set of unifiers of two terms unifiable modulo E is not guaranteed. We say that an equational theory is finitary whenever, for every two unifiable terms t, t ′ , mgu E (t, t ′ ) is a finite set.

One important property of unification systems that we shall use in the rest of this paper is the following replacement property.

Lemma 2 For any equational theory E, if a E-unification system S is satisfied by a substitution σ, and c is any free constant in C away from S, then for any term t, σδ c,t is also a solution of S.

Variables and constants. Using Lemma 2 we can clarify the difference and similitudes between variables and free constants. First, a formal point: since free constants do not occur in the equations of the equational theory they are not among the constants obtained by skolemization. Second, we agree that in the resolution procedure [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF], variables have a special role whereas by Herbrand's theorem we know that it suffices to consider models of a set of clauses with at most one free constant. In spite of this we almost use variables and free constants (as in Lemma 2) interchangeably.

The rationale is that ordered completion yields a rewriting relation which is convergent on ground terms, and thus cannot be employed to normalize terms that contain variables. Lemma 2 is thus fundamental since it implies that some of the free constants that may appear in an unifier can be replaced, the main difference with variables being that if, for a simplification ordering <, we have t < t ′ , then for every substitution σ we also have tσ < t ′ σ, whereas it is not the case that for every replacement δ c,s we also have tδ c,s < t ′ δ c,s .

Deduction systems

Our protocol analysis is based on the assumption that all the agents operate on messages via a message manipulation library. We consider a signature F containing the function symbols employed to denote the messages, with a special subset of symbols F p denoting the functions of the library which can be employed by all participants.

Definition 5 (Deduction systems) A deduction system is defined by a triple (E, F , F p ) where E is an equational presentation on a signature F and F p a subset of public constructors in F .

Example 1 For instance the following deduction system models public key cryptography:

({dec p (enc p (x, y), y -1 ) = x}, {dec p ( , ), enc p ( , ), -1 }, {dec p ( , ), enc p ( , )})
The equational theory is reduced here to a single equation that expresses that one can decrypt a cipher text when the inverse key is available.

Symbolic derivations

We present in this section our model for agents.

Definitions

Symbolic derivations. Given a deduction system (F , P, E), a role applies public symbols in P to construct a response from its initial knowledge and from messages received so far. Additionally, it may test equalities between messages to check the well-formedness of a message. Hence the activity of a role can be expressed by a fixed symbolic derivation:

Definition 6 (Symbolic Derivations) A symbolic derivation for a deduction system (F , P, E) is a tuple (V, S, K, In, Out) where V is a mapping from a finite ordered set (Ind, <) to a set of variables Var(V), K is a set of ground terms (the initial knowledge) In is a subset of Ind, Out is a multiset of elements of Ind and S is a unification system. The set Ind represents internal states of the symbolic derivation. We impose that any i ∈ Ind is exactly one of the following kind:

Deduction state: There exists a public symbol f ∈ P of arity n such that V(i)

? = f (V(α 1 ), . . . , V(α n )) ∈ S with α j < i for j ∈ {1, . . . , n} .
Re-use state: if there exists j < i with V(j) = V(i);

Memory state: if there exists t in K and an equation V(i)

? = t in S;
Reception state:

if i ∈ In;
Additionally, a state i is also an emission state if i ∈ Out.

The unification system S contains no equation but those described above and equations V(i) ? = V(j), and the mapping V must be injective on non-re-use states.

A symbolic derivation is closed if it has no reception state. A substitution σ satisfies a closed symbolic derivation if σ |= E S.

We believe that using symbolic derivations instead of more standard constraint systems permits one to simplify the proofs by having a more homogeneous framework. There is however one drawback to their usage. While most of the time it is convenient to have an identification between the order of deduction of messages and their send/receive order, building in this identification too strictly would prevent us from expressing simple problems. Re-use states are employed to reorder the deduced messages to fit an order of sending messages which can be different. For example consider an intruder that knows (after reception) two messages a and b received in that order, and that he has to send first b, then a. Since the states in a symbolic derivation have to be ordered, we have to use at least one re-use state (for a) to be able to consider a sending of a after the sending of b. We note that re-use states that are not employed in a connection can be safely eliminated without changing the deductions, the definition of the knowledge nor the tests in the unification system.

With respect to earlier definitions, we have chosen to consider injective variable-state mapping functions. The rationale for this choice is essentially aesthetic, as using this more strict definition implies that every equality test performed by the attacker is an equality V(i) ? = V(j) in the unification system. Not having this restriction would require the introduction of a) an equivalence class on ASDs to model the fact that two ASDs can be solutions to exactly the same HSDs, and b) the subset of ASDs that have an injective variable-state mapping function,and c) the construction, by adding equality tests, for every ASD of an equivalent ASD in this subset.

Example 2 Let us consider the cryptographic protocol for deduction system DY where F D and P D have been extended by a free public symbol f :

A→B: enc p (N a , pk(B)) B→A: enc p (f (N a ), pk(A)) where A knows A, B, pk(B), pk(A), sk(A) B knows A, B, pk(A), pk(B), sk(B)
Let us define a symbolic derivation for role B:

Ind B = {1, . . . , 9} V B = i ∈ Ind → x i K B = {A, B, pk(A), pk(B), sk(B)} In B = {6} Out B = {9} S B = {x 1 ? = A, x 2 ? = B, x 3 ? = pk(A), x 4 ?
= pk(B), x 5 ?

= sk(B)

x 7 ? = dec p (x 6 , x 5 ), x 8 ? = f (x 7 ), x 9 ? = enc p (x 8 , x 3 )}
The set of deduction states in B is {7, 8, 9}, there are no re-use state, the set of memory states is {1, . . . , 5} and the only reception state is 6. Assuming that the role B tests whether the received message is a cipher, one may add a tenth deduction state with x 10 ? = enc p (x 7 , x 4 ) and an equation x 6 ? = x 10 . Similarly, a symbolic derivation for role A would be: The set of deduction states in A is {6, 7, 9}, there are no re-use state, the set of memory states is {0, . . . , 5} and the only reception state is 8. We have added an equality test y 9 ?

Ind A = {1, . . . , 10} V = i ∈ Ind → y i K = {A,
= y 7 to model that A checks whether the message received actually contains the encryption of f (N a). Generally speaking, if ground reachability and ground symbolic equivalence for the deduction system are decidable (see Section 3.3) then an as prudent as possible set of deductions and equality tests for the narration can be computed (see [START_REF] Chevalier | Compiling and Securing Cryptographic Protocols[END_REF]).

In addition we assume that two symbolic derivations do not share any variable, and that equality between symbolic derivations is defined modulo a renaming of variables. The proof of the following lemma is a direct consequence of the definition. x 3 ? = pk (A) 4

x 4

x 4 ? = pk (B) 5

x 5

x 5 ? = sk(B) 6

x 6 7

x 7

x 7 ? = decp (x 6 , x 5 ) 8

x 8

x 8 ? = f (x 7 ) 9

x 9

x 9 ? = encp (x 8 , x 3 )

(a) With a connection, before computing the resulting symbolic derivation x 3 ? = pk(A) 4

x 4

x 4 ? = pk(B) 5

x 5

x 5 ? = sk(B) 7

x 7

x 7 ? = decp (x 6 , x 5 ) 8

x 8

x 8 ? = f (x 7 ) 9

x 9

x 9 ? = encp (x 8 , x 3 ) (b) After computing the symbolic derivation resulting from the connection (i)

1. For every variable V(i) there is at most one equation in S of the form V(i)

? = f (t 1 , . . . , t n ); 2. If V(i)
is a variable such that the above equation is in S, then either a) i is a deduction state and i = min(j | V(i) = V(j)), or b) i is a re-use state.

We rely on the normal form defined by the o-completion of the equational theory E to prove that every closed symbolic derivation defines in a unique way the terms deduced.

Lemma 4 Let I be a deduction system, and consider a closed and satisfiable I-symbolic derivation C = (V, S, K, In, Out). Then there exists a unique ground substitution σ in normal form that satisfies S.

Proof. Since the symbolic derivation C = (V, S, K, In, Out) is closed is has by definition no input states, and thus all states are either knowledge, re-use or deduction states. By induction on the set of indexes Ind ordered by <.

Base case: Assume i is a minimal element in Ind. By minimality i cannot be a re-use state. If it is a knowledge state then by definition there exists in S an equation V(i)

?
= t, with t a ground term in normal form, and thus for every unifier τ of S we must have V(i)τ = t. If i is a deduction state, and since it is minimal, the public symbol employed must be of arity 0 and hence is a constant, i.e. again a ground term t. In both cases there exists a unique ground substitution σ in normal form defined on {V(i)} and such that any unifier of S is an extension of σ. = f (V(j 1 ), . . . , V(j n )) with j 1 , . . . , j n < i that has to be satisfied by every unifier θ of S. By induction every such unifier has to be equal to σ on {V(j 1 ), . . . , V(j n )}. Thus for every unifier θ of S we have

V(i)θ = E f (V(j 1 )θ, . . . , V(j n )θ). By induction f (V(j 1 )θ, . . . , V(j n )θ) = E f (V(j 1 )σ, . . . , V(j n )σ). Thus, we have V(i)θ = (f (V(j 1 )σ, . . . , V(j n )σ))↓ and σ can be uniquely extended on V(i) with V(i)σ = (f (V(j 1 )σ, . . . , V(j n )σ))↓ which is again a ground term.
By Lemma 4, if a derivation is closed, then for every i ∈ Ind the variable V(i) is instantiated by a ground term. Figuratively we say that a term t is known at step i in a closed symbolic derivation if there exists j ≤ i such that V(j) is instantiated by t.

Ground symbolic derivations. An important case when considering protocol refutation is the one in which the attacker cannot alter the messages exchanged among the honest participants. This case can either be employed to model a weaker attacker or, when trying to refute a cryptographic protocol, by guessing first which messages are sent by the attacker, and then by checking whether these guesses correspond to messages the attacker can actually send.

Definition 7 (Ground symbolic derivation) We say that a symbolic derivation

C h = (V h , S h , K h , In h , Out h
) is a ground symbolic derivation whenever S h is satisfiable and there exists a ground substitution σ such that, for every unifier τ of S h and every i ∈ Ind h we have \ h (i)σ = \ h (i)τ .

In other words the input and output messages of a ground symbolic derivation are fixed ground terms. We note that since C h is not closed, and in spite of having S h satisfiable, it is not necessarily true that C ⋆ h = ∅. Also a simple analysis of the case study of the proof of Lemma 4 shows that it suffices to assume that σ is defined only on indexes i ∈ In h .

Connection. We express the communication between two agents represented each by a symbolic derivation by connecting these symbolic derivations. This operation consists in identifying some input variables of one derivation with some output variables of the other and contrariwise. This connection should be compatible with the variable orderings inherited from each symbolic derivation, as detailed in the following definition: Assume that there is a monotone bijection φ from

Definition 8 Let C 1 , C 2 be two symbolic derivations with for i ∈ {1, 2} C i = (V i , S i , K i , In i , Out i ),
I 1 ∪ I 2 to O 1 ∪ O 2 such that φ(I 1 ) = O 2 and φ(I 2 ) = O 1 . A connection of C 1 and C 2 over the connection function φ, denoted C 1 • φ C 2 is a symbolic derivation C = (V, φ(S 1 ∪ S 2 ), K 1 ∪ K 2 , (In 1 ∪ In 2 ) \ (I 1 ∪ I 2 ), (Out 1 ∪ Out 2 ) \ (O 1 ∪ O 2 ))
where:

• (Ind, <) is defined by:

-Ind = (Ind 1 \ I 1 ) ∪ (Ind 2 \ I 2 );
-< is the transitive closure of the relation:

< 1 ∪ < 2 ; • φ is extended to a renaming of variables in Var(V 1 ) ∪ Var(V 2 ) such that φ(V 1 (i)) = V 2 (j) (resp. φ(V 2 (i)) = V 1 (j)) if i ∈ I 1 (resp. I 2 ) and φ(i) = j
When the exact connection function in a connection does not matter, is uniquely defined, or is described otherwise, we will omit the subscript and denote it

C 1 •C 2 .
A connection is satisfiable if the resulting symbolic derivation is satisfiable. It can easily computed, when it exists, by considering increasing sequences of states in each symbolic derivation and mapping input states of one SD with output states of the other. We model the initial knowledge of the intruder with another symbolic derivation C K :

Example 3 Let C h be the symbolic derivation in Example 2:

Ind h = {0, . . . , 8} V h = i ∈ Ind → x i K h = {A, B, pk(A), pk(B), sk(B)} In h = {5} Out h = {0, . . .
Ind K = {0 k , . . . , 3 k } V K = i k ∈ Ind k → y i K K = {A, B, pk(A), pk(B)} In K = ∅ Out K = Ind K S K = {y 0 ? = A, y 1 ? = B, y 2 ? = pk(A), y 3 ? = pk(B)}
and we let C ′ be the following derivation:

Ind ′ = {0 ′ , . . . , 8} V ′ = i ′ ∈ Ind ′ → z i K = {n} ⊂ C new In ′ = {0 ′ , . . . , 3 ′ , 8 ′ } Out ′ = {5 ′ } ∪ Ind ′ S ′ = {z 4 ? = n, z 5 ? = enc p (z 4 , z 3 ), z 6 ? = f (z 4 ), z 7 ? = enc p (z 6 , z 2 ), z 8 ? = z 7 }
Let φ be the application from 0 k , . . . , 3 k , 5 ′ , 8 to 0 ′ , . . . , 3 ′ , 5, 8 ′ respectively and ψ be a function of empty domain. Then we have with the ordering:

(C h • ψ C K ) • φ C ′ : Ind = {0, . . . , 4, 0 k , . . . , 3 k , 5 ′ , 6 ′ , 7 ′ , 6, 7, 8} V = V h |Ind ∪ V K |Ind ∪ V ′ |Ind K = {A, B, pk(A), pk (
0 < 1 < 2 < 3 < 4 < 5 ′ < 6 < 7 < 8 0 k < . . . < 3 k < 4 ′ < . . . < 7 ′ < 8
The connection of two symbolic derivations C 1 and C 2 identifies variables in the input of one with variables in the output of the other. Variables that have been identified are removed from the input/output set of the resulting symbolic derivation C. The set of equality constraints of C is the union of the equality constraints in C 1 and C 2 , plus equalities stemming from the identification of input and output. We have chosen to have a multiset of output variables to enable the modeler to specify whether a communication between two participants is hidden-when the output state occurs only once in the initial output multisetor visible-in which case there is more than one occurrence of the output state in the initial output multiset-to an external observer.

One easily checks that a connection of two symbolic derivations is also a symbolic derivation. Also, the associativity of function composition applied on the connections implies the associativity of the connection of symbolic derivations. Since connection functions are bijective, we will also identify C • C ′ and C ′ • C. Thus when we compose several symbolic derivations, we will freely re-arrange or remove parentheses.

Traces. Let C 1 and C 2 be two I-symbolic derivations and ϕ be a connection such that C = C 1 • ϕ C 2 = (V, S, K, In, Out) is closed and satisfiable. Lemma 4 implies that there exists a unique ground substitution τ in normal form such that any unifier σ of S 1 ∪ S 2 is equal to τ on the image of V. We denote Tr C1•ϕC2 (C ′ ) the restriction of this substitution τ to the variables in the sequence of C ′ , for

C ′ ∈ {C 1 , C 2 , C 1 • ϕ C 2 },
and call it the trace of the connection on C ′ . In the rest of this paper we will always assume that trace substitutions are in normal form.

Solutions of symbolic derivations

Honest and attacker symbolic derivations

Generally speaking, a solution of a symbolic derivation C is any couple (C ′ , ϕ) such that C • ϕ C ′ is closed and satisfiable. We specialize this definition for the case of protocol analysis in order to ensure that every term possessed by the attacker, including her initial knowledge, has been either leaked by the protocol or is a nonce she has created. This consideration lead us to consider two types of symbolic derivations, one that is employed to model honest agents, and one to model an attacker.

Honest derivations. We do not impose constraints on the symbolic derivations representing honest principals, but for the avoidance of constants in an infinite set C new ⊆ C. These constants are employed to model new values created by an attacker. We assume that nonces created by the honest agents are created at the beginning of their execution and are constants away from C new . Attacker derivations. We consider an attacker modeled by a symbolic derivation in which only the following actions are possible:

• create a fresh, random value;

• receive from and send a message to one of the honest participant;

• deduce a new message from the set of already known messages;

• every state is in Out given that the intruder should be able to observe his own knowledge;

• given that we consider an actual execution, the set of states is totally ordered.

The definition of attacker symbolic derivations models these constraints:

Definition 10 (Attacker symbolic derivations) Let C = (V, S, K, In, Out) be a symbolic derivation. It is an attacker symbolic derivation, or ASD, if a) Ind is a total order, and b) Out contains at least one occurrence of each index in Ind, and c) K is a subset of C new .

The fact that the initial knowledge of the attacker is empty but for the nonces is not a restriction when analyzing protocols, as one can see from Ex. 3.

Example 5

The following derivation C ′ is an ASD for the same deduction system as Example 2: Informally the ASD expresses that the attacker receives some key k, creates a nonce n, sends the encrypted nonce to a role B as in Example 2. Then the attacker tries to check that applying f to n gives a term equal to the decryption of B's response.

Ind ′ = {0 ′ , . . . , 8} V ′ = i ′ ∈ Ind ′ → z i K = {n} ⊂ C new In ′ = {0 ′ , . . . , 3 ′ , 8 ′ } Out ′ = {5 ′ } ∪ Ind ′ S ′ =
Solutions of a symbolic derivation. Given a symbolic derivation C h we denote C ⋆ h the set of couples (C, ϕ) where C is an ASD and ϕ is a connection function between C and C h such that C h • C is closed and satisfiable. In that case we say that C is a solution of C h .

Example 6 In Example 3 the ASD C ′ is a solution of C h • C K since (C h • ψ C K ) • φ C ′ is
closed and S is satisfiable (by simply propagating the equalities x 0 = A, x 1 = B, . . .).

Decision problems

Satisfiability. The problem of the existence of a secrecy attack on a bounded protocol execution-shown to be NP-complete in [START_REF] Rusinowitch | Protocol insecurity with finite number of sessions is NP-complete[END_REF] for the standard Dolev-Yao deduction system-is equivalent to the satisfiability problem below.

I-Satisfiability

Input: a HSD C Output: Sat iff C ⋆ = ∅ A variant of I-satisfiability is its restriction to set of inputs C which are ground symbolic derivations, and that we call I-ground satisfiability.

Ground I-Satisfiability

Input:

a ground HSD C Output: Sat iff C ⋆ = ∅
Equivalence. Let us now define the equivalence of HSDs w.r.t. an active intruder.

Definition 11 Two HSDs C h and C

′ h are symbolically equivalent iff C ⋆ h = C ′ h ⋆ .
I-Symbolic Equivalence Input:

Two honest I-symbolic derivations C h and C ′ h Output: Sat iff C h ⋆ = C ′ h ⋆ .
Again it is possible to define a ground version of the I-symbolic equivalence problem when the input consists in two ground symbolic derivations. One can easily encode static equivalence problems into ground I-Symbolic Equivalence problems by publishing every constant not hidden in the frame. Ground I-Symbolic Equivalence Input:

Two honest I-ground symbolic derivations C h and C ′ h Output: Sat iff C h ⋆ = C ′ h ⋆ .
Remark. Another possible definition of the set of solutions would be a set of ASDs, without mention of the connection function. The equivalence relation would have been distinct since in that case an ASD can be in two sets of solutions but without the same connection function. However, this would have had no impact on our decidability result. Our choice in this paper corresponds to diff-equivalence between biprocesses [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF]: the diff operator defines a bijection between the in-and output states of two processes derivations, and the equality of the sets of solutions is understood modulo this one-to-one function.

Finitary Deduction Systems

An equational theory E is finitary whenever every E-unification system has a finite set of more general unifiers. We define an analog for deduction systems w.r.t. symbolic derivations rather than equational theories w.r.t. unification systems. In the rest of this paper, we consider effective finitary deduction systems, i.e. deduction systems for which it is possible to compute a finite set of "most general attacks".

Stutter-free ASDs

We say that an ASD C I is well-formed w.r.t. a HSD C h and a connection ϕ if, in the connection C h • ϕ C I , a deduction subsequently applied on a deduced term t, or a re-use of the term t is always applied by referring to the state in which t was first deduced.

Definition 12 (Well-formed ASD) Let C h be a HSD and consider an ASD

C I = (V I , S I , K I , In I , Out I ) such that (C I , ϕ) ∈ C ⋆ h
, and σ = Tr CI •ϕC h (C I ). We say that C I is (C h , ϕ)-well-formed if for every deduction states i, for every state j ∈ Ind I with i < j we have V I (i)σ = V I (j)σ implies that • either V I (i) = V I (j), i.e. j is a re-use state;

• or there is no equation x ? = f (. . . , V I (j), . . .) in S I and j is not an emission state.

This restriction is mostly syntactic, and can be assumed w.l.o.g. for our purpose, as shown by the Lemma 8.

Our aim is the reduction of equivalence problems to reachability problems for finitary deduction systems. In the latter problems, one only considers which terms are deducible by the attacker. Hence the following definitions that will be employed to split an ASD into a deduction only part solving a reachability problem and a testing part modeling the possible tests. Given a HSD C h we denote C h sf the set of stutter-free solutions of C h . These ASDs have the special property that a connection cannot be unsatisfiable because of a rejection by the attacker. Formally speaking, we have the following proposition.

Proposition 1 Let C I = (V I , S I , K I , In I , Out I ) ∈ C ⋆
h be a deduction-only ASD. Then for any ground substitution σ of domain In I the unification system S I σ is satisfiable in the empty theory.

Proof.

We remind that a unification system S is in solved form in the empty theory if and only if there exists an ordering < u on variables such that S contains, for each variable x, at most one equation x ? = t and if for every y ∈ Var(t) we have y < u x. First let us notice that since C I is deduction-only, S I does not contain any equation V I (i)

? = V I (j) with V I (i) = V I (j).
By definition S I contains exactly one equation V I (i) ? = t if i is not an input or the re-use of an input state, and none otherwise. In the former case we can assume that for a mgu θ of S we have V(i)θ = V(i). Using the ordering on states as the ordering < u , Lemma 3 implies that S I is in solved form, and adding to S I equations V I (i) ? = t i , for i ∈ In I and t i a ground term thus leads to a unification system also in solved form.

Sets of solutions

Outline. We prove in this section that ASDs are such that, when replacing a constant in C new by the result of a sequence of compositions (this operation is called opening) we obtain another ASD which can be connected to all the HSDs the original ASD could be connected to (Lemma 5). This notion of replacement acts as the instantiation of a unifier modulo an equational theory. Accordingly we define from it a well-founded ordering on ASDs mimicking the role of the instantiation ordering on unifiers. Finally, we prove that given a set of ASDs S, the inclusion S ⊆ C ⋆ h can be check by testing only the minimal ASDs in S (Lemma 6).

Opening of symbolic derivations. • we replace all occurrences of c in C by V(i).

If C = (V, S, K, In, Out) and C ⊆ C new ∩ K is a set such such that C ∩ Sub(K \ C) = ∅,
We note that the set K ′ obtained from K after the replacement is still a set of ground terms since C ∩ Sub(K \ C) = ∅, and thus the result of the operation is still a symbolic derivation. Also, C is an ASD, then so is open C (C).

Lemma 5 Let C I ∈ C ⋆ h with C I = (V I , S I , K I , In I , Out I ), let C ⊆ K I and let C c ∈ C ′ h sf for some HSD C ′ h . If a connection C c • C h • open C (C I ) is closed then it is satisfiable. Proof. By Proposition 1 Tr Cc•C h •open {c} (CI ) (C c ) satisfies S c . Since C I is an ASD we have C ∩ Sub(K \ C) = ∅,
E S h • S ′ I imply σδ c,t |= E S h • S ′ I . Let σ ′ = Tr Cc•C h •open C (CI ) (C I ).
For each memory state i ∈ Ind I that contains a constant c ∈ C we let t c = V I (i)σ ′ . We define δ as the replacement of each constant c ∈ C by the term t c .

By induction on the indexes of the connection

C c • C h • open C (C I )
we have:

Tr Cc•C h •open C (CI ) (C c • C h • open C (C I )) = Tr C h •CI (C h • C I )δ
Thus every equation in S h ∪ S I (minus the removed memory equations) is satisfied by the composition with C c . Since every equation in its unification system is satisfied the connection

C c • C h • open C (C I ) is satisfiable.
Ordering on symbolic derivations. Consider two symbolic derivations:

C I = (V I , S I , K I , In I , Out I ) C ′ I = (V ′ I , S ′ I , K ′ I , In ′ I , Out ′ I )
We say that -

C I ≤ C ′ I if: • there exists C ⊆ K I ,
V ′′ I is the restriction of V ′ I to the domain Ind ′ I \ I -and S ′′ I = S ′ I \ {V ′ I (i) ? = c i } i∈I .
We say that C I , C ′ I are equivalent modulo a renaming of nonces, and denote C I ≡ C ′ I , whenever there exists C ⊆ K I , a stutter-free symbolic derivation C C with only memory states, and a connection ϕ such that

C C • ϕ open C (C I ) = C ′ h .
Given a set S of ASDs we denote min < (S) the set of ASDs in S that are minimal in S modulo renaming of nonces.

Since C ≤ C ′ implies that either: a) C has strictly less deduction states than C ′ , and less states, b) C has strictly less states than C', c) or C and C ′ are equivalent modulo a renaming of nonces, it is clear that < is a well-founded ordering relation modulo this renaming.

Lemma 6 Let S be a set of ASDs and C h be a HSD.

If min < (S) ⊆ C h ⋆ then S ⊆ C h ⋆ .
Proof. Assume min < (S) ⊆ C h ⋆ and let C I be in S. By definition of the ordering, first point, there exists a derivation C ′ I ∈ min < (S), a set of constants C, and a stutter-free derivation

C c such that C c •open C (C ′ I ) = C I . By hypothesis we have C ′ I ∈ C h ⋆ . By Lemma 5 this implies that C I = C c • open C (C ′ I ) is also in C h ⋆ .
Complete sets of solutions. The ordering < plays the same role w.r.t. the solutions of a HSD as the instantiation ordering on substitutions w.r.t. the solutions of an unification system. In particular the traditional notion of most general unifier is translated into a notion of minimal solution.

Definition 16 (Complete set of solutions) A set Σ of ASDs is a complete set of solutions of an HSD C h whenever:

• Σ ⊆ C ⋆ h ;
• for every ASD C I ∈ C sf h there exists an ASD C m ∈ Σ and a stutter free ASD C c such that C m ≤ C I • C c .

We have departed from our line of translating terms from the unification framework to the symbolic derivation framework by introducing a symbolic derivation C c . It permits us to consider cases in which the computation of a complete set of unifiers introduces unnecessary deduction steps in individual ASDs. A common example of such addition is the normalization of messages t, t ′ , i.e. the automatic deduction of the two messages t and t ′ even when they are not useful for the attacker.

Finitary deduction systems

We have already noted that a NP decision procedure for the satisfiability of HSDs for the Dolev-Yao deduction system is known since [START_REF] Rusinowitch | Protocol insecurity with finite number of sessions is NP-complete[END_REF]. While this procedure is based on the guessing of an attack of minimal size, other procedures have been proposed [START_REF] Amadio | On the reachability problem in cryptographic protocols[END_REF][START_REF] Millen | Constraint solving for boundedprocess cryptographic protocol analysis[END_REF] that instead cover all possible stutter-free derivations [START_REF] Chevalier | Verifying cryptographic protocols with subterms constraints[END_REF],

i.e. compute a complete set of solutions. We define deduction systems for which such a procedure exists to be finitary.

Definition 17 (Finitary Deduction Systems) Let I be a deduction system. If there exists a procedure that computes for every I-HSD C h a finite complete set of solutions we say that I is a finitary deduction system.

Decidability of Symbolic Equivalence

This section is devoted to the proof of the main theorem of this paper.

Theorem 1 Symbolic equivalence is decidable for finitary deduction systems.

We first prove that every ASD can be written as the connection between a stutter-free ASD and a testing ASD in which no new term is deduced (Lemma 7). This implies the reduction of the inclusion problem to the one of checking whether, for any stutter-free ASD in C ⋆ h , the connections of this ASD with C h and C ′ h result in closed symbolic derivations C 1 and C 2 such that C ⋆ 1 ⊆ C ⋆ 2 (Lemma 9). Given a stutter-free ASD in C ⋆ h this latter test is simple since it suffices to consider the connection with ASD that have at most one deduction (Prop. 2).

We relate these types of ASD with well-formed ASDs with the following lemma.

Lemma 7 Let C I be a (C h , ϕ)-well-formed ASD. Then there exists a connection ψ, a well-formed deduction-only ASD C d , and a testing ASD C t such that:

• C I = C d • ψ C t ,
• for all HSD C ′ and connection ψ, the connection

C ′ • ψ C I is closed if, and only if, C ′ • ψ C d is closed.
Proof. Let C h be a HSD, C I = (V I , S I , K I , In I , Out I ) bean ASD, and ϕ be a connection such that (C I , ϕ) ∈ C ⋆ h . We construct a sequence of couples (C d , C t ) of ASDs such that C d is deduction-only, C t is testing, and such that in the end C d is well-formed. We start from:

C d = (V I , S I \ S = , K I , In I , Out I ∪ Ind I ) C t = (V I , S = , ∅, Ind I , Out I )
and the connection ψ being the identity. By construction C t is testing and C d is deduction-only. However C d may not be well-formed.

For each deduction state i in C d such that there exists a deduction state j < i with V I (i)σ = V I (j)σ, let S VI (i) be the subset of equations of S I in which V I (i) occurs. Since i is a deduction state, S VI (i) contains one equation It is clear that once the construction is performed on every deduction states from C d , this symbolic derivation will be well-formed. = V I (j) on all states i, j such that: a) i is a deduction state, and b) i < j, and c) V I (i)σ = V I (j)σ. It is clear that S I ∪ S 1 is also satisfied by σ.

V I (i) ? = f (x 1 , . . . , x n ).
Lemma 8 Let C h , C ′ h be two HSDs such that C ⋆ h \ C ′ h ⋆ = ∅. Then C ⋆ h \ C ′
Then, replace in S I each equation x ? = f (. . . , V I (j), . . .) such that there exists a deduction state i < j with V I (i)σ = V I (j)σ by the equation x ? = f (. . . , V I (i), . . .), and let S I ′ be the obtained unification system. Given the equations in S 1 it is clear that S I ∪ S 1 and S I ′ ∪ S 1 are satisfied by the same set of substitutions.

Let C I ′ = (V I , S I ′ ∪ S 1 , K I , In I , Out I ). It remains to note that:

• Tr CI •ϕC h (C I • ϕ C h ) = Tr CI ′ •ϕC h (C I ′ • ϕ C h ); • Tr CI •ϕC ′ h (C I • ϕ C ′ h ) = Tr CI ′ •ϕC ′ h (C I ′ • ϕ C ′ h ), and thus (C I ′ , ϕ) / ∈ C ′ h ; • by construction C I ′ is (C h , ϕ)-well-formed. Thus, C I ′ is (C h , ϕ)-well-formed ASD in C ⋆ h \ C ′ h ⋆ .
As a consequence, we obtain the following lemma that permits to split the symbolic equivalence problem into two simpler problems.

(C t , ϕ) ∈ (C d • ψ C h ) ⋆ . Since C d • ϕ C t = C I / ∈ C ′ h ⋆ then either C d • ψ C ′ h is closed, but not satisfiable, or C t • ϕ (C d • ψ C ′ h ).
In the former case we have C sf h ⊆ C ′⋆ h , and in the latter case we have

C t ∈ (C I • C h ) ⋆ \ (C I • C ′ h ) ⋆ .

Conversely, if one of the two points does not hold, we easily construct an ASD in C

⋆ h \ C ′⋆ h .
Then we prove that if in the previous lemma the testing part is known, the stutter-free part is also a stutter-free solution of the connection between the testing part and the HSD.

Lemma 10 Assume C I ∈ C sf h and C t ∈ (C I • C h ) ⋆ . Then C I ∈ (C t • C h ) sf . Proof. We let C I , C h ,
and C t be as in the statement of the lemma, and denote them as follows:

   C I = (V I , S I , K I , In I , Out I ) C h = (V h , S h , K h , In h , Out h ) C t = (V t , S t , K t , In t , Out t )
Since C I ∈ C sf h there exists a one-to-one2 mapping ϕ :

In I ∪ In h → Out I ∪ Out h such that C ′ h = C I • ϕ C h is closed and satisfiable. Let us denote C ′ h = (V ′ h , S ′ h , K ′ h , In ′ h , Out ′ h ).

Also by hypothesis there exists a one-to-one mapping ψ : In

′ h ∪In t → Out ′ h ∪ Out t such that C t • ψ C ′
h is closed and satisfiable. Since C ′ h is closed the function ψ is actually a mapping from In t to Out ′ h ∪ Out t . Let D be the subset of the domain of ψ of indexes i such that ψ(i) ∈ Out I , and D be its complement in the domain of ψ. Let us define from ψ and D two functions: In h ∪InI = ϕ Inh∪InI it is easy to see that:

ψ ′ = ψ | D ϕ ′ = ψ |D ∪ ϕ Let C ′′ h = C h • ψ ′ C t . Since by construction C I • ϕ ′ (C h • ψ ′ C t ) = C t • ψ (C h • ϕ C I ) and C t ∈ (C h • ϕ C I ) ⋆ the
Tr CI • ϕ ′ (C h • ψ ′ Ct) (C I ) = Tr CI •ϕC h (C I )
As a consequence the hypothesis

C I ∈ C sf h implies C I ∈ (C ′′ h ) sf .
The next step is to bound the size of the testing ASD C t obtained in Lemma 9. To this end, given an ASD C I ∈ C sf h we define:

χ(C I ) = {C t testing ASD | C t • C I ∈ C ⋆ h \ C ′ h ⋆ } i.e.
σ I = Tr CI •C h (C I ) σ ′ I = Tr CI •C ′ h (C I ) σ t = Tr Ct•CI •C h (C t ) σ ′ t = Tr C ′ t •CI •C h (C ′ t )
where the ASD C ′ t is constructed from C t as follows. We note that, if V t (i) = V t (j) for two distinct states i, j which are not reuse states, we can introduce a new variable x, change V t (j) to x, and introduce in S t a new test equation V t (i) ? = x. In other words we can assume wlog that V t is injective on states which are not reuse states. This permits one to ensure that the subset S d t of equations which are not test equations is satisfiable in any closed connection with another symbolic derivation. We define

σ d t = Tr C d t •CI •C ′ h (C d t )
. By the second point of Lemma 7 there exists a mapping ψ : Ind t → Ind I such that for every i ∈ Ind t we have V t (i)σ t = V I (ψ(i))σ I . Wlog we assume that ψ is defined as an extension of the connection between C I and C t , thereby ensuring that for input states i of C t we also have V

t (i)σ ′ t = V I (ψ(i))σ ′ I .
Claim 1. Wlog we can assume that for any deduction state i ∈ Ind t we have

V t (i)σ ′ t = V I (ψ(i))σ ′ I .
Proof of the claim. Let i ∈ Ind t be a deduction state such that V t (i)σ ′ t = V I (ψ(i))σ ′ I . Adding a reuse state if necessary, we can change i into an input state that is connected to ψ(t) (or a state which is a reuse of ψ(i)). This construction does not change σ t nor σ ′ t and thus the fact that

C t • C I • C h or C t • C I • C ′ h is satisfiable.
When repeatedly applying it, we obtain a symbolic derivation C t that satisfies the claim.

♦

We now split the analysis in two cases depending on whether the set = x 2 }, ∅, {1, 2}, ∅) where 1 is connected to ψ(i) and 2 is connected to ψ(j).

I t ⊆ Ind t of indexes i such that V t (i)σ ′ t = V I (ψ(i))σ ′ I is
On the other hand, if I t is not empty, let i 0 be minimal in this set, and let V t (i 0 ) ? = f (V t (i 1 ), . . . , V t (i n )) be the equation corresponding to this deduction state in S d t . Given the claim we can assume that i t is the first deduction state, and thus that all preceding states are input states. Thus there exists an ordering on the set Ind 0 = {t, 0, . . . , n} such that the following symbolic derivation is in χ(C I ) and satisfies the proposition:

(V : i ∈ Ind 0 → x i , {x 0 ? = f (x 1 , . . . , x n ) , x 0 ? = x t },
(C h • ϕ C t ) sf \ (C ′ h • ϕ C t ) ⋆ = ∅ implies C ⋆ h ⊆ C ′ h ⋆ .
Let us now prove the contrapositive of the converse implication and assume C ⋆ h ⊆ C ′ h ⋆ . By Proposition 2 there exists a symbolic derivation C I ∈ C sf h , a testing ASD C t and a connection ψ such that:

   C t • ψ C I ∈ C h ⋆ C t • ψ C I / ∈ C ′ h ⋆ C t contains
∆ = (C h • ϕ C t ) sf \ (C ′ h • ϕ C t ) ⋆ = ∅ Let C τ be
= ∅) C c • (C τ • ψ (C h • ϕ C t )) is satisfiable whereas, since C τ • ψ (C ′ h • ϕ C t ) is closed, C c • (C τ • ψ (C ′ h • ϕ C t )) is not. By Lemma 5 if C σ ∈ C ′ h ⋆ then so is C c • (C τ • ψ (C ′ h • ϕ C t )). Since C σ ∈ Σ implies C σ ∈ (C h • ϕ C t ) ⋆ we thus have C σ ∈ (C h • ϕ C t ) ⋆ \ (C ′ h • ϕ C t ) ⋆ .
⋆ h ⊆ C ′ h ⋆ .
As a trivial consequence we obtain the announced theorem.

Theorem 1, p. 21. Symbolic equivalence is decidable for finitary deduction systems.

Conclusion

We have introduced in this paper the notion of finitary deduction systems, and proved that symbolic equivalence is decidable for such attacker models. We believe that definition also captures the essence of lazy intruder techniques that are employed in many tools. Accordingly, we believe that a practical consequence of this paper will be the inclusion in existing reachability analysis tools of a symbolic equivalence checking algorithm.

In terms of comparison of expected runtimes for tools currently deciding reachability, a back-of-the-enveloppe computation for tools employing lazy constraint solving techniques such as OFMC [START_REF] Basin | Ofmc: A symbolic model checker for security protocols[END_REF] and CL-AtSe [START_REF] Turuani | The cl-atse protocol analyser[END_REF] would be twice (given that two protocols have to be analyzed and assuming tool is not parallelized) the runtime for safe (since these tools usually stop at the first attack found, and thus typically have a much shorter running time in these cases) protocols of a similar size. We refer the interested reader to [START_REF] Turuani | The cl-atse protocol analyser[END_REF] for more details, but given that CL-AtSe now implements a concurrent search algorithm and has been deployed on Amazon's EC2, we believe that less than 10s for reasonable industrial protocols is achievable nowadays.

{y 1 ?= A, y 2 ?= B, y 3 ? 4 ? 5 ? 6 ? 7 ?

 1234567 B, pk(A), pk(B), sk(A), N a} In = {9} Out = {7} S = = pk(A), y = pk(B), y = sk(A), y = enc p (y 5 , y 3 ), y 8 ? = f (y 6 ), y 10 ? = dec p (y 9 , y 5 ), y 10 ? = y 8 }

Figure 1 :

 1 Figure 1: Honest symbolic derivations of Example 2 with a connection corresponding to the intended communications and the test equations not shown

, 8, 8} S h = {x 0 ?= A, x 1 ?= B, x 2 ? 6 ?= dec p (x 5 , x 4 ), x 7 ?= f (x 6 ), x 8 ?

 012654768 = enc p (x 7 , x 2 )}

?= A, x 1 ?= B, x 2 ? 6 ?= dec p (x 5 , x 4 ), x 7 ?= f (x 6 ), x 8 ?= enc p (x 7 , x 2 ) y 0 ?= A, y 1 ?= B, y 2 ? 5 ?= n, z 6 ? 7 ?= f (z 5 ), z 8 ?= enc p (z 7 , z 2 ), z 9 ?= z 8 }

 126547687012567587298 B), sk(B), n} In = ∅ Out = Ind ∩ Ind ′ S = {x 0 = enc p (z 5 , z 3 ), z

Definition 9 (Example 4

 94 Honest symbolic derivations) A symbolic derivation C is an honest symbolic derivation or HSD, if the constants occurring in C are away from C new . The symbolic derivation for role B in Example 2 is honest.

{z 4 ?= n, z 5 ?= enc p (z 4 , z 3 ), z 6 ?= f (z 4 ), z 7 ?= enc p (z 6 , z 2 ), z 8 ?= z 7 }

 4546476287

Definition 13 (

 13 Deduction-only ASD) An ASD C I = (V I , S I , K I , In I , Out I ) is deduction-only if S I contains no equation V I (i) ? = V I (j). Definition 14 (Testing ASD) An ASD C I = (V I , S I , K I , In I , Out I ) is testing if K I = ∅. Definition 15 (Stutter-free ASDs) A well-formed deduction-only ASD is said to be stutter-free.

  we open C on C, and denote the operation open C (C), when for each c ∈ C: • If i ∈ Ind is the first knowledge state with V(i) ? = c ∈ S, we remove this equation from S and add i to the input states;

  and thus C ∩ Sub(S h ) = ∅. Let us denote S ′ I the unification system S I in which the equations x ? = c with c ∈ C are removed. For any substitution σ and any constant c ∈ C, Lemma 2 and σ |=

  a stutter-free symbolic derivation C C and a connection ϕ such that C C • ϕ open C (C I ) = C ′ I modulo a renaming of variables; • or there exists a set of memory states I ⊆ Ind ′ I such that C I is equal to C ′′ I = (V ′′ I , S ′′ I , K ′′ I , In ′′ I , Out ′′ I ) where:

  C h , ϕ)-well-formed ASD. Proof. Assume (C I , ϕ) ∈ C ⋆ h \ C ′ h ⋆ , and C I = (V I , S I , K I , In I , Out I ), and σ = Tr CI •ϕC h (C I ). By hypothesis σ satisfies S I . Let S 1 be the set of equations V I (i) ?

  an ASD in ∆. By definition of finitary deduction systems one can compute from C h • ϕ C t a finite set Σ of ASDs such that there exists C σ ∈ Σ and C c stutter free such that C ′ I ≤ C I • C c . By definition of the ordering there exists a stutter free derivation C θ and a set of constants C such that:open C (C σ ) • C θ = C τ • C cBy hypothesis there exists a connection functionψ such that C τ • ψ (C h • ϕ C t ) is closed and satisfiable whereas C τ • ψ (C ′ h • ϕ C t )is closed but not satisfiable. By Lemma 5 (employed with C

  Induction case: Assume there exists a unique ground substitution σ in normal

form with support: {V(j) | j < i} such that any unifier of S is an extension of σ. If i is a re-use state, we note that V(i) is already in the support of σ, and we are done. If it is a knowledge state, reasoning as in the basic case permits us to extend σ to V(i). If it is a deduction state then there exists in S an equation V(i) ?

  with disjoint sets of variables and index sets (Ind 1 , < 1 ) and (Ind 2 , < 2 ) respectively. Let I 1 , I 2 , be subsets of In 1 , In 2 , and O 1 , O 2 be sub-multisets of Out 1 , Out 2 respectively.

  Since the ASD is well-formed, all other equations in S VI (i) are of the form V I (i) I (j), and thus are already in S = . We obtain a new couple of ASDs (C ′ d , C ′ t ) by removing the state i from C d (and thus from the output variables of C d , removing i from the input states of C t , and adding the equation V I (i) (x 1 , . . . , x n ) to the unification system of C t , thereby making i a deduction state in C t .

? = V ? = f

  Lemma 9 Let C h and C ′ h be two HSDs. We have C ⋆ h ⊆ C ′⋆ h if, and only if: • C sf h ⊆ C ′⋆ h ; • and for each ASD C I ∈ C sf h and for all testing ASD C t ∈ (C I • C h ) ⋆ we have C t ∈ (C I • C ′ h ) ⋆ . ′⋆ h . By Lemma 8 we can assume wlog that C I = (V I , S I , K I , In I , Out I ) is well-formed. By Lemma 7 C I can be written C d • ϕ C t where C d is a stutter-free ASD and C t is a testing ASD. By construction we have

	Proof. Assume (C I , ψ) ∈ C ⋆ h \ C

  connection between C I and C ′′ h is also closed and satisfiable, and thus C I ∈ (C ′′ h ) ⋆ . Since C I ∈ C sf h the first two points of the definition of stutter free derivations are satisfied by C I . Given that:

	ϕ ′

  the set of testing ASDs that distinguish C h from C ′ h . By Lemma 9, C ⋆ h ⊆ C ′ h ⋆ if, and only if, there exists an ASD C I such that χ(C I ) = ∅. By ordering the equations in the unification system of an ASD C t ∈ χ(C I ) and keeping a minimal one, we prove that an ASD of bounded length can be constructed from C t . if, and only if, there exists C I ∈ C sf h such that χ(C I ) contains an ASD C t with at most one deduction and one equality test. ′ which are satisfied by Tr C ′ •C h (C ′ ) yields another symbolic derivation in C ′ ∈ C ⋆ h \ C ′ C ′ can be split into one stutter-free derivation C I = (V I , S I , K I , In I , Out I ) and one test derivation C t = (V t , S t , K t , In t , Out t ).

	Proposition 2 C ⋆ h ⊆ C ′ h ⋆ Proof. The converse direction is trivial.
	First let us note that if C ′ ∈ C ⋆ h \ C ′ Thus and wlog we let C ′ ∈ C ⋆ h \ C ′	h	⋆ .
		We also define a partition
	S d t ∪ S t t of S t such that S d t contains only deduction equations and S t t contains only test equations. Let C d t = (V

h ⋆ then, adding test equations to C h ⋆ be an aware ASD. According to Lemma 7 t , S d t , K t , In t , Out t ). Let us define the following substitutions:

  empty or not. If it is empty, the claim implies that we can assume there is no deduction states in C t , and thus that S t = S t t . Since C t • C I • C h is satisfiable but not C t • C I • C ′ h there exists two input states i, j and one equation V t (i) (j) in S t which is satisfied by σ t but not by σ ′ t . Thus χ(C I ) contains one symbolic derivation (V : i ∈ {1, 2} → x i , {x 1 ?

? = V t

  {t, 1, . . . , n}, ∅) Now we simply gather the results from Lemma 10 and Proposition 2. Given two HSDs C h and C ′ h we have C ⋆ h ⊆ C ′ h ⋆ if, and only if, there exists a symbolic testing derivation C t with at most one deduction state and one equality and a connection ϕ such that(C h • ϕ C t ) sf ⊆ (C ′ h • ϕ C t ) ⋆ .Proof. Let us first prove the contrapositive of the direct direction. Let C I be an ASD in(C h • ϕ C t ) sf \ (C ′ h • ϕ C t ) ⋆ ,and ψ be a connection such that:C I • ψ (C h • ϕ C t ) is closed and satisfiable C I • ψ (C ′ h • ϕ C t ) is closedand not satisfiableFrom ϕ and ψ we easily define two connections ϕ ′ and ψ ′ such thatC I • ϕ ′ C t is an ASD C ′ I such that C ′ I • ψ ′ C h isclosed and satisfiable whereas C ′ I • ψ ′ C ′ h is closed but not satisfiable. Hence:

	Proposition 3

  at most one deduction and one equality test ByLemma 10 this implies that there exists a connection ϕ such thatC I ∈ (C h • ϕ C t ) sf . Given the construction it is clear that C I / ∈ (C ′ h • ϕ C t ) ⋆ .The proof of the following theorem depends on the fact that for finitary deduction systems, the set min < ((C t • C h ) sf ) is by definition finite. The test of Proposition 3 thus becomes effective by Lemma 6 when a finite witness set is available.Theorem 2 (Inclusion of C⋆ h into C ′ h ⋆ ) Let D be a finitary deduction system. The inclusion C ⋆ h ⊆ C ′ h ⋆ is decidable for any two honest D-symbolic derivations C h , C ′ h .Proof. By Prop. 3 the inclusion does not hold if, and only if, there exists an ASD C t of bounded length and a connection function ϕ such that:

  Thus, if C h ⊆ C ′ h one can guess (in bounded time) a symbolic derivation C t and compute a finite Σ of symbolic derivations that contains one which is not in (C ′ h • C t ) ⋆ . Conversely it is clear if one such derivation is found then C

a restriction of symbolic equivalence in which the actions of all the honest agents are totally ordered.

Since the connection is closed the mapping is total.


Margit Kriegbaum
email: m.kriegbaum@pubhealth.ku.dk

Anne Mette Larsen

PhD Ulla Christensen

PhD a , Merete Osler DrMSc Rikke Lund

Merete Osler

Margit Kriegbaum Msc

MD Mette

Reduced probability of smoking cessation in men with increasing number of job losses and partnership breakdowns

Keywords: unemployment, marital status, smoking cessation, life-course

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

INTRODUCTION

Smoking is recognized as one of the most important causes of morbidity and premature mortality in industrialised countries. [1;2] Smoking cessation has an important impact in improving health. [START_REF] Bjartveit | Health consequences of sustained smoking cessation[END_REF] Most smokers start in their teenage years [START_REF] Chassin | The natural history of cigarette smoking: predicting young-adult smoking outcomes from adolescent smoking patterns[END_REF] and while the majority of those who start continue to smoke throughout their adult lives, [START_REF] Jarvis | A profile of tobacco smoking[END_REF] some smokers quit spontaneously. Socioeconomic differences exist in smoking cessation with the more advantaged being more likely to quit. [6;7] Other factors such as stressful life-events might play a role in smoking cessation. Some studies suggest that smoking is used to cope with stress and stressful life-events. [8;9] Unemployment and divorce or partnership breakdown are stressful life-events which may impede a change of lifestyle and hinder attempts to quit smoking. Few studies have focused on the association between these events and smoking cessation. Unemployed individuals have been reported to be less likely to quit smoking. [10;11] However, other studies did not find statistically significant differences. [START_REF] Chandola | Socio-demographic predictors of quitting smoking: how important are household factors?[END_REF] Among unemployed Fagan et al. [START_REF] Fagan | Cigarette smoking and quitting behaviors among unemployed adults in the United States[END_REF] found that the probability of quitting was higher among those unemployed for more than 6 months than for those unemployed for a shorter period. Furthermore, some studies have found that smoking predicted unemployment. [12;14] Married people have more success in quitting smoking compared to the never married, separated, and divorced. [12;15;16] Broms et al. [START_REF] Broms | Smoking cessation by socioeconomic status and marital status: the contribution of smoking behavior and family background[END_REF] found that living with a partner was not associated with smoking cessation.

However, in the same study, getting, or remaining married was associated with higher chances of smoking cessation in men compared to those who remain single in men. In a panel study by Nystedt [START_REF] Nystedt | Marital life course events and smoking behaviour in Sweden 1980-2000[END_REF] getting divorced was associated with lower chances of smoking cessation.

In life-course epidemiology the accumulation hypothesis states that the risk of poor health outcomes increases with the number of risk factors or duration of the exposure. This hypothesis has been tested related to cardiovascular disease, for which smoking is a major risk factor. To our knowledge, no studies have related accumulation of specific stressful life-events to smoking behaviours. In this study we examined the influence of history of unemployment and cohabitation over 22 years on smoking cessation. The aim of our study was to investigate the association between the history of unemployment and cohabitation and smoking cessation in midlife and to assess whether any association depends on the number of events or the duration of an unfavourable situation. Additionally, we set out to study how the joint exposure to history of unemployment and cohabitation is related to the probability of smoking cessation.

METHODS

This study is based on a subpopulation of the metropolit project, which comprises all 12,270 boys born within the metropolitan area of Copenhagen in 1953. In 1968, the Danish Civil Registration System (CRS) was established, and each Danish resident was registered with a personal identification number (PIN): The 11,532 members of the original metropolit population who survived until 1968 were given identification numbers by the authorities. Data from birth certificates were gathered in 1965. In 2004 the members of the cohort who were still alive and living in Denmark were sent a questionnaire about health behaviours social networks etc. Of the 9,507 eligible cohort members 6,292 (66.2 %) responded. Furthermore, the cohort was linked to registers with socioeconomic information in Statistics Denmark 1980-2003 using the PIN as a key and also with the Central Psychiatric Register and, the Central Hospital Register. We included only those from the 2004 survey participants who in addition to answering the questionnaire had a full record of register-data for the years 1980-2003 (N=6,232).

Outcome variables

The measure of smoking cessation was based on self-reported information from the 2004 survey. A recent review [START_REF] Gorber | The accuracy of selfreported smoking: a systematic review of the relationship between self-reported and cotinineassessed smoking status[END_REF] of the accuracy of self reported smoking found that there was under-reporting compared to its prevalence found by measurement of cotinine. The under-reporting of current smoking was more pronounced in groups in which smoking was stigmatized such as pregnant women and heart patients. The present study was based on middle-aged men from the general population and we do not judge that under-reporting is particularly pronounced in this group. The response to the question "Do you smoke?" was used to divide the participants into 3 groups: 1) current smokers (smoke on a daily basis and smoke but not every day) 2) ex-smokers 3) never smokers. The analyses of factors associated with smoking cessation were based on comparisons between ex-and current smokers, omitting the last category.

Assessment of history of cohabitation and labour-market participation

Information on history of unemployment and cohabitation was based on annual records from Statistics Denmark for the period 1980 to 2003 when cohort members were between 28 and 49 years old. Hence, it is possible to study the change of labour-market attainment as well as cohabitation status from one calendar-year to the next. Based on this information we constructed four exposure variables: number of job-losses, years unemployed, number of broken partnerships and years living without a partner.

Job-loss was defined as a change in individual labour-market participation that involved a period of unemployment and was categorized as follows: no job-losses (ref), one job-loss, two joblosses, three or more job-losses. Job-loss status was assigned to the categories based on change of employer's identification code. We restricted the category of job-loss to men who had been unemployed for at least three months of the calendar-year in order to exclude those who changed job with short or no intervening period of unemployment. Men with no job-losses were classified as continuously employed. Few (n=18) in the cohort were permanently outside the labour-market during the entire period and this group was pooled with the reference group i.e. those with no joblosses. [START_REF] Kriegbaum | Job losses and accumulated number of broken partnerships increase risk of premature mortality in Danish men born in 1953[END_REF] Years unemployed was based on information from Statistics Denmark about labourmarket status for each calendar-year, which was determined by the main source of income for that year. The group of unemployed comprises both individuals who were unemployed the entire calendar-year and those who had short spells of employment, but were mainly unemployed. We grouped the men as either working (employed or self employed) or not working (due to unemployment or for health reasons). Years unemployed was the sum of years in the non-working group between the ages of 28 and 49. This information was classified into four groups: no unemployment (ref), 1 to 5 years, 6 to 9 years and over 9 years of unemployment.

In this study, men living within either marriages (heterosexual and homosexual (allowed since 1989)) or consensual unions (heterosexual only) were grouped. Two individuals living at the same address were classified as a consensual union if they had common children or were of opposite sex, and both were at least 16 years old, and the age-difference was less than 15 years, and they were not related, and there were no other adults in the household. The partner's identification-number enabled to follow changes from one partner to another. We divided the cohort members into five groups according to their history of cohabitation between 1980 and 2003: 1) consistently cohabiting with the same partner (ref), 2) never cohabited, not living with a partner at any time during this period, 3) one broken partnership, 4) two broken partnerships, 5) three or more broken partnerships. We maintained the "never cohabited" as a separate group because of its size (n=314) and because other studies of this cohort [START_REF] Lund | Marital history from age 15 to 40 years and subsequent 10year mortality: a longitudinal study of Danish males born in 1953[END_REF] and of other populations [START_REF] Modin | Born out of wedlock and never married--it breaks a man's heart[END_REF] have indicated high mortality in this group. A broken partnership was defined as the end of cohabitation. The classification comprises individuals who were formerly cohabiting but during any year were living without a partner or with a new partner. Very few of the married men became widowers (n=40) during follow-up and these cases were classified as broken partnerships. [START_REF] Kriegbaum | Job losses and accumulated number of broken partnerships increase risk of premature mortality in Danish men born in 1953[END_REF] Years living without a partner was based on information from Statistics Denmark about cohabiting partners for each calendar-year assessed as described above. The sum of years in the ages 28-49 years the individual lived without a partner was classified in four groups (always living with a partner (ref), 1 to 5 years, 6 to 9 years and above 9 years).

Assessment of covariates

In this study we included information about psychiatric admissions that occurred before the measurement of job-losses and broken partnerships as confounders, while later admissions, which might be a consequence of these events, were not included. Information about admission to a psychiatric ward was obtained from the Central Psychiatric Register for the period 1968 to 1981, when the cohort members were 15 to 28 years old. We coded the admissions as either no admissions or at least one admission. From the social registers from 1980, we used 'educational attainment coded into 'high' (at least secondary education) and 'low' (primary education only). Age at smoking initiation has been related to later "smoking career". [START_REF] Khuder | Age at smoking onset and its effect on smoking cessation[END_REF] Those who start to smoke early may experience poor health at a young age which might influence their labour-market participation and family-life. However, there is no agreement about which age of smoking initiation is critical for later smoking outcomes. We included information on age at smoking initiation as reported in the questionnaire from 2004 and used different cut-points between the ages of 11 and 16 and found that the younger at smoking initiation the less likelihood of quitting smoking. However, the choice of cut-point did not change the association between exposures and smoking cessation. In the final analyses, we used 13 years as the cut-point. This corresponds to 22 % of the cohortmembers. We included the amount of tobacco smoked (currently for current smokers and in the past for ex-smokers) from self-reported accounts of numbers of cigarettes, pipes, cigarillos, and cigars per day and calculated the amount of tobacco per day in grams.

Statistical methods

We used logistic regression to analyse the associations between smoking cessation and history of cohabitation and job-losses. The analyses were based on men who had smoked at some time (n=4,665), i.e. leaving out never smokers. We analysed the four exposure variables (number of joblosses, number of broken partnerships,length of periods of unemployment living without a partner) in a series of separate models (one to five) where the covariates were included one at the time. In a sixth model we adjusted number of job-losses for number of broken partnerships and years without employment for years living without a partner.

The score test in 'proc logistic' was used to test for trend (Cochran Armitage test) in models with exposure-variables included as continuous variables. Statistical interaction was tested by adding an interaction term to the models. However, the separate and joint effects were showed as by two new composite variables 1) the categories of job-loss were grouped as none versus any; and the categories of broken partnerships were grouped as none, never cohabited, and at least one broken partnership. The variables for job-losses and broken partnerships were combined leaving six combinations, the doubly-unexposed group being used as reference group. 2) time unemployed and time living without a partner was combined as unexposed to both, exposed to unemployment (1 or more years), exposed to living alone (1 or more years) and exposed to both. SAS (ver. 9,1) was used for all analysis.

RESULTS

Of the 6,262 cohort members included in this study 2,646 (42.5 %) were smokers at the time of the survey, 2,019 (32.4 %) had quit smoking, and 1,567 (25.1 %) had never smoked. Table 1 shows the distribution of smoking status in relation to job-losses, broken partnerships, years of unemployment, years living without a partner, educational attainment, psychiatric admissions, age at smoking initiation and mean amount of tobacco consumed. Compared to ex-smokers and to never smokers, current smokers more often experienced job-losses, broken partnerships, and longer periods of unemployment or of living without a partner. Those with less education, psychiatric admissions, and those who started smoking at age 13 or younger were more likely to be current smokers. Table 2 shows the crude and adjusted odds of smoking cessation. The probability of smoking cessation decreases with the number of job-losses and broken partnerships. Living without a partner for more than five years was associated with poorer chance of smoking cessation, and this was further decreased among those living without a partner for more than nine years. However, living without a partner for between one and five years was not associated with smoking cessation. All estimates indicated that the risk of smoking increased with the number of stressful events or duration of exposure. The tests for trend all confirmed this association (p<0.0001). We found that the covariates attenuated the associations to a smaller extent. Finally, we included job-losses and broken partnerships in the same model and similarly for years unemployed and years living without a partner which attenuated the estimates to a larger degree.

We tested statistical interaction between history of unemployment and history of cohabitation in the probability of smoking cessation in two models: interaction between job-losses and broken partnership (p=0.04) and interaction between years unemployed and years living without a partner (p=0.76). Table 3 shows the separate and joint effects. Those with combined exposure of job-loss and broken partnership have a low probability of smoking cessation compared to the reference group and to those with just one of the exposures. Moreover, the never cohabitant who experienced one or more job-losses had a five times lower probability of smoking cessation compared to the doubly-unexposed group. The combined exposure to time living without a partner and time without employment was also associated with lower probability of smoking cessation.

DISCUSSION

In this study we found consistent support for the accumulation hypothesis as both number of jobloss and broken partnerships were inversely related to smoking cessation. Furthermore, the chance of smoking cessation decreased with duration of unemployment and of living without a partner.

Those with exposure to both job-losses and broken partnerships had low probability of smoking cessation; and particularly the never cohabiting with job-losses had low probability of smoking cessation.

We found no studies that investigated accumulation of the same factors related to smoking cessation. However, some studies have focused on related issues and some have linked accumulation of social risk factors to health behaviours. Nystedt [START_REF] Nystedt | Marital life course events and smoking behaviour in Sweden 1980-2000[END_REF] investigated the associations between smoking behaviour and marital life-course changes. He found that those who divorced or had never cohabited were less likely to cease smoking while this did not apply to those with multiple changes in marital status. However, multiple marital changes and divorce was associated with starting to smoke. The multiple marital changes in Nystedt´s study are not entirely comparable to the present study as they might involve multiple changes in an out of marriage as a result of divorce, remarriage and widowhood while the present study considered only cessation of partnerships. Montgomery et al. [START_REF] Montgomery | Health and social precursors of unemployment in young men in Great Britain[END_REF] found that the risk of being a smoker increased with time spent unemployed between the ages of 16 and 33. Although these studies use different smoking outcomes, they both agree with the present study in that the accumulation of exposures related to the labour-market is associated with smoking behaviours.

Strengths and limitations

This study used prospectively collected information; the measures of history of employment and cohabitation were based on register data, which provided complete histories of cohabitation and employment from 1980 to 2003 of all cohort members who were alive and living in Denmark during this period. This allows studying both number of events and duration of exposures in a 22year period. However, register data was limited in that they are based on annual information only.

Register data were not available before 1980 when the cohort members were 28 years old; however we believe that the participation in labour-market and family-life is important in the ages 28 to 49 years. The non-respondents of the questionnaire had poorer socioeconomic characteristics than responders. However, a previous study of loss to follow-up in the same population showed that the association with smoking outcomes was similar in respondents and non-respondents. [START_REF] Osler | Rapid report on methodology: does loss to follow-up in a cohort study bias associations between early life factors and lifestyle-related health outcomes?[END_REF] This study included only men and mainly heterosexual relationships, and it is very likely that exposures related to labour-market and family-life affect women differently. [START_REF] Mckee | Sex differences in the effects of stressful life events on changes in smoking status[END_REF] Smoking status can change several times and these changes have been related to job-losses and broken partnerships in other studies. [26;27] However, smoking was measured only once in the metropolit project and we were not able to study how exposures were related to changes in smoking behaviours.

We found that the association between history of unemployment and smoking cessation differed when history of cohabitation was included and vice versa. In this study design it was not possible to determine whether they each acted as confounders or as mediators for each other as they were measured during the same time span. We found that the associations between history of unemployment and partnership and smoking were affected to a small degree by inclusion of psychiatric admissions. However, this might be due to the fact that only the more severe cases of psychiatric illness are registered in hospital records. Milder cases of mental disorders might influence on the results, but unfortunately this information was unavailable. Further, factors such as social support, depression and nicotine dependence were either unmeasured or measured simultaneous with the outcome. Thus, future studies with information on the temporal order of these factors could spread light on the role of these in relation to accumulated events and smoking behaviours. Future life-course studies that include both disease outcomes and behavioural variables could focus on the question of whether the association between accumulated social risk factors and disease are mediated by health behaviours.

In conclusion, the results of the present study indicate that exposure to accumulated stressful life events, or longer periods of exposure are associated with lower probability of smoking cessation. Those unemployed for more than nine years have a low probability of ceasing to smoke.

As this group has no, or very infrequent, contact with the labour-market they do not benefit from smoking-reduction programmes provided at work. The never cohabited also have low probability of smoking cessation; job-loss worsens the chance of quitting. These groups could be targets for special attention from general practitioners. Furthermore, universal policies such as regulation of tobacco could have an effect on these groups.

Table 1 :

 1 Distribution (in number and %) of history of job-losses and history of cohabitation (age 28-50 years), educational attainment and psychiatric admission in relation to smoking in men aged 51

	History of job-losses/unemployment	Current	Ex smoker	Never smoker
	(1980-2003)	smoker	2019	1567
		2646
	No job-losses	1672 (63.2%)	1586 (78.6%)	1297 (82.8 %)
	1 job-loss	547 (20.7%)	278 (13.8 %)	178 (11.4 %)
	2 job-losses	250 (9.5%)	93 (4.6 %)	52 (3.3 %)
	3+ job-losses	177 (6.7%)	62 (3.1 %)	40 (2.6 %)
	Time unemployed	1162 (43.9%)	1169 (57.9 %)	1038 (66.2 %)
	1-5 years	924 (34.9%)	673 (33.3 %)	445 (28.4 %)
	6-9 years	228 (8.6%)	88 (4.4 %)	49 (3.1 %)
	10-23 years	332 (12.6%)	89 (4.4 %)	35 (2.2 %)
	Continuously cohabited (1980-2003)	947 (35.8%)	970 (48.0 %)	752 (48.0 %)
	Never cohabited 1980-2003	202 (7.6%)	69 (3.4 %)	103 (6.6 %)
	1 Broken partnership	790 (29.3%)	599 (29.7 %)	435 (27.8 %)
	2 Broken partnership	426 (13.9%)	251 (12.4 %)	187 (11.9 %)
	3+ Broken partnership	281 (10.6%)	130 (6.4 %)	90 (5.7 %)
	Time living without a partner	697 (26.3%)	685 (33.9 %)	495 (31.6 %)
	1-5 years	703 (26.6%)	672 (33.3 %)	490 (31.3 %)
	6-9 years	346 (13.1%)	269 (13.3 %)	200 (12.8 %)
	10-23 years	900 (34.0%)	393 (19.5 %)	382 (24.4 %)
	High educational attainment	1534 (58.0%)	1395 (69.1 %)	1205 (76.9 %)
	Low educational attainment	1112 (42.0%)	624 (30.9 %)	362 (23.1 %)
	No psychiatric admissions	2535 (95.8%)	1975( 97.8 %)	1553 (99.1 %)
	Psychiatric admissions	111 (4.2%)	44 (2.2 %)	14 (0.9 %)
	Started smoking at 14 or older	1988 (77.7 %) 1569 (83.8 %)	NA
	Started smoking at 13 or younger	571 (22.3 %)	304 (16.3 %)	NA
	Nicotine consumption g/day mean	20.8 (13.0)	21.3 (16.5)	NA
	(SD)

Table 3 :

 3 Adjusted Odds Ratios (OR) and 95 % Confidence Intervals (CI) for smoking cessation in relation to combinations of history of cohabitation and job-losses (age 28-39)

		No of cases	OR (95 % CI)
	No broken partnerships, no job-	707	1 (ref.)
	loss
	Never cohabitant, no job-loss	83	0.43 (0.29-0.65)
	Broken partnership,	825	0.77 (0.66-0.89)
	No job-loss
	No broken partnership,+ job-loss	213	0.68 (0.53-0.86)
	Never cohabitant, + job-loss	113	0.19 (0.12-0.30)
	Broken partnership,	618	0.37 (0.31-0.45)
	+ job-loss
	Time unemployed and living with
	a partner
	No years unemployed and no	456	1 (ref.)
	years living without a partner
	No years unemployed, 1+ year	617	0.81 (0.68-0.96)
	living without a partner
	1+ year unemployed, no years	176	0.69 (0.55-0.88)
	living without a partner
	1+ year unemployed and 1+ year	624	0.50 (0.43-0.59)
	living without a partner

Acknowledgement:

The authors thank K Svalastoga, E Høgh, P Wolf, T Rishøj, G Strande-Sørensen, E Manniche, B Holten, I A Weibull and A Ortmann who established the data between 1965 and 1983.

Funding:

The Danish Medical Research Council, The Danish Health Insurance Fund, Wedell-Wedellsborg Foundation, Krista and Viggo Petersen Foundation. The funding bodies have not influenced the analysis of data or their interpretation.

License statement: "The Corresponding Author has the right to grant on behalf of all authors and does grant on behalf of all authors, an exclusive licence (or non exclusive for government employees) on a worldwide basis to the BMJ Publishing Group Ltd to permit this article (if accepted) to be published in JECH and any other BMJPGL products and sublicences such use and exploit all subsidiary rights, as set out in our licence (http://jech.bmj.com/site/about/licence.pdf)."