Symbolic Verification of Distance Bounding Protocols

Distance bounding protocols are cryptographic protocols that enable a verifier V to establish an upper bound on the physical distance to a prover P. They are typically based on timing the delay between sending out a challenge and receiving back the corresponding response. The first distance bounding protocol was proposed by Brands and Chaum [10], and since then various protocols have been proposed. In general, distance bounding protocols are made of two or three phases, the second one being a rapid phase during which the time measurement is performed. To improve accuracy, this challenge/response exchange during which the measurement is performed is repeated several times, and often performed at the bit level. Symbolic analysis does not allow us to reason at this level, and thus the rapid phase will be abstracted by a single challenge/response exchange, and operations done at bit level will be abstracted too.

For illustration purposes, we consider the TREAD protocol. As explained before, we ignore several details that are irrelevant to our symbolic security analysis, and we obtain the protocol described in Fig. 1. First, the prover generates a nonce \(\gamma \), and computes the signature \(\sigma \) with his own key. This signature is sent to V encrypted with the public key of V. Upon reception, the verifier decrypts the message and checks the signature. Then, the verifier sends a nonce m, and starts the rapid phase during which he sends a challenge c to the prover. The protocol ends successfully if the answer given by the prover is correct and arrived before a predefined threshold.

Typically, an attack occurs when a verifier is deceived into believing it is co-located with a given prover whereas it is not. Attacker may replay, relay and build new messages, as well as predict some timed challenges. Since the introduction of distance bounding protocols, various kinds of attacks have emerged, e.g. distance fraud, mafia fraud, distance hijacking attack, ...For instance, a distance fraud only consider a dishonest prover who tries to authenticate remotely, whereas a distance hijacking scenario allows the dishonest prover to take advantage of honest agents in the neighbourhood of the verifier.

The TREAD protocol is vulnerable to a mafia fraud attack: an honest verifier v may end successfully a session with an honest prover p thinking that this prover p is in his vicinity whereas p is actually far away. The attack is described in Fig. 1. After learning \(\gamma \) and a signature \(\sigma =\mathsf {sign}(\gamma ,sk_p)\), the malicious agent i will be able to impersonate p. At the end, the verifier v will finish his session correctly thinking that he is playing with p (who is actually far away).

The first symbolic framework developed to analyse distance bounding protocols is probably the one proposed in [27]. Since then, several formal symbolic models have been proposed: e.g. a model based on multiset rewriting rules has been proposed in [5], another one based on strand spaces is available in [31]. However, these models do not come with a procedure allowing one to analyse distance bounding protocols in an automatic way. Recently, some attempts have been done to rely on existing automatic verification tools, e.g. ProVerif [13, 19] or Tamarin [26]. Those tools typically consider an unbounded number of sessions, and some approximations are therefore performed to tackle this problem well-known to be undecidable [21].

Here, following the long line of research on symbolic verification for a bounded number of sessions which is a problem well-known to be decidable [29, 32] and for which automatic verification tools have been developed (e.g. OFMC [6], Akiss [12]), we aim to extend this approach to distance bounding protocols.

As usual in symbolic models, we represent messages using a term algebra. We consider a set \(\mathcal {N}\) of names split into two disjoint sets: the set \(\mathcal {N}_\mathsf {pub}\) of public names which contains the set \(\mathcal {A}\) of agent names, and the set \(\mathcal {N}_\mathsf {priv}\) of private names. We consider the set \(\mathcal {X}\) of message variables, denoted \(x, y, \ldots \), as well as a set \(\mathcal {W}\) of handles: \(\mathcal {W}= \{\mathsf {w}_1, \mathsf {w}_2, \ldots \}\). Variables in \(\mathcal {X}\) model arbitrary data expected by the protocol, while variables in \(\mathcal {W}\) are used to store messages learnt by the attacker. Given a signature \(\varSigma \), i.e. a finite set of function symbols together with their arity, and a set of atomic data \(\mathcal {A}t\), we denote \(\mathcal {T}(\varSigma ,\mathcal {A}t)\) the set of terms built from \(\mathcal {A}t\) using function symbols in \(\varSigma \). Given a term u, we denote \( st (u)\) the set of the subterms occurring in u, and \( vars (u)\) the set of variables occurring in u. A term u is ground when \( vars (u) = \emptyset \). Then, we associate an equational theory \(\mathsf {E}\) to the signature \(\varSigma \) which consists of a finite set of equations of the form \(u =v\) with \(u,v \in \mathcal {T}(\varSigma ,\mathcal {X})\), and induces an equivalence relation over terms denoted \(=_\mathsf {E}\).

We consider equational theories that can be represented by a convergent rewrite system, i.e. we assume that there is a confluent and terminating rewrite system such that:where \(t\mathord {\downarrow }\) denotes the normal form of t. Moreover, we assume that such a rewrite system has the finite variant property as introduced in [16]. This means that given a sequence \(t_1, \ldots , t_n\) of terms, it is possible to compute a finite set of substitutions, denoted \(\mathsf {variants}(t_1, \ldots , t_n)\), such that for any substitution \(\omega \), there exist \(\sigma \in \mathsf {variants}(t_1, \ldots , t_n)\) and \(\tau \) such that: \(t_1\omega \mathord {\downarrow }, \ldots , t_n\omega \mathord {\downarrow }= (t_1\sigma )\mathord {\downarrow }\tau , \ldots , (t_n\sigma )\mathord {\downarrow }\tau \). Many equational theories enjoy this property, e.g. symmetric/asymmetric encryptions, signatures and blind signatures, as well as zero-knowledge proofs.

Moreover, this finite variant property implies the existence of a finite and complete set of unifiers and gives us a way to compute it effectively. Given a set \(\mathcal {U}\) of equations between terms, a unifier (modulo a rewrite system \(\mathcal {R}\)) is a substitution \(\sigma \) such that \(s\sigma \mathord {\downarrow }= s'\sigma \mathord {\downarrow }\) for any equation \(s = s'\) in \(\mathcal {U}\). A set S of unifiers is said to be complete for \(\mathcal {U}\) if for any unifier \(\sigma \), there exists \(\theta \in S\) and \(\tau \) such that \(\sigma = \tau \circ \theta \). We denote \(\mathsf {csu}_\mathcal {R}(\mathcal {U})\) such a set. We will rely on these notions of \(\mathsf {variants}\) and \(\mathsf {csu}\) in our procedure (see Sect. 4).

An attacker builds her own messages by applying function symbols to terms she already knows and which are available through variables in \(\mathcal {W}\). Formally, a computation done by the attacker is a recipe, i.e. a term in \(\mathcal {T}(\varSigma , \mathcal {W}\cup \mathcal {N}_\mathsf {pub}\cup \mathbb {R}^+)\).

To model time, we will use non-negative real numbers \(\mathbb {R}^+\), and we may allow various operations (e.g. \(+\), −, \(\times \), ...). A time expression is constructed inductively by applying arithmetic symbols to time expressions starting with the initial set \(\mathbb {R}^+\) and an infinite set \(\mathcal {Z}\) of time variables. Then, a timing constraint is typically of the form \(t_1 \sim t_2\) with \(\sim \,\in \, \{<, \le , =\}\). We do not constraint the operators since our procedure is generic in this respect provided we have a way to decide whether a set of timing constraints is satisfiable or not. In practice, our tool (see Sect. 7) will only be able to consider simple linear timing constraints.

We assume that cryptographic protocols are modelled using a simple process algebra. Following [12], we only consider a minimalistic core calculus. In particular, we do not introduce the new operator and we do not explicitly model the parallel operator. Since we only consider a bounded number of sessions (i.e. a calculus with no replication), this is at no loss of expressivity. We can simply assume that fresh names are generated from the beginning and parallel composition can be added as syntactic sugar to denote the set of all interleavings.

Syntax. We model a protocol as a finite set of traces. A trace T is a finite sequence (possibly empty and denoted \(\epsilon \) in this case) of pairs, i.e. \(T = (a_1,\mathsf {a}_1). \ldots . (a_n, \mathsf {a}_n)\) where each \(a_i \in \mathcal {A}\), and \(\mathsf {a}_i\) is an action of the form:with \(x \in \mathcal {X}\), \(u, v, v' \in \mathcal {T}(\varSigma , \mathcal {N}\cup \mathbb {R}^+\cup \mathcal {X})\), \(z \in \mathcal {Z}\), and \(t_1 \sim t_2\) a timing constraint.

As usual, we have output and input actions. An input action acts as a binding construct for both x and z, whereas an output action acts as a binding construct for z only. For sake of clarity, we will omit the time variable z when we do not care of the precise time at which the input (resp. output) action has been performed. As usual, our calculus allows one to perform some tests on received messages, and it is also possible to extract a timestamp from a received message and perform some tests on this extracted value using timing constraints. Typically, this will allow us to model an agent that will stop executing the protocol in case an answer arrives too late.

We assume the usual definitions of free and bound variables for traces, and we assume that each variable is at most bound once. Note that, in the constructs presented above, the variables z, x are bound. Given a set \(\mathcal {V}\) of variables, a trace is locally closed w.r.t. \(\mathcal {V}\) if for any agent a, the trace obtained by considering actions executed by agent a does not contain free variables among those in \(\mathcal {V}\). Such an assumption, sometimes called origination [6, 15], is always satisfied when considering traces obtained by interleaving actions of a protocol. Therefore, we will only consider traces that are locally closed w.r.t. both \(\mathcal {X}\) and \(\mathcal {Z}\).

Contrary to the calculus introduced in [19] which assumes that there is at most one timer per thread, we are more flexible. This generalisation is not mandatory to analyse our case studies but it allows us to present our result on traces and greatly simplifies the theoretical development.

Of course, when performing a security analysis, other traces have to be considered. Typically, we may want to consider several instances of each role, and we will have to generate traces corresponding to all the possible interleavings of the actions composing these roles.

Semantics. The semantics of a trace is given in terms of a labeled transition system over configurations of the form \((T;\varPhi ;t)\), and is parametrised by a topology reflecting the fact that interactions between agents depend on their location.

In our model, the distance between two agents is given by the time it takes for a message to travel from one to another. We have that:with \(||\cdot ||:\mathbb {R}^3\rightarrow \mathbb {R}\) the Euclidean norm and \(c_0\) the transmission speed. We suppose, from now on, that \(c_0\) is a constant for all agents, and thus an agent a can recover, at time \(t +\textsf {Dist}_{\mathcal {T}_0}(a,b)\), any message emitted by the agent b before \(t \in \mathbb {R}^+\).

Intuitively, T represents the trace that still remains to be executed; \(\varPhi \) represents the messages that have been outputted so far; and t is the global time.

The precise location of each agent is not relevant, only the distance between them matters. Here \({\textsf {Dist}_{\mathcal {T}_0}(v,i) < t_0}\) whereas \({\textsf {Dist}_{\mathcal {T}_0}(v,p) \ge t_0}\).

A possible configuration is \(K_0 = (T_\mathsf {ex};\varPhi _0;0)\) withWe have that v is playing the verifier’s role with p (who is far away). We do not consider any prover’s role but we assume that p (acting as a prover) has started a session with i and thus the corresponding encryption (here \(\gamma \in \mathcal {N}_\mathsf {priv}\)) has been added to the knowledge of the attacker (handle \(\mathsf {w}_3\)). We also assume that \(sk_i \in \mathcal {N}_\mathsf {priv}\), the private key of the agent \(i \in \mathcal {M}_0\), is known by the attacker. A more realistic configuration would include other instances of the prover and the verifier roles and will probably give more knowledge to the attacker. This simple configuration is actually sufficient to retrieve the attack presented in Sect. 2.2.

We write \(\left. \lfloor \varPhi \rfloor \right. _{a}^{t}\) for the restriction of \(\varPhi \) to the agent a at time t, i.e.:Our labeled transition system is given in Fig. 2 and relies on labels \(\ell \) which can be either equal to the unobservable \(\tau \) action or of the form \((a,\mathsf {a})\) with \(a \in \mathcal {A}\), and \(\mathsf {a}\in \{\mathsf {test}, \mathsf {eq}\} \cup \{\mathsf {in}(u), \mathsf {out}(u)~|~ u \in \mathcal {T}(\varSigma , \mathcal {N}\cup \mathbb {R}^+)\} \cup \{\mathsf {let}(v) ~|~ v \in \mathbb {R}^+\}\). The TIM rule allows time to elapse and is labeled with \(\tau \) (often omitted for sake of simplicity). The OUT rule allows an output action to be executed, and the outputted term will be added to the frame. Rule EQ is used to perform some tests, and those tests are evaluated modulo the equational theory. Then, the LET rule allows us to evaluate a term that is supposed to contain a real number, and could then be used in a timing constraint through the variable z. Then, we have a rule to evaluate a timing constraint. The IN rule allows an agent a to execute an input: the received message u has been sent at time \(t_b\) by an agent b who was in possession of the message at that time. In case b is a malicious agent, i.e. \(b \in \mathcal {M}_0\), the message u may have been forged through a recipe R, and b has to be in possession of all the necessary information at that time. The variable z is used to store the time at which this action has been executed.

The goal of this paper is to propose a new procedure for analysing a bounded number of sessions of distance bounding protocols. Once the topology is fixed, the existence of an attack can be directly encoded as a reachability property considering a finite set of traces. The following sections are thus dedicated to the study of the following problem:

We consider symbolic runs which are finite sequences of pairs with possibly a run variable typically denoted \(\mathsf {y}\) at its ends. We have that each pair \((a, \mathsf {a})\) is such that \(a \in \mathcal {A}\) and \(\mathsf {a}\) is an action of the form (with \(u\in \mathcal {T}(\varSigma , \mathcal {N}\cup \mathbb {R}^+\cup \mathcal {X})\)):Excluding the special variable \(\mathsf {y}\), a symbolic run \((a_1, \mathsf {a}_1). \ldots . (a_n, \mathsf {a}_n)\), only contains variables from the set \(\mathcal {X}\). We say that it is locally closed if whenever a variable x occurs in an output action (resp. let action) \(\mathsf {a}_j\), then there exists an input action \(\mathsf {a}_i\) occurring before (i.e. \(i < j\)) such that \(a_i = a_j\) and \(x \in vars (\mathsf {a}_i)\). Symbolic runs are often denoted \(w, w', \ldots \), and we write \(w \sqsubseteq w'\) when the sequence w is a prefix of \(w'\). Given a symbolic run \(w_0\) whose sequence of outputs is \(\mathsf {out}(u_1) \cdot \ldots \cdot \mathsf {out}(u_n)\), we denote \(\phi (w_0) = \{\mathsf {w}_1 \rightarrow u_1, \ldots , \mathsf {w}_n \rightarrow u_n\}\).

We also consider symbolic recipes which are terms in \(\mathcal {T}(\varSigma , \mathcal {W}\cup \mathcal {N}_\mathsf {pub}\cup \mathcal {Y})\) where \(\mathcal {Y}\) is a set of recipe variables disjoint from \(\mathcal {X}\) and \(\mathcal {W}\). We use capital letters X, Y, and Z to range over \(\mathcal {Y}\).

Our logic is based on two predicates expressing deduction and reachability without taking into account timing constraints. More formally, given a configuration \((T;\varPhi ;t)\), its untimed counterpart is \((T;\phi )\) where \(\phi \) is the untimed counterpart of \(\varPhi \), i.e. a frame of the form: \(\phi = \{\mathsf {w}_1 \rightarrow u_1, \ldots , \mathsf {w}_n \rightarrow u_n\}\). The relaxed semantics over untimed configurations is given in Fig. 3. Since time variables (from \(\mathcal {Z}\)) are not instantiated during a relaxed execution, in an untimed configuration \((T;\phi )\), the trace T is only locally closed w.r.t. \(\mathcal {X}\). Our predicates are:

Formally, we have that:

This semantics is extended as usual to first-order formulas built using the usual connectives (e.g. conjunction, quantification, ...)

In the above definition, we implicitly assume that all variables are universally quantified, i.e., all statements are ground. By abuse of language we sometimes call \(\sigma \) a grounding substitution for a statement \(H \Leftarrow ( B_1, \ldots , B_n)\) when \(\sigma \) is grounding for each of the atomic formulas \(H, B_1, \ldots , B_n\). The skeleton of a statement f, denoted \(\mathsf {skl}(f)\), is the statement where recipes are removed. Our definition of statement is in line with the original one proposed in [12] but we state an additional invariant used to establish the completeness of our procedure.

In order to define our set of seed statements, we have to fix some naming conventions. Given a trace T of the form \((a_1, \mathsf {a}_1).(a_2,\mathsf {a}_2).\ldots .(a_n,\mathsf {a}_n)\), we assume w.l.o.g. the following naming conventions:

For each \(m \in \{0, \ldots , n\}\), the sets \(\mathsf {Rcv}(m)\), \(\mathsf {Snd}(m)\), \(\mathsf {Eq}(m)\), \(\mathsf {Let}(m)\), and \(\mathsf {Test}(m)\) respectively denote the set of indexes of the receive, send, equality, let, and test actions amongst \(\mathsf {a}_1, \ldots , \mathsf {a}_m\). We denote by |S| the cardinality of S.

Given a set \(\mathcal {C} \subseteq \mathcal {N}_\mathsf {pub}\cup \mathbb {R}^+\), the set of seed statements associated to T and \(\mathcal {C}\), denoted \(\mathsf {seed}(T,\mathcal {C})\), is defined in Fig. 4. If \(\mathcal {C} = \mathcal {N}_\mathsf {pub}\cup \mathbb {R}^+\), then \(\mathsf {seed}(T,\mathcal {C})\) is said to be the set of seed statements associated to T and in this case we write \(\mathsf {seed}(T)\) as a shortcut for \(\mathsf {seed}(T,\mathcal {N}_\mathsf {pub}\cup \mathbb {R}^+)\). When computing seed statements, we compute complete sets of unifiers and complete sets of variants modulo \(\mathcal {R}\). This allows us to get rid of the rewrite system in the remainder of our procedure and then only consider unification modulo the empty equational theory. In this case, it is well-known that (when it exists) \(\mathsf {csu}_\emptyset (\mathcal {U})\) is uniquely defined up to some variable renaming, and we write \(\mathsf {mgu}(u_1,u_2)\) instead of \(\mathsf {csu}_{\emptyset }(\{u_1 = u_2\})\).

We now show that as far as the timing constraints are ignored, the set \(\mathsf {seed}(T)\) is a sound and complete abstraction of a trace. Moreover, we have to ensure that the proof tree witnessing the existence of a given predicate in \(\mathcal {H}(\mathsf {seed}(T))\) matches with the relaxed execution we have considered. This is mandatory to establish the completeness of our procedure.

This notion of matching is extended to a proof tree \(\pi \) as expected, meaning that all the instances of Conseq used in \(\pi \) satisfy the property.

Actually, the completeness of our procedure will be established w.r.t. a subset of recipes, namely uniform recipes. We establish that an execution of a trace \(T_0\) which only involves uniform recipes has a counterpart in \(\mathcal {H}(\mathsf {seed}(T_0))\) which is uniform too.

We are now able to state our soundness and completeness result.

We restrict the use of the resolution rule and we only apply it on a selected atom. To formalise this, we assume a selection function \(\mathsf {sel}\) which returns \(\bot \) when applied on a solved statement, and an atom \(\mathsf {k}_w(X,t)\) with \(t \not \in \mathcal {X}\) when applied on an unsolved statement. Resolution must be performed on this selected atom.

During saturation, the statement obtained by resolution is given to an update function which decides whether it has to be added or not into the knowledge base (possibly after some transformations). In original Akiss, many deduction statements are discarded during the saturation procedure. This is useful to avoid non-termination issues and it is not a problem since there is no need to derive the same term (from the deduction point of view) in more than one way. Now, considering that messages need time to reach a destination, a same message emitted twice at two different locations deserves more attention.

As illustrated by Example 11, we therefore need to consider more recipes (even if they deduce the same message) to accommodate timing constraints, but we have to do this in a way that does not break termination (in practice). To tackle this issue, we modified the canonicalization rule, as well as the update function to allow more deduction statements to be added in the knowledge base.

The intuition is that there is no need to consider several recipes (here X and Y) to deduce the same term t when such a recipe does not occur in the head of the statement.

Then, the update of K by f denoted \(K \Cup \{f\}\), is defined to be K if either \(\mathsf {skl}(f\mathord {\Downarrow })\) is not in normal form; or \(f\mathord {\Downarrow }\) is solved but not well-formed. Otherwise, \(K \Cup \{f\} = K \cup \{f\mathord {\Downarrow }\}\). To initiate our saturation procedure, we start with the initial knowledge base \(K_{\mathsf {init}}(S)\) associated to a set S of statements (typically \(\mathsf {seed}(T,\mathcal {C})\) for some well-chosen \(\mathcal {C}\)). Given a set S of statements, the initial knowledge base associated to S, denoted \(K_\mathsf {init}(S)\), is defined to be the empty knowledge base updated by the set S, i.e. \(K_\mathsf {init}(S) = (((\emptyset \Cup f_1) \Cup f_2) \Cup \ldots f_n\) where \(f_1, \ldots , f_n\) is an enumeration of the statements in S. In return, the saturation procedure produces a set \(\mathsf {sat}(K)\) which is actually a knowledge base.

Then, we can establish the soundness of our saturation procedure. This is relatively straightforward and follows the same lines as the original proof.

Completeness is more involved. Indeed, we can not expect to retrieve all the recipes associated to a given term. To ensure termination (in practice) of our procedure, we discard some statements when updating the knowledge base, and we have to justify that those statements are indeed useless. Actually, we show that considering uniform recipes is sufficient when looking for an attack trace.

However, the notion of uniform recipe does not allow one to do the proof by induction. We therefore consider a more restricted notion that we call asap recipes. The idea is to deduce a term as soon as possible but this may depend on the agent who is performing the computation. We also rely on an ordering relation which is independent of the agent who is performing the computation, and which is compatible with our notion of asap w.r.t. any agent.

Given a relaxed execution with input recipes \(R_1, \ldots , R_k\), we define the following relations:

Then, \(<_{\mathsf {exec}}\) is the smallest transitive relation over recipes built on \( dom (\phi )\) that contains \(<^{\mathsf {in}}_\mathsf {exec}\) and \(<^{\mathsf {sub}}_\mathsf {exec}\). As usual, we denote \(\le _\mathsf {exec}\) the reflexive closure of \(<_\mathsf {exec}\).

Given a timed execution \(\mathsf {exec}= (T_0;\emptyset ;t_0) \xrightarrow {\ell _1,\ldots , \ell _n} (S;\varPhi ;t)\) with \(\varPhi = \{\mathsf {w}_1 \xrightarrow {a_1,t_1} u_1, \ldots , \mathsf {w}_n \xrightarrow {a_n,t_n} u_n\}\), we denote by \(\mathsf {agent}(\mathsf {w}_i)\) (resp. \(\mathsf {time}(\mathsf {w}_i)\)) the agent \(a_i\) (resp. the time \(t_i\)). The relation \(<^a_{\mathsf {exec}} \) over \( dom (\varPhi ) \times dom (\varPhi )\) with \(a \in \mathcal {A}\) is defined as follows: \(\mathsf {w}<^a_\mathsf {exec}\mathsf {w}' \) when:

This order is extended on recipes as follows: \(R <^a_\mathsf {exec}R'\) when:

We have that \(<_\mathsf {exec}^a\) is a well-founded order for any \(a\in \mathcal {A}\) which is compatible with \(<_\mathsf {exec}\), i.e. \(R <_\mathsf {exec}R'\) implies \(R <^a_\mathsf {exec}R'\) for any agent a.

We are now able to introduce our notion of asap recipe.

We may note that our definition of being asap takes care about honest agents who are not allowed to forge messages from their knowledge using recipes not in \(\mathcal {W}\cup \mathcal {N}_\mathsf {pub}\cup \mathbb {R}^+\). Hence, a recipe \(R \in \mathcal {W}\) is not necessarily replaced by a recipe \(R'\) even if \(R <^a_\mathsf {exec}R'\) and \({R'\varPhi \mathord {\downarrow }= R\varPhi \mathord {\downarrow }}\). Actually, such a recipe \(R'\) is not necessarily an alternative to R when \(a \not \in \mathcal {M}_0\).

Then, we can establish completeness of our saturation procedure w.r.t. these asap recipes.

Our procedure is given in Algorithm 1. We start with the set K of solved statements obtained by applying our saturation procedure on the trace T. We consider each reachability statement in K, and after instantiating the remaining variables with fresh constants using a bijection \(\rho \), we compute for each input \((a_i, \mathsf {in}(v_i))\) occurring in \(\ell '_1 \ldots , \ell '_n\) all the possible recipes that may lead to the term \(v_i\rho \) and store them in the set \(\overline{L_i}\). Actually, thanks to our soundness result (Proposition 1), we know that these recipes deduce the requested terms, and it only remains to check that the timing constraints are satisfied (lines 10–11).

We consider a trace T of the form \((a_1, \mathsf {a}_1).(a_2,\mathsf {a}_2).\ldots .(a_n,\mathsf {a}_n)\) locally closed w.r.t. \(\mathcal {X}\) and \(\mathcal {Z}\) and we assume the naming convention given in Sect. 4.2. Moreover, we denote by \(\mathsf {orig}(j)\) the index of the action in the trace T that performed the j^th output, i.e. \(\mathsf {orig}(j)\) is the minimal k such that \(|\mathsf {Snd}(k)|=j\). The function \(\mathsf{Timing}\) takes as inputs the initial configuration, the recipes used to feed the inputs occurring in the trace, and the terms corresponding to these inputs. Note that all these terms may still contain variables from \(\mathcal {Z}\). This function computes a formula that represents all the timing constraints that have to be satisfied to ensure the executability of the trace in our timed model. More formally, \(\mathsf{Timing}((T;\emptyset ;t_0)), R_{i_1} \ldots R_{i_p}, u_{i_1} \ldots u_{i_p})\) is the conjunction of the formulas:

The last step of our algorithm consists in checking whether the resulting formula \(\psi \) is satisfiable or not, i.e. whether there exists a mapping from \( vars (\psi )\) to \(\mathbb {R}^+\) such that the formula \(\psi \) is true. Of course, even if our procedure is generic w.r.t. to timing constraints, the procedure to check the satisfiability of \(\psi \) will depend on the constraints we consider. Actually, all the formulas encountered during our case studies are quite simple: they are expressed by equations of the form \(z' - z \le t\), and we therefore rely on the well-known Floyd-Warshall algorithm to solve them. When needed, we may rely on the simplex algorithm to solve more general linear constraints.

First, we may note that to obtain an effective saturation procedure, it is important to start with a finite set of seed statements. Our set \(\mathsf {seed}(T)\) is infinite but as it was proved in [12], we can restrict ourselves to perform saturation using the finite set \(\mathsf {seed}(T,\mathcal {C}_T)\) where \(\mathcal {C}_T\) contains the public names and the real numbers occurring in the trace T. More formally, we have that:

Nevertheless, the saturation may not terminate. We could probably avoid some non-termination issues by improving our update operator. However, ensuring termination in theory is a rather difficult problem (the proof of termination for the original Akiss procedure for subterm convergent theories is quite complex [12] – more than 20 pages). We would like to mention that we never encountered non-termination issues in practice on our case studies.

Another issue is that, when computing the set \(\overline{L_i}\), we need to compute all the recipes R such that \(\mathsf {k}_w(R,u) \in \mathcal {H}(K)\) for a given term u. This can be achieved using a simple backward search and will terminate since K only contains solved statements that are well-formed. The naive recursive algorithm will therefore consider terms \(u_1, \ldots , u_n\) that are strict subterms of the initial term u. Note that statements that are not well-formed are discarded by our update operator: ensuring completeness of our saturation procedure when discarding statements that are not well-formed is the challenging part of our completeness proof.

We consider a topology \(\mathcal {T}_0\) and a configuration \((T;\emptyset ;t_0)\) built on top of \(\mathcal {T}_0\) and such that T is locally closed w.r.t. both \(\mathcal {X}\) and \(\mathcal {Z}\).

Soundness (item 1 above) is relatively straightforward. Item 2 is more involved. Of course, our algorithm does not consider all the possible recipes for inputs. Some recipes are discarded from our analysis. Actually, it is sufficient to focus our attention on asap recipes. To justify that this is not an issue regarding completeness, we first establish the following result.

Then, we may apply Theorem 2 (item 1) on this “asap execution” and deduce the existence of \(f = \mathsf {r}_{\ell '_1, \ldots , \ell '_n} \Leftarrow \mathsf {k}_{w_1}(X_1, x_1), \ldots , \mathsf {k}_{w_m}(X_m,x_m)\) in K and a substitution \(\sigma \) witnessing the fact that \(\mathsf {r}_{\ell _1, \ldots , \ell _n} = \mathsf {r}_{\ell '_1\sigma , \ldots , \ell '_n\sigma }\in \mathcal {H}(K)\). Moreover, we know that f and \(\sigma \) match with \(\mathsf {exec}\) and \(R_1, \ldots , R_k\). Considering the symbolic recipes \(\hat{R}_1, \ldots , \hat{R}_k\) witnessing this matching, and instantiating their variables with adequate fresh constants (using \(\rho \)), we can show that \(\hat{R}_1\rho , \ldots , \hat{R}_k\rho \) are recipes that allow to perform the timed execution \(\ell '_1\rho , \ldots , \ell '_n\rho \). Note that thanks the strong relationship we have between \(R_1, \ldots , R_k\) and \(\hat{R_1}, \ldots , \hat{R_k}\) (by definition of matching, \(R_i = \hat{R_i}\sigma \)), we know that the resulting timing constraints gathered in the formula \(\psi \) due to inputs are less restrictive, and the other ones are essentially unchanged. This allows us to ensure that the formula \(\psi \) will be satisfiable. Now, applying Lemma 2, we can assume w.l.o.g. that recipes involved in such a trace are asap, and thus according to Theorem 2 will be considered by our procedure, and put in \(\overline{L_{i_1}}, \ldots , \overline{L_{i_p}}\) at line 6 of Algorithm 1.

Our syntax is very close to the one presented in Sect. 3. For sake of simplicity, we sometimes omit timestamps on input/output actions. Regarding our timing constraints, our syntax only allows linear expressions of the form \(z_1 - z_2 \sim z_3\) with \(z_i\in \mathcal {Z}\cup \mathbb {R}^+\) and \(\sim \ \in \{=,<, \le \}\). These expressions are enough to model all our case studies. To ease the specification of protocols our tool support parallel composition of traces (\(T_1 \mid \mid T_2\)). This operator is syntactic sugar and can be translated to sets of traces in a straightforward way.

To mitigate the potential exponential blowup caused by this translation, we always favour let, equality, and test actions, as well as output actions when no timestamp occur on it. The second optimisation consists in executing input actions (without timestamps) in a raw. These optimisations will allow us to reduce the number of traces that have to be considered during our analysis, and are well-known to be sound when verifying reachability properties [4, 30].

In this section we demonstrate that our tool can be effectively used to analyse distance bounding protocols and payment protocols. Our experiments have been done on a standard laptop and the results obtained confirm termination of the saturation procedure when analysing various protocols (\(\times \) stands for attack, means that the protocol has been proved secure). We indicate the number of roles (running in parallel) we consider and the number of traces (due to all the possible interleaving of the roles) that have been analysed by the tool in order to conclude. Our algorithm stops as soon as an attack is found, and thus the number of possible interleavings is not relevant in this case.

We only consider two distinct topologies: one to analyse mafia fraud scenarios (2 honest agents far away with a malicious agent close to each honest agent) and one to analyse distance hijacking for which 3 agents are considered (malicious agent in the neighbourhood of the verifier on which the security property is encoded is not allowed). This may seem restrictive but it has been shown to be sufficient to capture all the possible attacks [19]. Our results are consistent with the ones obtained in [13, 14, 19, 26].

Distance Bounding Protocols. As explained in Sect. 2 on the TREAD protocol, we ignore several details that are irrelevant to a security analysis performed in the symbolic model. Moreover, our procedure is not yet able to support the exclusive-or operator and thus it has been modelled in an abstract way when analysing the protocols BC and Swiss-Knife. When no attack was found for 2 roles, we consider more roles (and thus more traces). The fact that the performances degrade when considering additional roles is not surprising and is clearly correlated with the number of traces that have to be considered.

Payment Protocols. We have also analysed three payment protocols (and some of their variants) w.r.t. mafia fraud – the only relevant scenario for this kind of application (see [13]). It happens that these protocols are more complex to analyse than traditional distance bounding protocols. They often involve more complex messages, and a larger number of message exchanges. Moreover, in protocols MasterCard RRP and NXP, the threshold is not fixed in advance but received during the protocol execution. Due to this, these protocols fall outside the class of protocols that can be analysed by [19, 26]. To our knowledge only [13] copes with this issue by proposing a security analysis in two steps: they first establish that the value of the threshold can not be manipulated by the attacker, and then analyse the protocol considering a fixed threshold. Such a protocol can be encoded in a natural way in our calculus using the let instruction \([z := v]\) that allows one to extract a timing information from a message. We analysed these protocols considering one instance of each role.