Typing and Compositionality for Security Protocols: A Generalization to the Geometric Fragment

Context and Motivation. Relative soundness results have proved helpful in the automated verification of security protocols as they allow for the reduction of a complex verification problem into a simpler one, if the protocol in question satisfies sufficient conditions. These conditions are of a syntactic nature, i.e., can be established without an exploration of the state space of the protocol.

A first kind of such results are typing results [4, 6, 13, 18]. In this paper, we consider a typed model, a restriction of the standard protocol model in which honest agents do not accept any ill-typed messages. This may seem unreasonable at first sight, since in the real-world agents have no way to tell the type of a random bitstring, let alone distinguish it from the result of a cryptographic operation; yet in the model, they “magically” accept only well-typed messages. The relative soundness of such a typed model means that if the protocol has an attack, then it also has a well-typed attack. This does not mean that the intruder cannot send ill-typed messages, but rather that this does not give him any advantage as he could perform a “similar” attack with only well-typed messages. Thus, if we are able to verify that a protocol is secure in the typed model, then it is secure also in an untyped model. Typically, the conditions sufficient to achieve such a result are that all composed message patterns of the protocol have a different (intended) type that can somehow be distinguished, e.g., by a tag. The restriction to a typed model in some cases yields a decidable verification problem, allows for the application of more tools and often significantly reduces verification time in practice [5, 6].

A similar kind of relative soundness results appears in compositional reasoning. We consider in this paper the parallel composition of protocols, i.e., running two protocols over the same communication medium, and these protocols may use, e.g., the same long-term public keys. (In the case of disjoint cryptographic material, compositional reasoning is relatively straightforward.) The compositionality result means to show that if two protocols satisfy their security goals in isolation, then their parallel composition is secure, provided the protocols meet certain sufficient conditions. Thus, it suffices to verify the protocols in isolation. The sufficient conditions in this case are similar to the typing result: every composed message can be uniquely attributed to one of the two protocols, which again may be achieved, e.g., by tags.

Contributions. Our contributions are twofold. First, we unify and thereby simplify existing typing and compositionality results: we recast them as an instance of the same basic principle and of the same proof technique. In brief, this technique is to reduce the search for attacks to solving constraint reduction in a symbolic model. For protocols that satisfy the respective sufficient conditions, constraint reduction will never make an ill-typed substitution, where for compositionality “ill-typed” means to unify messages from two different protocols.

Second, this systematic approach also allows us to significantly generalize existing results to a larger set of protocols and security properties. For what concerns protocols, our soundness results do not require a particular fixed tagging scheme like most previous works, but use more liberal requirements that are satisfied by many existing real-world protocols like TLS.

While many existing results are limited to simple secrecy goals, we prove our results for the entire geometric fragment suggested by Guttman [11]. We even augment this fragment with the ability to directly refer to the intruder knowledge in the antecedent of goals; while this does not increase expressiveness, it is very convenient in specifications. In fact, handling the geometric fragment also constitutes a slight generalization of existing constraint-reduction approaches.

Organization. In Sects. 2 and 3, we introduce a symbolic protocol model based on strands and properties in the geometric fragment. In Sect. 4, we reduce verification of the security properties to solving constraints. In Sects. 5 and 6, we give our typing and parallel compositionality results. In Sect. 7, we introduce a tool that checks if protocols are parallel-composable and report about first experimental results. In Sect. 8, we conclude and discuss related work. Proof sketches are in the appendix.

2.1 Messages

Let \(\varSigma \) be a finite set of operators (also referred to as function symbols); as a concrete example, Table 1 shows a \(\varSigma \) that is representative for a wide range of security protocols. Further, let \(\mathcal {C}\) be a countable set of constants and \(\mathcal {V}\) a countable set of variables, such that \(\varSigma \), \(\mathcal {V}\) and \(\mathcal {C}\) are pairwise disjoint. We write \(\mathcal {T}_{\varSigma \cup \mathcal {C}}(\mathcal {V})\) for the set of terms built with these constants, variables and operators, and \(\mathcal {T}_{\varSigma \cup \mathcal {C}}\) for the set of ground terms. We call a term t atomic (and write \( atomic (t)\)) if \(t \in \mathcal {V}\cup \mathcal {C}\), and composed otherwise. We use also other standard notions such as subterm, denoted by \(\sqsubseteq \), and substitution, denoted by \(\sigma \).

The set of constants \(\mathcal {C}\) is partitioned into three countable and pairwise disjoint subsets: (i) the set \(\mathcal {C}_{P_i}\) of short-term constants for each protocol \(P_i\), denoting the constants that honest agents freshly generate in \(P_i\); (ii) the set \(\mathcal {C}_{priv}\) of long-term secret constants; and (iii) the set \(\mathcal {C}_{pub}\) of long-term public constants. This partitioning will be useful for compositional reasoning: roughly speaking, we will allow the intruder to obtain all public constants, and define that it is an attack if the intruder finds out any of the secret constants.

2.2 Formats

We use in this paper a notion of formats that is crucial to make our typing and compositionality results applicable to real-world protocols like TLS. Here, we break with the formal-methods tradition of representing clear-text structures of data by a pair operator \((\cdot ,\cdot )\). For instance, a typical specification may contain expressions like \(( A,NA )\) and \(( NB,(KB,A) )\). This representation neglects the details of a protocol implementation that may employ various mechanisms to enable a receiver to decompose a message in a unique way (e.g., field-lengths or XML-tags). The abstraction has the disadvantage that it may easily lead to false positives and false negatives. For example, the two messages above have a unifier \(A \mapsto NB \) and \( NA \mapsto ( KB,NA )\), meaning that a message meant as \(( A,NA )\) may accidentally be parsed as \(( NB,(KB,A) )\), which could lead to a “type-flaw” attack. This attack may, however, be completely unrealistic in reality.

To handle this, previous typing results have used particular tagging schemes, e.g., requiring that each message field starts with a tag identifying the type of that field. Similarly, compositionality results have often required that each encrypted message of a protocol starts with a tag identifying the protocol that this message was meant for. Besides the fact that this does not really solve the problem of false positives and false negatives due to the abstraction, practically no existing protocol uses exactly this schema. Moreover, it is completely unrealistic to think that a widely used protocol like TLS would be changed just to make it compatible with the assumptions of an academic paper — the only chance to have it changed is to point out a vulnerability that can be fixed by the change.

Formats are a means to have a faithful yet abstract model. We define formats as functions from data-packets to concrete strings. For example, a format from TLS is \(\mathbf{client\_hello(time,\,random, \,session\_id,\,cipher\_suites, }\,\mathbf{comp\_ }\,\mathbf{methods) } = \mathsf {byte}(1)\cdot \mathsf {off}_{3}(\mathsf {byte}(3) \ \cdot \mathsf {byte}(3)\cdot time \cdot random \cdot \mathsf {off}_{1}( session\_id ) \cdot \ \mathsf {off}_{2}( cipher\_suites ) \cdot \mathsf {off}_{1}( comp\_methods )) \), where \(\mathsf {byte}(n)\) means one concrete byte of value n, \(\mathsf {off}_{k}(m)\) means that m is a message of variable length followed by a field of k bytes, and \(\cdot \) represents string concatenation.

In the abstract model, we are going to use only abstract terms like the part in bold in the above example. It is shown in [19] that under certain conditions on formats this abstraction introduces neither false positives nor false negatives. The conditions are essentially that formats must be parsed in an unambiguous way and must be pairwise disjoint; then every attack on the concrete bytestring model can be simulated in the model based on abstract format symbols (in the free algebra). Both in typing and compositionality, these conditions allow us to apply our results to real world protocols no matter what formatting scheme they actually use (e.g., a TLS message cannot be accidentally be parsed as an EAC message). In fact, these reasonable conditions are satisfied by many protocols in practice, and whenever they are violated, typically we have a good chance to find actual vulnerabilities.

We will model formats as transparent in the sense that if the intruder learns \(\mathsf {f}(t_1,\ldots ,t_n)\), then he also obtains the \(t_i\).

2.3 Intruder Knowledge and Deduction Rules

We specify how the intruder can compose and decompose messages in the style of the Dolev-Yao intruder model.

Definition 1

An intruder knowledge M is a finite set of ground terms \(t\in \mathcal {T}_{\varSigma \cup \mathcal {C}}\). Let \(\mathtt {Ana}(t)=(K,T)\) be a function that returns for every term t a pair (K, T) of finite sets of subterms of t. We define \(\vdash \) to be the least relation between a knowledge M and a term t that satisfies the following intruder deduction rules:

The rules (Axiom) and (Public) formalize that the intruder can derive any term \(t \in M\) that is in his knowledge and every long-term public constant \(c \in \mathcal {C}_{pub}\), respectively, and the (Compose) rule formalizes that he can use compose known terms with any operator in \(\varSigma \) (where n denotes the arity of f). Table 1 provides an example \(\varSigma \) for standard cryptographic operators, along with the \(\mathtt {Ana}\) function defined for each of them, which are available to all agents, including the intruder.

For message decomposition, we namely rely on analysis rules for terms in the form of \(\mathtt {Ana}(t)=(K,T)\), which intuitively says that if the intruder knows the keys in set K, then he can analyze the term t and obtain the set of messages T. We require that all elements of K and T are subterms of t (without any restriction, the relation \(\vdash \) would be undecidable). Consider, e.g., the analysis rule for symmetric encryption given in Table 1: \(\mathtt {Ana}(\mathsf {scrypt}(k,m))=(\{k\},\{m\})\) says that given a term \(\mathsf {scrypt}(k,m)\) one needs the key \(\{k\}\) to derive \(\{m\}\). By default, atomic terms cannot be analyzed, i.e., \(\mathtt {Ana}(t)=(\emptyset ,\emptyset )\). The generic (Decompose) deduction rule then formalizes that for any term with an \(\mathtt {Ana}\) rule, if the intruder can derive the keys in K, he can also derive all the subterms of t in T.

We define the following notions. A protocol consists of a set of operational strands (an extension of the strands of [12]) and a set of goal predicates that the protocol is supposed to achieve. The semantics of a protocol is an infinite-state transition system over symbolic states and security means that all reachable states satisfy the goal predicates. A symbolic state \((\mathcal {S};M;E;\phi )\) consists of a set \(\mathcal {S}\) of operational strands (representing the honest agents), the intruder knowledge M, a set E of events that have occurred, and a symbolic constraint \(\phi \) on the free variables occurring in the state. We first define constraints, then operational strands, the transition relation on symbolic states, and finally the goal predicates.

3.1 Symbolic Constraints

The syntax of symbolic constraints is

where s, t range over terms in \(\mathcal {T}_{\varSigma \cup \mathcal {C}}(\mathcal {V})\), M is a finite set of terms (not necessarily ground) and \(\bar{x}\) is list of variables. The sublanguage \(\phi _\sigma \) defines equations on messages, and we can existentially quantify variables in them, e.g., consider a \(\phi \) of the form \(\exists x.\, y \doteq f(x)\). We refer to equations also as substitutions since the application of the standard most general unifier on a conjunction of equations results in a set of substitutions. The constraints can contain such substitutions in positive and negative form (excluding all instances of a particular substitution).

\(M\vdash t\) is an intruder constraint: the intruder must be able to derive term t from knowledge M. Note that we have no negation at this level, i.e., we cannot write negated intruder constraints. A base constraint is a constraint built according to this grammar without the two cases marked \(\star \), i.e., disjunction \(\phi \vee \phi \) and existential quantification \(\exists \bar{x}.\, \phi \), which may only occur in negative substitutions.

For ease of writing, we define the semantics of the constraint language as standard for each construct (rather than following strictly the grammar of \(\phi \)).

Definition 2

Given an interpretation \(\mathcal {I}\), which maps each variable in \(\mathcal {V}\) to a ground term in \(\mathcal {T}_{\varSigma }\), and a symbolic constraint \(\phi \), the model relation \(\mathcal {I}\,\models \,\phi \) is:

We say that \(\mathcal {I}\) is a model of \(\phi \) iff \(\mathcal {I}\,\models \, \phi \), and that \(\phi \) is satisfiable iff it has a model. Two constraints are equivalent, denoted by \(\equiv \), iff they have the same models. We define as standard the variables, denoted by \( var (\cdot )\), and the free variables, denoted by \( fv (\cdot )\), of terms, sets of terms, equations, and constraints. A constraint \(\phi \) is closed, in symbols \( closed (\phi )\), iff \( fv (\phi )=\emptyset \).

Every constraint \(\phi \) can be quite straightforwardly transformed into an equivalent constraint of the form

where the \(\phi _i\) are base constraints. Unless noted otherwise, in the following we will assume that constraints are in this form.

Definition 3

A constraint is well-formed if each of its base constraints \(\phi _i\) satisfies the following condition: we can order the conjuncts of \(\phi _i\) such that \(\phi _i= M_1\vdash t_1 \wedge \ldots \wedge M_n\vdash t_n \wedge \phi _i'\), where \(\phi _i'\) contains no further \(\vdash \) constraints and such that \(M_j \subseteq M_{j+1}\) (for \(1 \le j<n\)) and \( fv (M_j) \subseteq fv (t_1)\cup \ldots \cup fv (t_{j-1})\).

Intuitively, this condition expresses that the intruder knowledge grows monotonically and all variables that occur in an intruder knowledge occur in a term that the intruder sent earlier in the protocol execution. We will ensure that all constraints that we deal with are well-formed.

3.2 Operational Strands

In the original definition of [21], a strand denotes a part of a concrete protocol execution, namely, a sequence of ground messages that an agent sends and receives. We introduce here an extension that we call operational strands, where terms may contain variables, there may be positive and negative equations on messages, and agents may create events over which we can formulate the goals:

where \(\phi _\sigma \) is as defined above; we will omit the parentheses when there is no risk of confusing the dots. \( fv \) and \( closed \) extend to operational strands as expected, with the exception of the receiving step, which can bind variables: we set \( fv (\mathsf {receive}(t). S )= fv ( S )\setminus fv (t)\). According to the semantics that we define below, in \(\mathsf {receive}(x).\mathsf {receive}( f (x)).\mathsf {send}(x).0\) the variable x is bound actually in the first receive, i.e., the strand is equivalent to \(\mathsf {receive}(x).\mathsf {receive}(y).(y \doteq f (x)).\mathsf {send}(x).0\) .

A symbolic state \((\mathcal {S};M;E;\phi )\) consists of a (finite or countable) set^{Footnote 1} \(\mathcal {S}\) of closed operational strands, a finite set M of terms representing the intruder knowledge, a finite set E of events, and a formula \(\phi \). \( fv (\cdot )\) and \( closed \) extend to symbolic states again as expected. We ensure that \( fv (\mathcal {S})\cup fv (M)\cup fv (E)\subseteq fv (\phi )\) for all reachable states \((\mathcal {S};M;E;\phi )\), and that \(\phi \) is well-formed. This is so since in the transition system shown shortly, the operational strands of the initial state are closed and the transition relation only adds new variables in the case of \(\mathsf {receive}(t)\), but in this case \(\phi \) is updated with \(M\vdash t\).

A protocol specification \((\mathcal {S}_0,G)\) (or simply protocol) consists of a set \(\mathcal {S}_0\) of closed operational strands and a set G of goal predicates (defined below). For simplicity, we assume that the bound variables of any two different strands in \(\mathcal {S}_0\) are disjoint (which can be achieved by \(\alpha \)-renaming). The strands in \(\mathcal {S}_0\) induce an infinite-state transition system with initial state \((\mathcal {S}_0;\emptyset ;\emptyset ;\top )\) and a transition relation \(\Rightarrow \) defined as the least relation closed under six transition rules:

1. T1

   \((\{\mathsf {send}(t). S \}\cup \mathcal {S};M;E;\phi )\Rightarrow (\{ S \}\cup \mathcal {S};M\cup \{t\};E;\phi )\)

2. T2

   \((\{\mathsf {receive}(t). S \}\cup \mathcal {S};M;E;\phi )\Rightarrow (\{ S \}\cup \mathcal {S};M;E;\phi \wedge M\vdash t)\)

3. T3

   \((\{\mathsf {event}(t). S \}\cup \mathcal {S};M;E;\phi )\Rightarrow (\{ S \}\cup \mathcal {S};M;E\cup \mathsf {event}(t);\phi )\)

4. T4

   \((\{\phi '. S \}\cup \mathcal {S};M;E;\phi )\Rightarrow (\{ S \}\cup \mathcal {S};M;E;\phi \wedge \phi ')\)

5. T5

   \((\{ 0 \}\cup \mathcal {S};M;E;\phi )\Rightarrow (\mathcal {S};M;E;\phi )\)

6. T6

   \((\mathcal {S};M;E;\phi )\Rightarrow (\mathcal {S};M;E\cup \{ lts (c)\};\phi )\) for every \(c\in \mathcal {C}_{priv}\)

The rule T1 formalizes that sent messages are added to the intruder knowledge M. T2 formalizes that an honest agent receives a message of the form t, and that the intruder must be able to create that message from his current knowledge, expressed by the new constraint \(M\vdash t\); this indirectly binds the free variables of the rest of the strand in the sense that they are now governed by the constraints of the state. (In a non-symbolic model, one would at this point instead need to consider all ground instances of t that the intruder can generate.) T3 formalizes that we add events to the set E. T4 simply adds the constraint \(\phi '\) to the constraint \(\phi \). T5 says that if a strand reaches \(\{0\}\), then we remove it. Finally, for every secret constant c in \(\mathcal {C}_{priv}\), T6 adds the event \( lts (c)\) to the set E. (We define later as a goal that the intruder never obtains any c for which \( lts (c)\in E\).) We cannot have this in the initial set E as we need it to be finite; this construction is later crucial in the parallel composition proof as we can at any time blame a protocol (in isolation) that leaks a secret constant. We discuss below that in practice this semantic rule does not cause trouble to the verification of the individual protocols.

3.3 Goal Predicates in the Geometric Fragment

We express goals by state formulas in the geometric fragment [11]. Here, we also allow to directly talk about the intruder knowledge, but in a restricted manner so that we obtain constraints of the form \(\phi \). Security then means: every reachable state in the transition system induced by \(\mathcal {S}_0\) satisfies each state formula, and thus an attack is a reachable state where at least one goal does not hold.

The constraints \(\phi \) we have defined above are interpreted only with respect to an interpretation of the free variables, whereas the state formulas are evaluated with respect to a symbolic state, including the current intruder knowledge and events that have occurred (as before, we define the semantics for each construct).

Definition 4

State formulas \(\varPsi \) in the geometric fragment are defined as:

where \(\mathsf {ik}(t)\) denotes that the intruder knows the term t. \( fv (\cdot )\) and \( closed \) extend to state formulas as expected. Given a state formula \(\varPsi \), an interpretation \(\mathcal {I}\), and a state \(\mathfrak {S}=(\mathcal {S};M;E;\phi )\), we define \(\mathcal {I},M,E\,\models _{\mathfrak {S}}\,\varPsi \) as:

Definition 5

A protocol \(P=( \mathcal {S}_0, \{\varPsi _0,\cdots , \varPsi _n\})\), where the \(\varPsi _i\) are closed state formulas, has an attack against goal \(\varPsi _i\) iff there exist a reachable state \(\mathfrak {S}=(\mathcal {S}; M; E;\phi )\) in the transition system induced by \(\mathcal {S}_0\) and an interpretation \(\mathcal {I}\) such that \(\mathcal {I},M,E\,\models _{\mathfrak {S}}\, \lnot \varPsi _i\) and \(\mathcal {I}\,\models _{\mathfrak {S}}\, \phi \). We also call \(\mathfrak {S}\) an attack state in this case.

Note that in this definition the interpretation \(\mathcal {I}\) does not matter in \(\mathcal {I},M,E\,\models _{\mathfrak {S}}\, \lnot \varPsi _i\) because \(\varPsi _i\) is closed.

Example 1

If a protocol generates the event^{Footnote 2} \(\mathsf {secret}(x_A,x_B,x_m)\) to denote that the message \(x_m\) is supposed to be a secret between agents \(x_A\) and \(x_B\), and—optionally—the event \(\mathsf {release}(x_m)\) to denote that \(x_m\) is no longer a secret, then we can formalize secrecy via the state formula \(\forall x_A x_B x_m. (\mathsf {secret}(x_A,x_B,x_m)\wedge \mathsf {ik}(x_m)\implies x_A=\mathsf {i}\vee x_B=\mathsf {i}\vee \mathsf {release}(x_m))\), where \(\mathsf {i}\) denotes the intruder. The release event can be used to model declassification of secrets as needed to verify perfect forward secrecy (when other data should remain secret even under the release of temporary secrets). We note that previous compositionality approaches do not support such goals. A typical formulation of non-injective agreement [15] uses the two events \(\mathsf {commit}(x_A, x_B, x_m)\), which represents that \(x_A\) intends to send message \(x_m\) to \(x_B\)), and \(\mathsf {running}(x_A,x_B,x_m,x_C)\), which represents that \(x_B \) believes to have received \(x_m\) from \(x_A\), with \(x_C\) a unique identifier: \(\forall x_A x_B x_m x_C.\, ( \mathsf {running}(x_A,x_B, x_m,x_C) \implies \mathsf {commit}(x_A,x_B,x_m) \vee x_A = \mathsf {i}\vee x_B = \mathsf {i})\), and injective agreement would additionally require: \(\forall x_A x_B x_m x_C x_C'.\, \mathsf {running}(x_A,x_B,x_m,x_C)\wedge \mathsf {running}(x_A,x_B,x_m,x_C') \implies x_A=\mathsf {i}\vee x_B=\mathsf {i}\vee x_C=x_C'\).   \(\square \)

We first show how to translate every state formula \(\varPsi \) in the geometric fragment for a given symbolic state \(\mathfrak {S}=(\mathcal {S};M;E;\phi )\) into a constraint \(\phi '\) (in the fragment defined in Sect. 3.1) so that the models of \(\phi \wedge \phi '\) represent exactly all concrete instances of \(\mathfrak {S}\) that violate \(\varPsi \). Then, we extend a rule-based procedure to solve \(\phi \)-style constraints (getting them into an equivalent simple form). This procedure provides the basis for our typing and parallel composition results.

4.1 From Geometric Fragment to Symbolic Constraints

Consider a reachable symbolic state \((\mathcal {S};M;E;\phi )\) and a goal formula \(\varPsi \). As mentioned earlier, we require that \(\varPsi \) is closed. Let us further assume that the bound variables of \(\varPsi \) are disjoint from the variables (bound or free) of \(\mathcal {S}\), M, E, and \(\phi \). We now define a translation function \( tr _{M,E}(\varPsi )=\phi '\) where \(\phi '\) represents the negation of \(\varPsi \) with respect to intruder knowledge M and events E. The negation is actually manifested in the first line of the definition:

Theorem 1

Let \(\mathfrak {S}=(\mathcal {S}; M; E; \phi )\) be a symbolic state and \(\varPsi \) a formula in the geometric fragment such that \( fv (\varPsi )=\emptyset \) and \( var (\varPsi )\cap var (\phi )=\emptyset \). For all \(\mathcal {I}\,\models \, \phi \), we have \(\mathcal {I},M,E{\,\models _{\mathfrak {S}}\,} \lnot \varPsi \ \text { iff } \ \mathcal {I}\,\models \, tr _{M,E}(\varPsi )\). Moreover, if \(\phi \) is well-formed, then so is \(\phi \wedge tr _{M,E}(\varPsi )\).

4.2 Constraint Reduction

As mentioned before, we can transform any well-formed constraint into the form \(\phi \equiv \exists \bar{x}. \phi _0\vee \ldots \vee \phi _n\), where \(\phi _i\) are base constraints, i.e., without disjunction and existential quantification (except in negative substitutions). We now discuss how to find the solutions of such well-formed base constraints. Solving intruder constraints has been studied quite extensively, e.g., in [7, 16, 18, 20], where the main application of constraints was for efficient protocol verification for a bounded number of sessions of honest agents. Here, we use constraints rather as a proof argument for the shape of attacks. Our result is of course not restricted to a bounded number of sessions as we do not rely on an exploration of reachable symbolic states (that are indeed infinite) but rather make an argument about the constraints in each of these states.

We consider constraint reduction rules of the form \(\dfrac{\phi '}{\phi }\) expressing that \(\phi '\) entails \(\phi \) (if the side condition \( cond \) holds). However, we will usually read the rule backwards, i.e., as: one way to solve \(\phi \) is \(\phi '\).

Definition 6

The satisfiability calculus for the symbolic intruder comprises the following constraint reduction rules:

where \((M' \vdash t)^{T\gg M}\) is \(M' \cup T \vdash t \) if \(M \subseteq M'\) and \(M' \vdash t\) otherwise, \((\cdot )^{T\gg M}\) extends as expected, \( eq (\sigma ) = x_1 \doteq t_1 \wedge \ldots \wedge x_n \doteq t_n\) is the constraint corresponding to a substitution \(\sigma = [x_1 \mapsto t_1, \ldots , x_n \mapsto t_n]\), and \( mgu (s \doteq t)\) is the standard most general unifier for the pair of terms t and s (in the free-algebra).

Recall that the \( mgu \), if it exists, is unique modulo renaming (\( mgu \) extends as expected). Let us now explain the rules. \(( Unify )\) expresses that one way to generate a term t from knowledge M is to use any term \(s\in M\) that can be unified with t, but one commits in this case to the unifier \(\sigma \); this is done by applying \(\sigma \) to the rest of the constraint and recording its equations. \(( Unify )\) cannot be applied when s or t are variables; intuitively: when t is a variable, the solution is an arbitrary term, so we consider this a solved state (until elsewhere a substitution is required that substitutes t); when s is variable, then it is a subterm of a message that the intruder created earlier. If the earlier constraint is already solved (i.e., a variable) then s is something the intruder could generate from an earlier knowledge and thus redundant.

\(( Equation )\), which similarly allows us to solve an equation, can be applied if s or t are variables, provided the conditions are satisfied, but later we will have to prevent vacuous application of this rule to its previous result, i.e., the equations \( eq (\sigma )\). \(( PubConsts )\) says that the intruder can generate all public constants.

\(( Compose )\) expresses that one way to generate a composed term \(f(t_1,\ldots ,t_n)\) is to generate the subterms \(t_1,\ldots ,t_n\) (because then f can be applied to them). \(( Decompose )\) expresses that we can attempt decryption of any term in the intruder knowledge according to the \(\mathtt {Ana}\) function. Recall that Table 1 provides examples of \(\mathtt {Ana}\), and note that for variables or constants Table 1 will yield \((\emptyset ,\emptyset )\), i.e., there is nothing to analyze. However, if there is a set T of messages that can potentially be obtained if we can derive the keys K, and T is not yet a subset of the knowledge M anyway, then one way to proceed is to add \(M\vdash k\) for each \(k\in K\) to the constraint store, i.e., committing to finding the keys, and under this assumption we may add T to M and in fact to any knowledge \(M'\) that is a superset of M. Also for this rule we must prevent vacuous repeated application, such as applying analysis directly to the newly generated \(M\vdash k\) constraints.

The reduction of constraints deals with conjuncts of the form \(M\vdash t\) and \(s\doteq t\). However, we also have to handle negative substitutions, i.e., conjuncts of the form \(\lnot \exists \bar{x}.\phi _\sigma \). We show that we can easily check them for satisfiability.

Definition 7

A constraint \(\phi \) is simple, written \( simple (\phi )\), iff \(\phi = \phi _1 \wedge \ldots \wedge \phi _n\) such that for each \(\phi _i\) (\(1 \le i \le n\)):

• if \(\phi _i = M \vdash t\), then \(t\in \mathcal {V}\);

• if \(\phi _i = s \doteq t\), then \(s \in \mathcal {V}\) and s does not appear elsewhere in \(\phi \);

• if \(\phi _i=\lnot \exists \bar{x}.\phi _\sigma \), then \( mgu (\theta (\phi _\sigma ))=\emptyset \) for \(\theta =[\bar{y}\mapsto \bar{c}]\) where \(\bar{y}\) are the free variables of \(\phi _i\) and \(\bar{c}\) fresh constants that do not appear in \(\phi \).

Theorem 2

If \( simple (\phi )\), then \(\phi \) is satisfiable.

Theorem 3

(Adaption of [18, 20]). The satisfiability calculus for the symbolic intruder is sound, complete, and terminating on well-formed constraints.

In our typed model, the set of all possible types for terms is denoted by \(\mathcal {T}_{\varSigma \cup \mathfrak {T}_{a}}\), where \(\mathfrak {T}_{a}\) is a finite set of atomic types, e.g., \(\mathfrak {T}_{a}=\{ Number , Agent , PublicKey , PrivateKey , SymmetricKey \}\). We call all other types \({ composed\,types}\). Each atomic term (each element of \(\mathcal {V}\cup \mathcal {C}\)) is given a type; constants are given an atomic type and variables are given either an atomic or a composed type (any element of \(\mathcal {T}_{\varSigma \cup \mathfrak {T}_{a}}\)). We write \(t:\tau \) to denote that a term t has the type \(\tau \). Based on the type information of atomic terms, we define the typing function \(\varGamma \) as follows:

Definition 8

Given \(\varGamma (\cdot ): \mathcal {V}\rightarrow \mathcal {T}_{\varSigma \cup \mathfrak {T}_{a}}\) for variables and \(\varGamma (\cdot ): \mathcal {C}\rightarrow \mathfrak {T}_{a}\) for constants, we extend \(\varGamma \) to map all terms to a type, i.e., \(\varGamma (\cdot ) : \mathcal {T}_{\varSigma \cup \mathcal {C}}(\mathcal {V})\rightarrow \mathcal {T}_{\varSigma \cup \mathfrak {T}_{a}}\), as follows: \(\varGamma (t)= f (\varGamma (t_1), \cdots , \varGamma (t_n))\) if \(t= f (t_1, \cdots , t_n)\) and \( f \in \varSigma ^n\). We say that a substitution \(\sigma \) is well-typed iff \(\varGamma (x) =\varGamma (\sigma (x))\) for all \(x\in dom (\sigma )\).

For example, if \(\varGamma (k) = PrivateKey \) and \(\varGamma (x) = Number \) then \(\varGamma (\mathsf {crypt}(\mathsf {pub}(k), x)) = \mathsf {crypt}(\mathsf {pub}( PrivateKey ), Number )\).

As we require that all constants be typed, we further partition \(\mathcal {C}\) into disjoint countable subsets according to different types in \(\mathfrak {T}_{a}\). This models the intruder’s ability to access infinite reservoirs of public fresh constants. For example, for protocols \(P_1,P_2\) and \(\mathfrak {T}_{a}=\{\beta _1, \ldots , \beta _n\}\), we have the disjoint subsets \(\mathcal {C}_{pub}^{\beta _i}\), \(\mathcal {C}_{priv}^{\beta _i}\), \(\mathcal {C}_{P_1}^{\beta _i}\) and \(\mathcal {C}_{P_2}^{\beta _i}\), where \(i \in \{1,\ldots ,n\}\) and, e.g., \(\mathcal {C}_{pub}^{\beta _i}\) contains all \(\mathcal {C}_{pub}\) elements of type \(\beta _i\). \(\mathcal {C}_{P_1}^{\beta _i}\) and \(\mathcal {C}_{P_2}^{\beta _i}\) are short-term constants, whereas \(\mathcal {C}_{pub}^{\beta _i}\) and \(\mathcal {C}_{priv}^{\beta _i}\) are long-term, and we consider it an attack if the intruder learns any of \(\mathcal {C}_{priv}^{\beta _i}\).

By an easy induction on the structure of terms, we have:

Lemma 1

If a substitution \(\sigma \) is well-typed, then \(\varGamma (t)= \varGamma (\sigma (t))\) for all terms \(t\in \mathcal {T}_{\varSigma \cup \mathcal {C}}(\mathcal {V})\).

According to this typed model, \(\mathcal {I}\) is a well-typed interpretation iff \(\varGamma (x) = \varGamma (\mathcal {I}(x))\) for all \(x\in \mathcal {V}\). Moreover, we require for the typed model that \(\varGamma (s) = \varGamma (t)\) for each \(s \doteq t\). This is a restriction only on the strands of the honest agents (as they are supposed to act honestly), not on the intruder: he can send ill-typed messages freely. We later show that sending ill-typed messages does not help the intruder in introducing new attacks in protocols that satisfy certain conditions.

5.1 Message Patterns

In order to prevent the intruder from using messages of a protocol to attack a second protocol, we need to guarantee the disjointness of the messages between both protocols. Thus, we use formats to wrap raw data, as discussed in Sect. 2.2. In particular, all submessages of all operators (except formats and public key operator) must be “wrapped” with a format, e.g., \(\mathsf {scrypt}(k, \mathsf {f}_a( Na ))\) and \(\mathsf {scrypt}(k, \mathsf {f}_b( Nb ))\) should be used instead of \(\mathsf {scrypt}(k, Na )\) and \(\mathsf {scrypt}(k_1, Nb )\).

We define the set of protocol message patterns, where we need to ensure that each pair of terms has disjoint variables: we thus define a well-typed \(\alpha \)-renaming \(\alpha (t)\) that replaces the variables in t with completely new variable names.

Definition 9

The message pattern of a message t is \( MP (t) = \{\alpha (t)\}\). We extend \( MP \) to strands, goals and protocols as follows. The set \( MP (S)\) of message patterns of a strand S and the set \( MP (\varPsi )\) of message patterns of a goal \(\varPsi \) are defined as follows:

The set of message patterns of a protocol \(P=( \{ S _1,\cdots , S _m\};\{\varPsi _0,\cdots , \varPsi _n\})\) is \( MP (P) = \bigcup \limits {_{i=1}^m} MP ( S _i) \cup \bigcup \limits {_{i=1}^n} MP (\varPsi _i)\), and the set of sub-message patterns of a protocol P is \( SMP (P) =\{\alpha (s) \mid t\in MP (P) \wedge s\sqsubseteq t \wedge \lnot atomic(s) \}\setminus \{u \mid u=pub(v)\text { for some term }v\}\). \( SMP \) applies to messages, strands, goals as expected.

Example 2

If \(S= \mathsf {receive}(\mathsf {scrypt}(k,(\mathsf {f}_1(x,y)))).\mathsf {send}(\mathsf {scrypt}(k,y))\), then \( SMP (S) = \{\mathsf {scrypt}(k,\mathsf {f}_1(x_1,y_1)),\mathsf {scrypt}(k,y_2), \mathsf {f}_1(x_3,y_3)\}\).    \(\square \)

Definition 10

A protocol \(P = (\mathcal {S}_0,G)\) is type-flaw-resistant iff the following conditions hold:

• \( MP (P)\) and \(\mathcal {V}\) are disjoint, i.e., \( MP (P) \cap \mathcal {V}= \emptyset \) (which ensures that none of the messages of P is sent as raw data).

• If two non-atomic sub-terms are unifiable, then they have the same type, i.e., for all \(t_1,t_2\in SMP (P)\), if \(\sigma (t_1)=\sigma (t_2)\) for some \(\sigma \), then \(\varGamma (t_1)=\varGamma (t_2)\).

• For any equation \(s\doteq t\) that occurs in strands or goals of P (also under a negation), \(\varGamma (s)=\varGamma (t)\).

• For any variable x that occurs in equations or events of G, \(\varGamma (x)\in \mathfrak {T}_{a}\).

• For any variable x that occurs in inequalities or events of strands, \(\varGamma (x)\in \mathfrak {T}_{a}\).

Intuitively, the second condition means that we cannot unify two terms unless their types match. Note that this match is a restriction on honest agents only, the intruder is still able to send ill-typed messages.

Example 3

Example 2 included a potential type-flaw vulnerability as \(\mathsf {scrypt}(k, \mathsf {f}_1(x_1,y_1))\) and \(\mathsf {scrypt}(k, y_2)\) have the unifier \([y_2\mapsto \mathsf {f}_1(x_1,y_1)]\). Here \(y_1\) and \(y_2\) must have the same type since they have been obtained by a well-typed variable renaming in the construction of \( SMP \). Thus, the two messages have different types. The problem is that the second message encrypts raw data without any information on who it is meant for and it may thus be mistaken for the first message. Let us thus change the second message to \(\mathsf {scrypt}(k, \mathsf {f}_2(y_2))\). Then \( SMP \) also includes \(\mathsf {f}_2(y_4)\) for a further variable \(y_4\), and now no two different elements of \( SMP \) have a unifier. \(\mathsf {f}_2\) is not necessarily inserting a tag: if the type of y in the implementation is a fixed-length type, this is already sufficient for distinction.    \(\square \)

Theorem 4

If a type-flaw-resistant protocol P has an attack, then P has a well-typed attack.

Note that this theorem does not exclude that type-flaw attacks are possible, but rather says that for every type-flaw attack there is also a (similar) well-typed attack, so it is safe to verify the protocol only in the typed model.

In this section, we consider the parallel composition of protocols, which we often abbreviate simply to “composition”. We define the set of operational strands for the composition of a pair of protocols as the union of the sets of the operational strands of the two protocols; this allows all possible transitions in the composition. The goals for the composition are also the union of the goals of the pair, since any attack on any of them is an attack on the whole composition (i.e., the composition must achieve the goals of the pair).

Definition 11

The parallel composition \(P_1 \parallel P_2\) of \(P_1 = ( S _0^{P_1}; \varPsi _0^{P_1})\) and \(P_2 = ( S _0^{P_2}; \varPsi _0^{P_2})\) is \(P_1 \parallel P_2 = ( S _0^{P_1} \cup S _0^{P_2};\, \varPsi _0^{P_1} \cup \varPsi _0^{P_2})\).

Our parallel composition result relies on the following key idea. Similar to the typing result, we look at the constraints produced by an attack trace against \(P_1 \parallel P_2\), violating a goal of \(P_1\), and show that we can obtain an attack against \(P_1\) alone, or a violation of a long-term secret by \(P_2\). Again, the core of this proof is the observation that the unification steps of the symbolic intruder never produce an “ill-typed” substitution in the sense that a \(P_1\)-variable is never instantiated with a \(P_2\) message and vice versa. For that to work, we have a similar condition as before, namely that the non-atomic subterms of the two protocols (the SMPs) are disjoint, i.e., each non-atomic message uniquely says to which protocol it belongs. This is more liberal than the requirements in previous parallel compositionality results in that we do not require a particular tagging scheme: any way to make the protocol messages distinguishable is allowed. Further, we carefully set up the use of constants in the protocol as explained at the beginning of Sect. 5, namely that all constants used in the protocol are: long-term public values that the intruder initially knows; long-term secret values that, if the intruder obtains them, count as a secrecy violation in both protocols; or short-term values of \(P_1\) or of \(P_2\).

The only limitation of our model is that long-term secrets cannot be “declassified”: we require that all constants of type private key are either part of the long-term secrets or long-term public constants. Moreover, the intruder can obtain all public keys, i.e., \(\mathsf {pub}(c)\) for every c of type private key. This does not prevent honest agents from creating fresh key-pairs (the private key shall be chosen from the long-term constants as well) but it dictates that each private key is either a perpetual secret (it is an attack if the intruder obtains it) or it is public right from the start (as all public keys are). This only excludes protocols in which a private key is a secret at first and later revealed to the intruder, or where some public keys are initially kept secret.

Definition 12

Two protocols \(P_1\) and \(P_2\) are parallel-composable iff the following conditions hold:

1. (1)

   \(P_1\) and \(P_2\) are \( SMP \) -disjoint, i.e., for every \(s\in SMP (P_1)\) and \(t\in SMP (P_2)\), either s and t have no unifier (\( mgu (s \doteq t) = \emptyset \)) or \(s=\mathsf {pub}(s_0)\) and \(t=\mathsf {pub}(t_0)\) for some \(s_0,t_0\) of type private key.

2. (2)

   All constants of type private key that occur in \( MP (P_1)\cup MP (P_2)\) are part of the long-term constants in \(\mathcal {C}_{pub}\cup \mathcal {C}_{priv}\).

3. (3)

   All constants that occur in \( MP (P_i)\) are in \(\mathcal {C}_{pub}\cup \mathcal {C}_{priv}\cup \mathcal {C}_{P_i}\), i.e., are either long term or belong to the short-term constants of the respective protocol.

4. (4)

   For every \(c \in \mathcal {C}_{P_i}^{ PrivateKey }\), \(P_i\) also contains the strand \(\mathsf {send}(\mathsf {pub}(c)).0\).

5. (5)

   For each secret constant \(c \in \mathcal {C}_{priv}^{\beta _i}\), for each type \(\beta _i\), each \(P_i\) contains the strands \(\mathsf {event}(lts_{\beta _i,P_i}(c)).0\) and the goal \(\forall x:\beta _i.\, \mathsf {ik}(x) \implies \lnot lts_{\beta ,P_i}(x)\).

6. (6)

   Both \(P_1\) and \(P_2\) are type-flaw resistant.

Some remarks on the conditions: (1) is the core of the compositionality result, as it helps to avoid confusion between messages of the two protocols; (2) ensures that every private key is either initially known to the intruder or is part of the long-term secrets (and thus prevents “declassification” of private keys as we discussed above). (3) means that the two protocols will draw from disjoint sets of constants for their short-term values. (4) ensures that public keys are known to the intruder. Note that typically the goals on long-term secrets, like private keys and shared symmetric keys, are very easy to prove as they are normally not transmitted. The fact that we do not put all public keys into the knowledge of the intruder in the initial state is because the intruder knowledge must be a finite set of terms for the constraint reduction to work. Putting it into strands means they are available at any time, but the intruder knowledge in every reachable state (and thus constraint) is finite. Similarly, for the goals on long-term secrets: the set of events in every reachable state is still finite, but for every leaked secret, we can in one transition reach the corresponding predicate that triggers the secrecy violation goal. (5) ensures that when either protocol \(P_i\) leaks any constant of \(\mathcal {C}_{priv}^{\beta _i}\), it is a violation of its secrecy goals. (6) ensures that for both protocols, we cannot unify terms unless their types match.

Theorem 5

If two protocols \(P_1\) and \(P_2\) are parallel-composable and both \(P_1\) and \(P_2\) are secure in isolation in the typed model, then \(P_1 \parallel P_2\) is secure (also in the untyped model).

We can then apply this theorem successively to any number of protocols that satisfy the conditions, in order to prove that they are all parallel composable.

This compositionality result entails an interesting observation about parallel composition with insecure protocols: unless one of the protocols leaks a long-term secret, the intruder never needs to use one protocol to attack another protocol. This means actually: even if a protocol is flawed, it does not endanger the security of the other protocols as long as it at least manages not to leak the long-term secrets. For instance, the Needham-Schroeder Public Key protocol has a well-known attack, but the intruder can never obtain the private keys of any honest agent. Thus, another protocol relying on the same public-key infrastructure is completely unaffected. This is a crucial point because it permits us to even allow for security statements in presence of flawed protocols:

Corollary 1

Consider two protocols \(P_1\) and \(P_2\) that are parallel-composable (and thus satisfy all the conditions in Definition 12). If \(P_1\) is secure in isolation and \(P_2\), even though it may have an attack in isolation, does not leak a long-term secret, then all goals of \(P_1\) hold also in \(P_1 \parallel P_2\).

We have developed the Automated Protocol Composition Checker APCC (available at http://www2.compute.dtu.dk/~samo/APCC.zip), a tool that verifies the two main syntactic conditions of our results: it checks both if a given protocol is type-flaw-resistant and if the protocols in a given set are pairwise parallel-composable. In our preliminary experiments, we considered a suite that includes widely used protocols like TLS, Kerberos (PKINIT and Basic) and protocols defined by the ISO/IEC 9798 standard, along with well-known academic protocols (variants of Needham-Schroeder-Lowe, Denning-Sacco, etc.). Although we worked with abstract and simplified models, we were able to verify that TLS and Kerberos are parallel-composable. In contrast, since some protocols of the ISO/IEC 9798 standard share common formats, they are not \( SMP \)-disjoint.

Another result is that many academic protocols are not pairwise parallel-composable. This was largely expected because they do not have a standardized implementation, and thus the format of messages at the wire level is not part of the specification. In fact, in these protocols there are several terms that may be confused with terms of other protocols, whereas a concrete implementation may avoid this by choosing carefully disjoint messages formats that can prevent the unification. Hence, our tool APCC can also support developers in the integration of new protocols (or new implementations of them) in an existing system.

This paper unifies research on the soundness of typed models (e.g., [4, 6, 13, 18]) and on parallel protocol composition (e.g., [2, 8–10, 12]) by using a proof technique that has been employed in both areas: attack reduction based on a symbolic constraint systems. For typing, the idea is that the constraint solving never needs to apply ill-typed substitutions if the protocol satisfies some sufficient conditions; hence, for every attack there exists a well-typed variant and it is thus without loss of generality to restrict the model to well-typed execution. For the parallel composition of \(P_1\) and \(P_2\) that again satisfy some sufficient conditions, the constraint solving never needs to use a message that the intruder learned from \(P_1\) to construct a message of \(P_2\); thus, the attack will work in \(P_1\) alone or in \(P_2\) alone, and from verifying them in isolation, we can conclude that their composition is secure.

We also make several generalizations over previous results. First, we are not limited to a fixed set of properties like secrecy [3, 6]. Instead, we consider the entire geometric fragment proposed by Guttman [11] that we believe is the most expressive language that can work with the given constraint-solving argument that is at the core of handling typing and compositionality results uniformly. Other expressive property languages have been considered, e.g., PS-LTL for typing results [4]; an in-depth comparison of the various existing property languages and their relative expressiveness is yet outstanding. Another common limitation is to rely on a fixed public key infrastructure, e.g., [3, 4, 8]. Our approach in contrast allows for the exchange of public keys (including freshly generated ones). Moreover, early works on typing and parallel composition used a fixed tagging scheme, whereas we use the more general notion of non-unifiable subterms for messages that have different meaning. Using the notion of formats, our results are applicable to existing real-world protocols like TLS with their actual formats.

Our work considered so far protocols only in the initial term algebra without any algebraic properties. There are some promising results for such properties (e.g., [9, 14, 17]) that we would like to combine with our approach. The same holds for other types of protocol composition, e.g., the sequential composition considered in [9], where one protocol establishes a key that is used by another protocol as input.