1 Introduction

When analyzing the security of protocols, one aims at proving specific security properties. The most common types of properties are secrecy, meaning that an intruder cannot know a secret value, and authentication, meaning that if A thinks he is talking to B, then he is really talking to B. In our digitalized world there are more and more cryptographic protocols everywhere, and we want to verify them to ensure their security.

It is not realistic to assume that a protocol is running alone in the network, and in the real world, an intruder can try to use messages of other protocols in the network to break a protocol. That is what we call a multi-protocol attack.

More precisely, we study the following problem of multi-protocols attacks. Given two protocols that ensure a certain security property in isolation, are they still safe for this property if we put them together in the same network? Unsurprisingly there exist many combinations of protocols where this is not the case, i.e., where we can mount multi-protocols attacks.

There are a lot of tools for automatic analysis of security properties, like ProVerif [3], AVISPA [2], Athena [27], Scyther [12], or Tamarin [23]. But they are generally used to analyze the security of a protocol executed in isolation, meaning that each agent only executes the analyzed protocol. In this paper, our aim is also to automatically find multi-protocols attacks using Tamarin .

Contributions: Several multi-protocols attacks have been found manually or using other tools, our aim is to find them automatically using the Tamarin prover [23]. Our contributions are the following:

  • We automatically find all the manual attacks described in [22]. Moreover, we find novel different attacks on the same properties, or unknown attacks on different properties. This demonstrates the limitations of a manual approach for finding attacks. It underlines that automatic verification is a very efficient approach for analyzing the security of cryptographic protocols.

  • We analyzed all the protocols given in [9], where the authors used Scyther, a different protocol verification tool. We confirm the results from Scyther using Tamarin.

  • We developed an algorithm to simplify the process of creating the multi-protocol specification file in Tamarin from the individual protocol specifications. The algorithm also automatically generates necessary helping lemmas in Tamarin in order to verify the combination of the two protocols more efficiently. The algorithm is implemented in Python, and available online [15].

Related work: The existence of multi-protocol attack have been introduced by Kelsey, Schneier, and Wagner in [18]. In this paper the attacks were found manually and the authors consider protocols crafted to break other protocols.

In [22], Mathuria, Raj Singh, Venkata Sharavan, and Kirtankar found six multi-protocol attacks based on 13 protocols from literature: Denning-Sacco protocol [13], amended Woo-Lam protocol [5], ISO Five-Pass protocol [7], Abadi-Needham protocol [1], six protocols from Perrig and Song using APG [26], and three protocols from Zhou and Foley using ASPB [30]. In contrast to these works, we use an automatic verification tool to find these attacks.

Cremers found many multi-protocol attacks in [9], using the tool Scyther, with 30 protocols from literature including Needham Schroeder protocol [24], Needham Schroeder symmetric key protocol [24], Needham Schroeder symmetric key amended protocol [25], Lowe’s modified version of the Needham Schroeder protocol [19], SPLICE/AS [29], Hwang and Chen’s version of SPLICE/AS [16], Clark and Jacob’s version of SPLICE/AS [8], a basic SOPH example (Secret-Out Public-Home), Woo Lam pi f [28], Kao Chow v.1, v.2 and v.3 [17], Yahalom’s protocol [4], and Lowe’s version of Yahalom protocol [21]. Compared to this work we use the Tamarin instead of Scyther.

There is also a considerable amount of work of preventing multi-protocol attacks by construction using special composition frameworks. These frameworks exist in the computational (e.g., Universal Composability [6]) and in the symbolic setting (e.g., Protocol Composition Logic [14]).

Outline: The paper is structured as follows. In Sect. 2, we present the results we obtain and we compare them with those obtained manually in [22] or using Scyther [9]. Then, Sect. 3 discusses our workflow in Tamarin , and finally the last section concludes the paper.

2 Multi-protocol Attacks

First we define the properties that we want to verify for each protocol. We define one property for secrecy and two authentication properties.

  • Secrecy [10]: if A claims the secrecy of a variable \(N_A\) at the end of the run of the protocol, then an intruder cannot know this variable.

  • Non-injective agreement [11]: if a protagonist A completes a run apparently with B, then B has run the protocol with A and A agrees with all other protagonist on all values. This is not exactly the same definition as in [20], but we keep this definition because it is this one that is used by Scyther.

  • Non-injective synchronisation [11]: if a protagonist A completes a run as the initiator apparently with B as the responder, then B has run the protocol as the responder with A, and all messages sent and received are exactly like described in the specification of the protocol, in the same order.

We call a type-flaw attack an attack where the intruder uses data of a different type than the data expected by the protocol. For example, in such an attack, the intruder could use two nonces \(N_1\), \(N_2\) instead of another single nonce N (\(N=(N_1,N_2)\)), or uses an ID as a nonce. We consider separately the case where the intruder can make type-flaw attacks (such attacks are valid) and the case where the intruder cannot (such attacks are not valid).

All our Tamarin files are available online [15].

2.1 Attacks by Cremers [9]

First we study the protocols analyzed in [9] using Scyther. We modeled all these protocols individually in Tamarin . Figure 1 presents our results using Tamarin for the properties described previously, and Fig. 2 presents our results for multi-protocols using Tamarin , where we verify the properties for the first of the two protocols. In these figures, ni-synch stands for non-injective synchronisation, sec stands for secrecy and ni-agree stands for non-injective agreement. Moreover, means that we did not find any attacks, and means there is at least one attack for the property. A yellow box means that the first protocol (the one for which we verify the security properties in the combination) is safe for this property in isolation, and red box means that both protocols are safe for this property in isolation. Empty box means that the property is not relevant for this protocol, for example the key \(K_{AB}\) does not exist in the protocol in the property secrecy A \(K_{AB}\) and secrecy B \(K_{AB}\), or a protagonist A never obtains a nonce \(N_B\) in the property secrecy A \(N_B\).

We find the same results with Tamarin as with Scyther. We do not consider type-flaw attack for these protocols, because the number of combination with multi-protocol attack is too large (more than 100 different combinations) to model them all manually with Tamarin . All timings are calculated with 6 CPUs of 2 GHz and 32 GB of memory.

Fig. 1.
figure 1

Results found using Tamarin with NS = Needham Schroeder [24], NSS = Needham Schroeder Symmetric Key [24], NSSA = Needham Schroeder Symmetric Key Amended [25], NSL = Needham Schroeder Lowe [19], AS = SPLICE/AS [29], AShc = Hwang and Chen version of SPLICE/AS [16], AScj = Clark and Jacob version of SPLICE/AS [8], K = Kao Chow [17], K2 = Kao Chow v.2 [17], K3 = Kao Chow v.3 [17], WLpif = Woo Lam pi f [28], Y = Yahalom [4], YL = Yahalom Lowe [21], soph = a SOPH basic example. ni-synch denotes non-injective synchronisation, ni-agree denotes non-injective agreement, and sec A \(N_A\) denotes the fact that A claims the secrecy of \(N_A\).

Full size image
Fig. 2.
figure 2

Result found with Tamarin . NS = Needham Schroeder [24], NSS = Needham Schroeder Symmetric Key [24], NSSA = Needham Schroeder Symmetric Key Amended [25], NSL = Needham Schroeder Lowe [19], AS = SPLICE/AS [29], AShc = Hwang and Chen’s version of SPLICE/AS [16], AScj = Clark and Jacob’s version of SPLICE/AS [8], K = Kao Chow [17], K2 = Kao Chow v.2 [17], K3 = Kao Chow v.3 [17], WLpif = Woo Lam pi f [28], Y = Yahalom [4], YL = Yahalom Lowe [21], soph = a SOPH basic example. ni-synch denotes non-injective synchronisation, ni-agree denotes non-injective agreement, and sec A \(N_A\) denotes fact that A claims the secrecy of \(N_A\). * = the first protocol is safe in isolation, ** = both protocol are safe in isolation (Color figure online)

Full size image

We can see in Fig. 2 that even if two protocols are safe in isolation for a property, it is not guaranteed that the combination of this two protocols is safe too if they share keys, and multi-protocol attacks are not only due to the other protocol that is not safe for this property.

We would expect that Tamarin takes more time to analyze properties for multi-protocols than for protocols in isolation, due to the increased number of transitions and the larger number of traces with the new protocol.

But as we can see in Figs. 1 and 2, this is not always the case, like for example for the property ni-synch A for Kao Chow (K) in Fig. 1, and for Kao Chow + Woo Lam pi f (K + WLpif) in Fig. 2. This is generally due to the fact that Tamarin finds an attack more rapidly than a proof as Tamarin stops after the first attack it finds (it does not try to find all attacks).

It can also happen that Tamarin proves a property for the combination of protocols more quickly than for the protocols in isolation, like for example Needham Schroeder Lowe in Fig. 1 and Needham Schroeder Lowe + SPLICE/AS in Fig. 2 for ni-synch A. This can occur for example if the precomputations are the dominating part of the total runtime.

2.2 Attacks by Mathuria et al. [22]

We try to find the attacks described in [22] using Tamarin , to see if we find the same or different attacks if we use an automatic tool. The properties verified are not clearly defined in [22], so we keep the properties as defined previously. More precisely, we verified different authentication properties: non-injective synchronization, non-injective agreement, and a weaker agreement property. The property non-injective agreement as define previously is too strong to get comparable result with the paper, most of protocols of the paper are not safe for this property even in isolation. So we consider a weaker authentication property defined as follows:

  • weaker agreement: if B thinks that a nonce \(N_A\) is generated by A, then A has generated \(N_A\) and B authenticates A (called Aut A in Figs. 3 and 4).

Figure 3 summarizes results that we obtain with Tamarin in isolation on protocols from [22], and Fig. 4 summarizes results we obtain for the multi-protocols. As previously, ni-synch stands for non-injective synchronization, sec stands for secrecy and ni-agree stands for non-injective agreement. Moreover means that we did not find any attacks, and means there is at least one attack for the property. A yellow box means that the first protocol (the one for which we verify security in the combination) is safe for this property in isolation, and red box means that both protocols are safe for this property in isolation. An empty box means that the property is not relevant for this protocol.

Fig. 3.
figure 3

Results found with Tamarin with APG from [26], DS = Denning Sacco [13], AWL = Amended Woo Lam [5], ISO5 = ISOFive-Pass [7], AN = Abadi Needham [1], ZF from [30], * = only type-flaw attacks.

Full size image
Fig. 4.
figure 4

Results found with Tamarin with APG from [26], DS = Denning Sacco [13], AWL = Amended Woo Lam [5], ISO5 = ISOFive-Pass [7], AN = Abadi Needham [1], ZF from [30], * = the first protocol is safe in isolation, ** = both protocols are safe in isolation. (Color figure online)

Full size image

We can see in Fig. 3 in the case of APG.3 for non-injective synchronization and non-injective agreement, all attacks which we found in isolation are type-flaw attacks, and the protocol is safe if we do not consider type-flaw attacks. But attacks we found for APG.3 with APG.2 are not type flaw attacks (see 2.2), so we consider type-flaw attacks separately in this paper. But in the case of ZF.2, we have a protocol that is not safe for any property, considering type-flaws or not. So it is useless to see if ZF.2 can have a multi-protocol attack for a property in combination with an other protocol, a point that the authors of the original paper missed most likely since they searched for attacks manually.

The property weaker agreement seems to be closest to the property used in [22], because we found the same attacks for some protocols. Thus, in rest of the paper, we only present attacks on this property.

In comparison to the original paper we have found, using Tamarin , sometimes different attacks, and sometimes new attacks on the authentication of other protagonists in the same combination of protocols. This is likely due to the fact that Mathuria et al. searched for attacks manually, and were thus probably unable to analyze all combinations in detail or missed attacks in their analysis.

In all protocols, we have three participants, A the initiator, B the responder, and S the trusted server. We use symmetric encryption, so S shares the key \(K_{AS}\) (respectively \(K_{BS}\)) with A (respectively B). Moreover, \(K_{AB}\) denotes the session key between A and B, and \(N_A\) (respectively \(N_B\)) a nonce generated by A (respectively B). Then \(\{M\}_K\) denotes the cipher-text obtained by encrypting a message M with the symmetric key K. As in the original paper, we assume that each participant shares the same key for both protocols. In the following, when we talk about authentication, we mean non-injective agreement.

In the following we discuss our results in details. First we discuss attacks that we found and that differ from those presented in [22], then we present new attacks for properties that were not analyzed in [22].

Different Attacks

APG.4 with APG.6: The first attack is on the authentication of A. In this attack, two protagonists A and \(A'\) initiate the APG.6 [26] protocol with B, and the intruder C pretends to be A in APG.4 [26]. In the protocol initiated by \(A'\), C learns \((N_{A'},N_B',A')\), used as a session key, and its ciphertext \(\{N_{A'},N_B',A'\}_{K_{BS}}\). In the protocol initiated by A, C learns the nonce \(N_B\), used to authenticate to B. In Fig. 5, steps on the left hand side are steps of APG.4, and steps on the right hand side are steps from APG.6.

Fig. 5.
figure 5

Representation of the attack on APG.4 with APG.6.

Full size image

This attack is a type-flaw attack, because the intruder uses \((N_{A'},N_B',A')\) as a session key. So we blocked type-flaw attacks in Tamarin to see if there are other types of attacks, and we did not find other attacks on the authentication of A.

Denning-Sacco with Amended Woo-Lam: This attack is on the authentication of A. Again, it is a type-flaw attack, because the intruder uses \((K_{AB},T)\) as a nonce. In this attack, the intruder C plays the role of A and S in both protocols. First, B initiates a protocol Woo-Lam [5] with C who impersonates A. Then C sends the ID of A and a fake session key and a timestamp as a nonce. B encrypts that and C has now a valid message to send to B in Denning-Sacco [13]. This attack is described in Fig. 6.

Fig. 6.
figure 6

Representation of the attack on Denning-Sacco with Woo-Lam.

Full size image

We did not find other types of attacks for this protocol when we blocked type-flaw attacks in Tamarin using a modified model.

New Attacks

APG.1 with APG.2: The attack described in [22] is an attack on the authentication of B, but we also found an attack on the authentication of A. In this attack, the intruder C plays the role of A in both protocols. First, B runs the APG.2 [26] protocol as the initiator and then the protocol APG.1 [26] as the responder. C can pretend to be A in APG.1 and B will accept. In Fig. 7 steps at the left are steps from APG.1, and the right part are steps from APG.2.

Fig. 7.
figure 7

Representation of the attack on APG.1 with APG.2.

Full size image

APG.3 with APG.2: This attack is an attack on the authentication of B. This attack is possible if A runs the APG.3 [26] protocol as the initiator, and APG.2 [26] as the responder. In this attack, C plays the roles of B and S in both protocols. Then C can pretend to be B in APG.3, and A will accept. In Fig. 8 steps at the left are steps of APG.3, and at the right part are steps from APG.2.

Fig. 8.
figure 8

Representation of the attack on APG.3 with APG.2.

Full size image

We also found an attack on the authentication of A. In this attack, the intruder C plays the role of A in both protocols. B runs the APG.2 protocol as the initiator, and APG.3 as the responder. C can pretend to be A, and B in APG.3 will accept. In Fig. 9 steps at the left are steps from APG.3, and steps at the right are steps from APG.2.

Fig. 9.
figure 9

Representation of the attack on APG.3 with APG.2.

Full size image

APG.4 with APG.6: We found an attack on the authentication of B. In this attack, A initiates the protocol APG.3, then the intruder C will initiate APG.6 with B, using data sent by A in the other protocol. Finally, C sends the answer of B to the server in APG.4, and lets the protocol run. In Fig. 10, steps on the left hand side are steps from APG.4, and steps on the right hand side are steps from APG.6.

Fig. 10.
figure 10

Representation of the attack on APG.4 with APG.6.

Full size image
Fig. 11.
figure 11

Representation of the attack on APG.5 with APG.6.

Full size image

This attack is possible because the message from APG.6 used for this attack is also used in APG.4, so C can get a response from B, while B does not act in APG.4.

APG.5 with APG.6: This attack is on the authentication of A. In this attack, two protagonists A and \(A'\) initiate the APG.6 [26] protocol with B, and the intruder C pretends to be A in APG.5 [26]. In the protocol initiated by \(A'\), C learns \((N_{A'},N_B',A')\), used as a session key, and its encrypted version \(\{N_{A'},N_B',A'\}_{K_{BS}}\). In the protocol initiated by A, C learns the nonce \(N_B\), used to authenticate to B. In Fig. 11, steps at the left part are steps of APG.5, and steps on the right are steps from APG.6.

This attack is a type-flaw attack. So we changed our model to disable such type-flaw attacks in Tamarin to see if there are other types of attacks, and we did not find another attack on the authentication of A.

We also found an attack on the authentication of A where the intruder uses \((N_{A'},N_B',A')\) as a session key. In this attack, A initiates the protocol APG.5, then the intruder C will initiate APG.6 with B, using data sent by A in the other protocol. Finally, C sends the answer of B to the server in APG.5, and lets the protocol run. In Fig. 12, steps on the left hand side are steps from APG.5, and on the right hand side are steps from APG.6.

Fig. 12.
figure 12

Representation of the attack on APG.5 with APG.6.

Full size image

This attack is possible because the message from APG.6 used for this attack is also used in APG.5, so C can get a response from B, while B does not act in APG.5.

3 Workflow in Tamarin

As we had to write many different combinations of multiple protocols to obtain our results, we tried to simplify the process by adopting the following workflow to combine to protocols:

  1. 1.

    Specify each protocol individually and check the properties in isolation using Tamarin.

  2. 2.

    Generate the files for all the required combinations using the individual specifications.

  3. 3.

    Verify the combined protocols, and compare the results to known results.

To simplify the process of generating the combined specifications, we adopted certain (mostly syntactic) conventions when specifying the protocols. These mostly concern the common setup rules (key distribution etc.), the placement of labels, and the uniqueness of labels to avoid conflicts.

These conventions allowed us to develop an algorithm that can generate the input files of the composed protocols based on the individual specifications, including intermediate lemmas that simplify the analysis for Tamarin by removing undesirable cases for the subsequent analysis. The generation of these lemmas goes beyond a pure syntactical merger of the individual files. The algorithm requires some interaction with Tamarin, but noticeably simplifies the following analysis. The main idea is that if Tamarin finds an a problem in the merged lemma, then we need to analyze the trace produced by the tool and to modify the lemma. This procedure seems to be systematic for all the examples that we have considered here.

This algorithm is implemented in Python, and works automatically on most combinations from [9, 22]. Only in a handful of cases we need to manually adapt the produced output to obtain a valid lemma that removes all undesirable cases. Note that even in these cases, the manual intervention was only necessary to create the models, the following analysis was then automatic. For more information about this algorithm, see the extended version of this paper [15]. The implementation is also available on line [15].

4 Conclusion

In this paper, we perform an automated analysis of multi-protocols in Tamarin. For this we have used the both protocols studied in [9] using Scyther and the protocol studied in [22] manually. In all cases where attacks were known previously, we also find attacks. However, the tool sometimes finds different attacks than the ones found manually or using Scyther. Moreover, we also find new and unknown attacks, underlining the advantages of an automatic analysis. We also proposed an algorithm to systematically merge two Tamarin files for our analysis.

Our future work is to see how we can integrate our algorithm for automatically merging two Tamarin files into the tools in order to facilitate the life of Tamarin users. Finally our experience also shows us that it might even be possible to propose a similar heuristic to help Tamarin users by automatically generating such helping intermediate lemmas.