Alexandre Debant

Stéphanie Delaune

Cyrille Wiedling

Proving physical proximity using symbolic models

For many modern applications like e.g. contactless payment, and keyless systems, ensuring physical proximity is a security goal of paramount importance. Formal methods have proved their usefulness when analysing standard security protocols. However, existing results and tools do not apply to e.g. distance bounding that aims to ensure physical proximity between two entities. This is due in particular to the fact that existing models do not represent in a faithful way the locations of the participants, and the fact that transmission of messages takes time. In this paper, we propose several reduction results: when looking for an attack, it is actually sufficient to consider a simple scenario involving at most four participants located at some specific locations. An interesting consequence of our reduction results is that it allows one to reuse ProVerif, an automated tool developed for analysing standard security protocols. As an application, we analyse several distance bounding protocols, as well as a contactless payment protocol.

Introduction

The shrinking size of microprocessors as well as the ubiquity of wireless communication have led to the proliferation of portable computing devices with novel security requirements. Whereas traditional security protocols achieve their security goals relying solely on cryptographic primitives like encryptions and hash functions, this is not the case anymore for many modern applications like e.g. contactless payment. Actually, a typical attack against these devices is the socalled relay attack, as demonstrated for EMV in [START_REF] Chothia | Relay cost bounding for contactless EMV payments[END_REF]. Such an attack allows a malicious participant to relay communication between a victim's card (possibly inside a wallet) and a genuine terminal so that the victim's card, even if it is far away from the terminal, will pay the transaction. Due to the contactless nature of most of our communication, obtaining reliable information regarding physical proximity is of paramount importance and specific protocols, namely distance bounding protocols, were proposed to achieve this specific goal [START_REF] Brands | Distance-bounding protocols[END_REF][START_REF] Kim | The swiss-knife RFID distance bounding protocol[END_REF]. They typically take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two participants.

In the context of standard security protocols, such as key establishment protocols, formal methods have proved their usefulness for providing security guarantees or detecting attacks. The purpose of formal verification is to provide rigorous frameworks and techniques to analyse protocols and find their flaws. For example, a flaw has been discovered in the Single-Sign-On protocol used e.g. by Google Apps. It has been shown that a malicious application could very easily get access to any other application (e.g. Gmail or Google Calendar) of their users [START_REF] Armando | Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for Google apps[END_REF]. This flaw has been found when analysing the protocol using formal methods, abstracting messages by a term algebra and using the Avantssar validation platform [START_REF] Armando | The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures[END_REF]. Another example is a flaw on vote-privacy discovered during the formal and manual analysis of an electronic voting protocol [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF]. All these results have been obtained using formal symbolic models, where most of the cryptographic details are ignored using abstract structures, and the communication network is assumed to be entirely controlled by an omniscient attacker. The techniques used in symbolic models have become mature and several tools for protocol verification are nowadays available [START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF][START_REF] Armando | The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures[END_REF][START_REF] Meier | The Tamarin Prover for the Symbolic Analysis of Security Protocols[END_REF].

However, protocols whose security rely on constraints from the physical world fall outside the scope of traditional symbolic models that are based on the omniscient attacker who controls the entire network, and who can for instance relay messages without introducing any delay. Due to the lack of formal symbolic models and verification tools, distance bounding protocols are only analysed so far with respect to some specific attack types known as e.g. distance fraud, mafia fraud, and terrorist fraud. Recently, another type of attack, namely distance hijacking [START_REF] Cremers | Distance hijacking attacks on distance bounding protocols[END_REF], has been discovered, and many protocols have been shown to be vulnerable to this new type of attacks. Following [START_REF] Basin | Formal reasoning about physical properties of security protocols[END_REF][START_REF] Kanovich | Towards timed models for cyber-physical security protocols[END_REF], and more recently [START_REF] Mauw | Distance-bounding protocols: Verification without time and location[END_REF], our aim is to bridge the gap between informal approaches currently used to analyse these protocols and the formal approaches already used for analysing traditional security protocols.

Our contributions. We first propose a calculus which allows timed protocols as well as the notion of physical proximity to be formally described. We model cryptography as a black box, thus the attacker cannot break cryptography, e.g. decrypt a message without having the appropriate decryption key. To model timed protocols in an accurate way, our communication model is subject to physical restrictions. These constraints apply to honest agents and attackers. An attacker can only intercept messages at his location, and attackers can not instantaneously exchange their knowledge: transmitting messages takes time. This models reality, where the attackers' ability to observe and communicate messages depends on their locations.

Our main contribution is to provide reduction results in the spirit of the one obtained in [START_REF] Comon-Lundh | Security properties: two agents are sufficient[END_REF] for traditional protocols: if there is an attack, then there is one considering only few participants at some specific locations. The results slightly differ depending on the type of attacks we consider (distance fraud, mafia fraud, or hijacking attack) but it allows one to focus on topologies involving a small number of participants (at most 4 including the malicious ones). We therefore reduce the number of topologies to be considered from infinitely many to only one (actually one per type of attacks). Our results hold in a rather general setting. In particular, we consider arbitrary cryptographic primitives as soon as they can be expressed using rewriting rules modulo an equational theory.

An interesting consequence of our reduction results is that it allows one to reuse techniques and tools developed for standard security protocols. Actually, we show how to encode these simple topologies, as well as the timing constraints, relying on the phase mechanism available in ProVerif. As an application, we analyse several distance bounding protocols, and we also consider the contactless payment protocol described in [START_REF] Chothia | Relay cost bounding for contactless EMV payments[END_REF]. All files related to the case studies are available here: http://people.irisa.fr/Alexandre.Debant/proving-physicalproximity-using-symbolic-methods.html Related work. Until recently, most distance bounding protocols have been analysed without a formal approach. Recent efforts have been made on proving security of distance bounding protocols. For instance, in 2001, Avoine et al. [START_REF] Avoine | A framework for analyzing RFID distance bounding protocols[END_REF] proposed a framework in which many protocols have been analysed and compared in a unified manner [START_REF] Avoine | Security of distance-bounding: A survey[END_REF]. A rather general model has been proposed by Boureanu et al. in [11]. This computational model captures all the classical types of attacks and generalises them enabling attackers to interact with many provers and verifiers. These models are very different from ours. Indeed, we consider here a formal symbolic model in which messages are no longer bitstrings but they are abstracted away by terms. Some recent attempts have been made to design formal symbolic model suitable to analyse distance bounding protocols: e.g. a model based on multiset rewriting rules has been proposed in [START_REF] Basin | Formal reasoning about physical properties of security protocols[END_REF] and [START_REF] Mauw | Distance-bounding protocols: Verification without time and location[END_REF], another one based on strand spaces is available here [START_REF] Nigam | Towards the automated verification of cyber-physical security protocols: Bounding the number of timed intruders[END_REF]. Even if our model shares some similarities with those mentioned above, we choose to design a new one based on the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. This allows us in particular to connect our theoretical results with the ProVerif verification tool that we ultimately use to analyse protocols.

Our main reduction result follows the spirit of [START_REF] Cortier | Analysing routing protocols: four nodes topologies are sufficient[END_REF] where it is shown that it is sufficient to consider five specific topologies when analysing routing protocols. To our knowledge, the only work proposing a reduction result suitable for distance bounding protocols is [START_REF] Nigam | Towards the automated verification of cyber-physical security protocols: Bounding the number of timed intruders[END_REF]. In this paper, the authors show that n attackers are actually sufficient when analysing an initial configuration involving at most n honest participants. Moreover, due to the way attackers are located (close to each honest participant), their result can not be applied to analyse some well-known attack scenarios (e.g. hijacking attack, distance fraud) that typically disallow the presence of an attacker in the neighbourhood of some honest participants. In contrast, our result reduces to only one topology, even when considering an arbitrary number of honest participants, and it applies to the scenarios mentioned above. A consequence of this result is that we can leverage the ProVerif tool to analyse such protocols. To do that we get some inspiration from [START_REF] Chothia | Relay cost bounding for contactless EMV payments[END_REF] and we use the phase mechanism of ProVerif to encode timing constraints. Our contributions improve upon their work by providing a strong theoretical foundation to their idea. Moreover, in order to consider scenario in which attackers are far away, and thus unable to produce an answer within the delay, we slightly modify the tool to discard some attacker behaviours. This was needed to be able to obtain meaningful results using ProVerif when analysing distance fraud and distance hijacking scenarios. Recently, a methodology to analyse distance bounding protocols within the Tamarin verification tool has been proposed [START_REF] Mauw | Distance-bounding protocols: Verification without time and location[END_REF]. Their model is not flexible enough to allow one to consider the different class of attacks, e.g. they cannot prove that a protocol is distance fraud resistant but vulnerable to mafia fraud. Nevertheless, they are able to analyse many protocols, confirmed some known vulnerabilities in a number of protocols, and discovered unreported attacks. All these protocols have been analysed in our framework, and a comparison is provided in Section 7.

Messages

As usual in the symbolic setting, we model messages through a term algebra. We consider both equational theories and reduction relations to represent the properties of the cryptographic primitives. This provides a lot of flexibility and allows one to model various cryptographic primitives.

Term algebra

We consider two infinite and disjoint sets of names: N is the set of basic names, which are used to represent keys, nonces, whereas A is the set of agent names, i.e. names which represent the agents identities. We consider an infinite set Σ 0 of constant symbols that are used for instance to represent nonces drawn by the attacker. We also consider two infinite and disjoint sets of variables, denoted X and W. Variables in X refer to unknown parts of messages expected by participants while variables in W are used to store messages learnt by the attacker.

We assume a signature Σ, i.e. a set of function symbols together with their arity. The elements of Σ are split into constructor and destructor symbols, i.e. Σ = Σ c Σ d . We denote Σ + = Σ ∪ Σ 0 , and Σ + c = Σ c ∪ Σ 0 . Given a signature F, and a set of atomic data A, we denote by T (F, A) the set of terms built from atomic data A by applying function symbols in F. A constructor term is a term in T (Σ + c , N ∪A∪X ). We denote vars(u) the set of variables that occur in a term u. A message is a constructor term u that is ground, i.e. such that vars(u) = ∅. The application of a substitution σ to a term u is written uσ. We denote dom(σ) its domain, and img(σ) its image. The positions of a term are defined as usual.

Example 1. We consider the following signature Σ ex = Σ c Σ d : Σ c = {commit, sign, sk, vk, ok, , ⊕, 0}, Σ d = {open, getmsg, check, proj 1 , proj 2 , eq}.

The symbols open and commit (arity 2) represent a commitment scheme, whereas the symbols sign, check (arity 2), getmsg, sk, and vk (arity 1) are used to model a signature scheme. Pairing is modelled using (arity 2), whereas projection functions are denoted proj 1 and proj 2 (arity 1). We also consider the symbols ⊕ and 0 to model the exclusive-or operator. Finally, we consider the function symbol eq to model equality test.

Equational theory

Following the approach developed in [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF], constructor terms are subject to an equational theory. This allows one to model the algebraic properties of the primitives. It consists of a finite set of equations of the form u = v where u, v ∈ T (Σ c , X ), and induces an equivalence relation = E over constructor terms. Formally, = E is the smallest congruence on constructor terms, which contains u = v in E, and that is closed under substitutions of terms for variables.

Example 2. To reflect the algebraic properties of the exclusive-or operator, we consider the equational theory E xor generated by the following equations:

(x ⊕ y) ⊕ z = x ⊕ (y ⊕ z) x ⊕ y = y ⊕ x x ⊕ 0 = x x ⊕ x = 0.

Rewriting rules

As in [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF], we also give a meaning to destructor symbols. This is done through a set of rewriting rules of the form g(t 1 , . . . , t n ) → t where g ∈ Σ d , and t, t 1 , . . . , t n ∈ T (Σ c , X ). A term u can be rewritten in v if there is a position p in u, and a rewriting rule g(t 1 , . . . , t n ) → t such that u| p = g(t 1 , . . . , t n )θ for some substitution θ. Moreover, we assume that t 1 θ, . . . , t n θ as well as tθ are messages. We only consider sets of rewriting rules that yield a convergent rewriting system, and we denote u↓ the normal form of a term u.

For modelling purposes, we split the signature Σ into two parts, Σ pub and Σ priv , and we denote Σ + pub = Σ pub ∪Σ 0 . An attacker builds messages by applying public symbols to terms he knows and that are available through variables in W. Formally, a computation done by the attacker is a recipe, i.e. a term in T (Σ + pub , W).

Example 3. Among symbols in Σ ex , only sk is in Σ priv . The properties of the symbols in Σ d are reflected through the following rewriting rules:

check(sign(x, sk(y)), vk(y)) → ok eq(x, x) → ok getmsg(sign(x, sk(y))) → x open(commit(x, y), y) → x proj 1 ( x 1 , x 2 ) → x 1 proj 2 ( x 1 , x 2 ) → x 2 .

Timed security protocols

In this section, we present our model which incorporates node location, time, and communication distance.

Process algebra

Protocols are modelled through processes using the following grammar:

P, Q := 0 | in(x).P | in <t (x).P | let x = v in P | new n.P | out(u).P | reset.P where x ∈ X , n ∈ N , u ∈ T (Σ + c , X N A), v ∈ T (Σ + , X N A) and t ∈ R + .
Most of these constructions are rather standard. As usual in symbolic models, 0 denotes the empty process that does nothing, and the new instruction is used to model fresh name generation. Then, we have standard constructions to model inputs and outputs. We may note the special construction in <t (x) that combines an input with a constraint on the local clock of the agent executing this action. This construction is in contrast with the approach proposed in e.g. [START_REF] Mauw | Distance-bounding protocols: Verification without time and location[END_REF] where input actions are not subject to any timing constraint, and are therefore always possible provided that enough time has elapsed. From this point of view, our model represents the reality more faithfully since an agent will not proceed an input arriving later than expected. The reset instruction will reset the local clock of the agent. Finally, the process let x = v in P tries to evaluate v, and in case of success the process P is executed; otherwise the process is blocked. In particular, this construction allows us to model the usual conditional operator relying on the destructor eq.

We write fv (P ) (resp. fn(P )) for the set of free variables (resp. names) occurring in P , i.e. the set of variables (resp. names) that are not in the scope of an input or a let (resp. a new). We consider parametrised processes, denoted P (z 0 , . . . , z n ), where z 0 , . . . , z n are variables from a special set Z (disjoint from X and W). Intuitively, these variables will be instantiated by agent names, and z 0 corresponds to the name of the agent that executes the process. A role R = P (z 0 , . . . , z n ) is a parametrised process that does not contain any agent name, and such that fv (R) ⊆ {z 0 , . . . , z n }. A protocol is then simply a set of roles.

Example 4. As a running example, we consider the signature-based Brands and Chaum distance bounding protocol [START_REF] Brands | Distance-bounding protocols[END_REF] that is informally described below:

1. P → V : commit(m, k) 2. V → P : n 3. P → V : n ⊕ m 4. P → V : k 5. P → V : sign( n, n ⊕ m , sk(P ))
The prover P generates a nonce m and a key k, and sends a commitment to the verifier V . The verifier V generates his own nonce n and initiates the time measurement phase, sometimed called the rapid phase. In this exchange, P answers with the exclusive-or of these two nonces. This step has to be done as quickly as possible since V will reject any answer arriving too late (a long response time does not give him any guarantee regarding its proximity with the prover). After this phase, P sends a means to open the commitment, as well as a signature on the values exchanged during the rapid phase. When a verifier ends a session of this protocol, the prover with whom he is communicating should be located in his neighbourhood. In our setting, the protocol is defined by the parametrised processes given below:

P (z P ) := new m.new k. out(commit(m, k)). in(x n ). out(x n ⊕ m). out(k). out(sign( x n , x n ⊕ m , sk(z P ))).0 V (z V , z P ) := in(y c ).new n.
reset.out(n).in <2×t0 (y 0 ). in(y k ).in(y sign ). let y m = open(y c , y k ) in let y check = check(y sign , vk(z P )) in let y eq = eq( n, n ⊕ y m , getmsg(y sign )) in 0.

Configuration and topology

Each process has a location. As in the classical Dolev-Yao model [START_REF] Dolev | On the security of public key protocols[END_REF], the attackers control the entire network but interacting with agents who are far away takes time. To formalise this, our execution model is parametrised by a topology.

Definition 1.

A topology is a tuple T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) where:

-A 0 ⊆ A is the finite set of agents composing the system; -M 0 ⊆ A 0 is the subset of agents that are dishonest; -Loc 0 : A 0 → R 3 is a mapping defining the position of each agent in space.

p 0 and v 0 are two agents in A 0 that represent respectively the prover and the verifier for which we analyse the security of the protocol.

In our model, the distance between two agents is expressed by the time it takes for a message to travel from one to another. Therefore, we consider Dist T0 : A 0 × A 0 → R, based on Loc 0 that will provide the time a message takes to travel between two agents. It is defined as follows:

Dist T0 (a, b) = Loc0(a)-Loc0(b) c0
for any a, b ∈ A 0 with • : R 3 → R the euclidian 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, any message emitted by any other agent b before t -Dist T0 (a, b).

Note that our model is not restricted to a single dishonest node. In particular, our results apply to the case of several compromised nodes that communicate (and therefore share their knowledge). However, communication is subject to physical constraints: message transmission takes time determined by the distance between nodes. All agents, including attackers, are subject to these constraints. This result in a distributed attacker with restricted, but more realistic, communication capabilities than those of the traditional Dolev-Yao attacker.

Our semantics is given by a transition system over configurations that manipulates extended processes, i.e. expressions of the form P a ta a with a ∈ A, P a a process such that fv (P a ) = ∅, and t a ∈ R + . Intuitively, P a describes the actions of agent a, and t a his local clock. In order to store the messages that have been outputted so far, we extend the notion of frame (introduced in [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]) to keep track of the time at which the message has been outputted and by whom.

Definition 2. Given a topology T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ), a configuration K over T 0 is a tuple (P; Φ; t), where:

-P is a multiset of extended process P t a with a ∈ A 0 ;

-Φ = {w 1 a1,t1 ---→ u 1 , . . . , w n an,tn ---→ u n } is an extended frame, i.e. a substitution such that w i ∈ W, u i ∈ T (Σ + c , N A), a i ∈ A 0 and t i ∈ R + for 1 ≤ i ≤ n; -t ∈ R + is the global time of the system.
We write Φ t a for the restriction of Φ to the agent a at time t, i.e. :

Φ t a = w i ai,ti ---→ u i | (w i ai,ti ---→ u i ) ∈ Φ and a i = a and t i ≤ t .
Example 5. Continuing Example 4, a topology T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) is depicted on the right where A 0 = {p 0 , v 0 , p}, and M 0 = {p 0 }. The precise location of each agent is not relevant, only the distance between them matters. Here, we assume that Dist T0 (p, v 0 ) < t 0 whereas Dist T0 (p 0 , v 0 ) ≥ t 0 . A typical configuration is:

v 0 p p 0 t 0 K 0 = ( P (p) 0 p V (v 0 , p 0 ) 0 v0 ; {w 1 p0,0 --→ sk(p 0 )}; 0)
where p is playing the role of the prover and v 0 the role of the verifier with a dishonest agent p 0 . The extended frame only contains the signature key of the dishonest agent, i.e. sk(p 0 ). A more realistic configuration would include other instances of these two roles and will give more knowledge to the attacker, but we will see that this configuration is already sufficient to present an attack.

Semantics

Given a topology T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ), the operational semantics of processes is formally defined by the rules given in Figure 1. The TIM rule allows time to elapse meaning that the global clock as well as the local clocks will be shifted by δ as formally defined below:

Shift(P, δ) = P ∈P Shift(P, δ) and Shift( P ta a , δ) = P ta+δ a . The RST rule allows an agent to reset his local clock. The other rules are rather standard. The IN rule allows an agent a to evolve when receiving a message. Note that, such a message has necessarily been sent at time t b by some other agent b who has to be in possession of all the necessary information at that time. We sometimes simply write -→ T0 instead of a,α --→ T0 . The relation → * T0 is the reflexive and transitive closure of → T0 , and we often write tr -→ T0 to emphasise the sequence of labels tr that has been used during this execution. Example 6. Continuing Example 5, the following sequence of transitions is enabled from the configuration K 0 :

K 0 p,τ --→ T0 p,τ --→ T0 p,out(commit(m ,k )) -------------→ T0 - → T0 v0,in(commit(m ,k )) -------------→ T0 v0,τ ---→ T0 v0,τ ---→ T0 K 1
-if b ∈ A0 M0 then u ∈ img( Φ t b b ); -if b ∈ M0 then u = RΦ↓ for some recipe R such that for all w ∈ vars(R) there exists c ∈ A0 such that w ∈ dom( Φ t b -Dist T (c,b) c ).
Moreover, in case is < tg for some tg, we assume in addition that ta < tg. where

K 1 = ( P 1 δ0 p V 1 0 v0 ; {w 1 p0,0 --→ sk(p 0 ), w 2 p,0
--→ commit(m , k )}; δ 0 ). The processes located in p and v 0 have evolved. We have that:

-P 1 = in(x n ).out(x n ⊕ m ).out(k ).out(sign( x n , x n ⊕ m , sk(p))); and -V 1 = out(n ).in <2×t0 (y 0 ).in(y k ).in(y sign ).let y m = open(y c , y k ) in . . . This corresponds to the beginning of a normal execution between p and v 0 . The two first transitions have been triggered using the NEW rule. The third one is an instance of the rule OUT. The message outputted at location p is received at location v 0 , but an instance of the rule TIM (here with δ 0 = Dist T0 (p, v 0 )) is needed to allow the message to reach this location.

Security properties

A distance bounding protocol is a protocol in which a party (the verifier) is assured of the identity of another party (the prover), as well as the fact that this prover is located in his neighbourhood. Several frauds against distance bounding protocols are usually considered. We introduce in Section 4.2 the ones that will be studied in this paper, and we explain how they will be formalised. Before to do that, we introduce the notion of t 0 -proximity and the notion of valid initial configuration that aims to represent all the scenarios that have to be analysed once the topology has been fixed.

Physical proximity on a given topology

For the sake of simplicity, we assume that processes representing instances of distance bounding protocols contain a process (typically a session of the verifier) that ends with a special action of the form end(v, p). Checking whether a protocol ensures physical proximity w.r.t. a given configuration K 0 is defined as follows.

Definition 3. Let T 0 be a topology and K 0 be a configuration over T 0 . We say that K 0 admits an attack w.r.t. t 0 -proximity in T 0 if

K 0 → * T0 ( end(a 1 , a 2 ) ta a P; Φ; t) with Dist T0 (a 1 , a 2 ) ≥ t 0 .
Of course, when analysing a distance bounding protocol, not all the configurations are interesting. Depending on the type of fraud under consideration, we explain in Definition 4 the configurations that are initial valid configurations, and therefore have to be analysed before declaring whether a protocol is secure or not.

K 0 = ( P (p) 0 p V (v 0 , p 0 ) 0 v0 ; {w 1 p0,0 --→ sk(p 0 )}; 0)
where V (z V , z P ) is V (z V , z P ) in which the occurrence of the process null has been replaced by end(z V , z P ). The sequence of transitions described in Example 6 is still possible ending in

K 1 = ( P 1 δ0 p V 1 0 v0 ; {w 1 p0,0 --→ sk(p 0 ), w 2 p,0 --→ commit(m , k )}; δ 0 ) where V 1 is V 1 in
which the occurrence of the process null has been replaced by end(v 0 , p 0 ). Now, we can pursue this execution as follows:

K 1 v0,out(n ) ------→ T0 - → T0 p,in(n ) -----→ T0 p,out(n ⊕m ) --------→ T0 p,out(k ) -----→ T0 - → T0 v0,in <2×t 0 (n ⊕m ) ------------→ T0 v0,in(k ) -----→ - → T0 v0,in(sign( n ,n ⊕m ,sk(p0))) -------------------→ ( P 2 3δ0+2δ 0 p end(v 0 , p 0 ) 2δ0+2δ 0 v0 ; Φ; 3δ 0 + 2δ 0 )
The two first lines correspond to a normal execution of the protocol between v 0 and p. Note that, on each line, we need an instance of the TIM rule with δ 0 = Dist T0 (v 0 , p) = Dist T0 (p, v 0 ) to allow the sent message to reach its destination. The last transition does not follow the normal execution of the protocol. Actually, the dishonest agent p 0 is responsible of this input. He built this message from the messages n and n ⊕ m that have been sent on the network, and the key sk(p 0 ) that is part of his initial knowledge. Note that he has to wait the necessary amount of time to allow these messages to reach him (e.g. δ 0 = Dist T0 (v 0 , p 0 )), and some time is needed for the forged message to reach v 0 (actually δ 0 = Dist T0 (v 0 , p 0 )). Therefore, the first rule of the last line is an instance of the TIM rule during which a delay of 2δ 0 has elapsed. Note that, according to Definition 5, this corresponds to an attack w.r.t. t 0proximity on configuration K 0 . Actually, this is the hijacking attack that has been reported in [START_REF] Cremers | Distance hijacking attacks on distance bounding protocols[END_REF] and described in Figure 2. Here, a dishonest prover p 0 exploits an honest prover p (located in the neighbourhood of v 0 ) to provide the verifier v 0 with false information about the distance between p 0 and v 0 .

Once the topology T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) is fixed, when analysing whether a protocol is secure or not, we have to consider any configuration that is valid w.r.t. the given topology. We consider a protocol P prox , and we assume that the initial knowledge of dishonest participants is given through a template I 0 , i.e. a set of terms in T (Σ + c , Z). Using this template I 0 , and considering a set of agents A 0 , we derive the initial knowledge of agent a ∈ A 0 as follows:

Knows(I 0 , a, A 0 ) = {(u 0 {z 0 → a})σ ground | u 0 ∈ I 0 and img(σ) ⊆ A 0 }. Definition 4. Let P prox be a protocol, V 0 (z 0 , z 1 ) be a parametrised role containing the special action end(z 0 , z 1 ), I 0 be a template, and T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) be a topology. A configuration K = (P; Φ; t) is a valid initial configuration for the protocol P prox and V 0 w.r.t. T 0 and I 0 if:

1. P = V 0 (v 0 , p 0 ) t v0
P for some t and for each P t a ∈ P there exists P (z 0 , . . . , z k ) ∈ P prox , and a 1 , . . . , a k ∈ A 0 such that P = P (a , a 1 , . . . , a k ). 2. img( Φ t a ) = Knows(I 0 , a, A 0 ) when a ∈ M 0 , and img( Φ t a ) = ∅ otherwise.

When t = 0 and t = 0 for each P t a ∈ P and each {w a ,t ---→ u} ∈ Φ, we say that K is a zero-configuration.

The first condition says that we consider initial configurations made up of instances of the roles of the protocols, and we only consider roles executed by agents located at the right place. The second condition allows one to give some initial knowledge to each malicious node. We may note that we do not give so much constraints regarding time. It is indeed important that all the possible initial configurations are analysed before declaring a protocol secure.

Example 8. Going back to Example 7 and considering the template I 0 = {sk(z 0 )}, we have that K 0 is a valid initial zero-configuration.

Definition 5. Let P prox be a protocol, V 0 (z 0 , z 1 ) be a parametrised role containing the special action end(z 0 , z 1 ), I 0 be a template, and T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) be a topology. We say that P prox admits an attack w.r.t. t 0 -proximity in T 0 if there exists a valid initial configuration K for P prox and V 0 w.r.t. T 0 and I 0 such that K admits an attack w.r.t. t 0 -proximity in T 0 . We say that P prox admits a zero-attack when in addition K is a zero-configuration.

When analysing a protocol, it is generally sufficient to consider valid initial configurations that are zero-configurations.

Proposition 1. Let P prox be a protocol, V 0 (z 0 , z 1 ) be a parametrised role containing the action end(z 0 , z 1 ), I 0 be a template, and T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) be a topology. Moreover, we assume that any guarded input in P prox and V 0 is preceded by a reset. We have that P prox admits an attack w.r.t. t 0 -proximity in T 0 if, and only if, P prox admits a zero-attack w.r.t. t 0 -proximity in T 0 .

Classification of attacks

We consider different types of attacks as it is usually done in distance bounding protocols. We do not consider here the notion of terrorist fraud since this notion relies on the fact that an attacker located in the neighbourhood of the verifier helps the prover located outside the neighbourhood. This may require the dishonest prover to share some knowledge with the attacker but without giving him any advantage for future attacks (in particular without revealing him all his credential). This does not fit in our model since here we assume colluding attackers who share their knowledge (provided that enough time has elapsed).

Distance fraud. A distance fraud is an attack where a dishonest prover who is far away succeeds in convincing an honest verifier that he is actually close to him. In general, it is supposed that this dishonest prover cheats without help of other entities located in the neighbourhood of the verifier. Therefore, when considering distance fraud, we only have to consider topologies T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) as follows:

p 0 ∈ M 0 , v 0 ∈ A 0 M 0 ,
and Dist T0 (v 0 , a) ≥ t 0 for any a ∈ A 0 {v 0 , p 0 }.

We denote C DF the set of topologies that satisfy these requirements. We may note that the valid initial configurations corresponding to such a topology will allow the agent v 0 to execute any role of the protocol an arbitrary number of times. This corresponds to a more complex scenario than those usually analysed in the context of distance fraud. Therefore, we will also consider the notion of simple distance fraud for which the agent v 0 is only authorised to execute the parametrised role V 0 (z 0 , z 1 ). Mafia fraud. A mafia fraud is an attack in which generally three agents are involved: a verifier, an honest prover located outside the neighbourhood of the verifier, and an external attacker. This attacker performs a man-in-the-middle attack between the verifier and the prover with the aim of convincing the verifier that the honest prover is actually close to it. Therefore, when considering mafia fraud, we consider topologies T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) that are as follows: both v 0 and p 0 are honest, i.e. v 0 , p 0 ∈ A 0 M 0 .

We denote C MF the set of topologies that satisfy these requirements.

Distance hijacking fraud.

A distance hijacking fraud is an attack in which a dishonest prover located far away succeeds in convincing an honest verifier that he is actually close to him. Contrary to the notion of distance fraud, the dishonest prover may exploit honest entities located in the neighbourhood of the verifier. Therefore, we only have to consider topologies T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) that are as follows:

p 0 ∈ M 0 , v 0 ∈ A 0 M 0 , and Dist T0 (v 0 , a) ≥ t 0 for any a ∈ M 0 .
We denote C DH the set of topologies that satisfy these requirements. Definition 6. Let P prox be a protocol, V 0 (z 0 , z 1 ) be a parametrised role containing the special event end(z 0 , z 1 ), and I 0 be a template. We say that P prox admits a distance fraud attack (resp. mafia fraud attack, distance hijacking attack) w.r.t. t 0 -proximity if there exist T ∈ C DF (resp. C MF , C DH ), a valid initial configuration K for P prox and V 0 w.r.t. T and I 0 such that K admits an attack w.r.t. t 0 -proximity in T .

Moreover, in case T ∈ C DF and V 0 is the only process located in v 0 in the configuration K, then such an attack is called a simple distance fraud attack.

Our main contribution is to provide reduction results that allow one to analyse the security of a protocol w.r.t. the frauds mentioned above considering only a specific topology. Then, we will show how to leverage an existing tool ProVerif to automatically analyse this notion of physical proximity.

Reducing the topology

Our reduction results allow one to analyse the security of a protocol considering only a specific topology. Each result is specific to a particular fraud but their proofs rely on some common ingredients. In each case, we succeed in providing a unique topology on which it is actually sufficient to perform the security analysis. These topologies are rather simple (at most four agents) and are depicted below for each type of fraud. Regarding distance fraud w.r.t. t 0 -proximity, the topology T t0 DF is as follows:

T t0 DF = ({p 0 , v 0 }, {p 0 }, Loc DF , v 0 , p 0 ) with Dist T t 0 DF (p 0 , v 0 ) = t 0 .
This topology is not uniquely defined. However, since our semantics only depends on the distance between agents (and not on their locations), it should be clear that we can consider an arbitrary one that fulfills the conditions expressed above.

Theorem 1. Let P prox be a protocol, V 0 (z 0 , z 1 ) be a parametrised role containing the special event end(z 0 , z 1 ), and I 0 be a template. We have that P prox admits a distance fraud attack w.r.t. t 0 -proximity, if and only if, there is an attack against t 0 -proximity in the topology T t0 DF .

Proof. (Sketch) We consider an attack trace in

T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) ∈ C DF . K 0 - → * T ( end(v 0 , p 0 ) tv v0 P; Φ; t) with Dist T (v 0 , p 0 ) ≥ t 0
We proceed in two main steps:

1. We show that the same trace can be done in a topology where all the agents in A 0 are moved into an existing location in T t0 DF . More precisely, all the agents except v 0 are moved at Loc DF (p 0 ) whereas v 0 is moved at Loc DF (v 0 ). We may note that the distance between any two agents has been shorten (keeping p 0 and v 0 far away), and thus the trace can still be done. 2. Then, we apply a renaming of agents preserving their location. The trace is still executable, and we show that the resulting initial configuration (the one after application of the renaming) is still a valid initial configuration.

In particular, the renaming used in the second step of the proof will leave v 0 unchanged. Therefore, a valid initial configuration built on T w.r.t. the simple distance fraud scenario will be transformed into a valid initial configuration built on T t0 DF w.r.t. the simple distance fraud scenario, i.e. V 0 (v 0 , p 0 ) will be the only process located in v 0 .

Mafia fraud

Regarding mafia fraud, T t0

MF is as follows:

T t0 MF = (A MF , M MF , Loc MF , v 0 , p 0 ) with A MF = {p 0 , v 0 , i 1 , i 2 }, M MF = {i 1 , i 2 }, Loc MF (v 0 ) = Loc MF (i 1 ), Loc MF (p 0 ) = Loc MF (i 2 ), and Dist T t 0 MF (p 0 , v 0 ) = t 0 .
However, we may note that the reduction we did in case of distance fraud is not possible anymore since it will require to lengthen the distance between some nodes. Typically a node n in the neighborhood of v 0 would be shifted at the same location as v 0 but this would lengthen the distance between n and p 0 . Since dishonest participants are allowed in the neighbourhood of v 0 , getting some inspiration from [START_REF] Nigam | Towards the automated verification of cyber-physical security protocols: Bounding the number of timed intruders[END_REF], we consider a dishonest participant right next to each honest participant. Such a dishonest participant is ideally located to forge and send messages that will be received by the honest agent close to him.

However, contrary to the result provided in [START_REF] Nigam | Towards the automated verification of cyber-physical security protocols: Bounding the number of timed intruders[END_REF], our goal is not only to reduce the number of dishonest agents but also the number of honest agents that are involved in an attack trace. In order to ensure that moving (and reducing) the honest agents will not cause any trouble, we need an extra assumption. We require that each role of the protocol is executable. This is a reasonable assumption that will allow one to discard any role executed by a malicious participant. Intuitively, all these operations will be done directly by the attacker. Definition 7. Given a template I 0 = {u 1 , . . . , u k }, we say that a parametrised role P (z 0 , ..., z n ) is I 0 -executable if fv (P ) ⊆ {z 0 , ..., z n }, fn(P ) = ∅ and for any term u (resp. v) occurring in an output or a let construction, there exists

R ∈ T (Σ + pub , {w 1 , . . . , w k } N X ) such that u = Rσ↓ (resp. v↓ = Rσ↓) where σ = {w 1 → u 1 , . . . , w k → u k }. A protocol P is I 0 -executable if each role of P is I 0 -executable.
Example 9. Going back to our running example given in Example 4. We have that P (z 0 ) is {sk(z 0 )}-executable whereas V (z 0 , z 1 ) is {z 1 }-executable. Therefore, we have that the protocol made of these two roles is {sk(z 0 ), z 1 }-executable.

Theorem 2. Let I 0 be a template, P prox be a protocol I 0 -executable, and V 0 (z 0 , z 1 ) be a parametrised role containing the special event end(z 0 , z 1 ). We have that P prox admits a mafia fraud attack w.r.t. t 0 -proximity, if and only if, there is an attack against t 0 -proximity in the topology T t0 MF . Proof. (Sketch) We consider an attack trace in T

= (A 0 , M 0 , Loc 0 , v 0 , p 0 ) ∈ C MF . K 0 - → * T ( end(v 0 , p 0 ) tv v0
P; Φ; t) with Dist T (v 0 , p 0 ) ≥ t 0 . We proceed in three main steps:

1. We reduce the number of active agents (those that are actually executing a process) -we do this for honest and malicious agents. We transform honest agent (but v 0 and p 0 ) into malicious ones. This intuitively gives more power to the attacker, and malicious agents in the neighborhood of v 0 are allowed in a mafia fraud scenario. Then, relying on our executability condition, we discard processes executed by malicious agents. These actions can actually be mimicked by an attacker located at the same place. 2. We reduce the number of attackers by placing them ideally (one close to each honest agent). Since we have removed all honest agents but two, we obtain a topology with only two dishonest agents.

3. To conclude, as in the case of a distance fraud attack, we reduce the knowledge showing that we can project all the dishonest agents that are located in v 0 on i 1 and all the dishonest agents that are located in p 0 on i 2 .

Distance hijacking attack

First, we may note that the reduction we did in case of distance fraud or mafia fraud are not possible anymore. Clearly, we need to consider honest participants in the neighbourhood of the verifier and moving them on the same location as v 0 will lengthen the distance with p 0 . Moreover, there is no hope to reduce the number of attackers by placing them close to each honest participant since this will introduce a malicious node in the neighbourhood of v 0 . This is forbidden when considering a distance hijacking scenario. Actually, adding such a dishonest node in the neighbourhood of v 0 will always introduce a false attack since in our model dishonest participants share their knowledge. Therefore, this dishonest participant would be able to play the role of the prover as if he was the dishonest prover p 0 (who is actually far away). Nevertheless, we will show that under reasonable conditions, we can reduce towards the topology T t0 DH which is made up of 3 agents. More formally,

T t0 DH = (A DH , M DH , Loc DH , v 0 , p 0 ) with A DH = {p 0 , v 0 , e 0 }, M DH = {p 0 }, Loc DH (p 0 ) = Loc DH (e 0 ),

and

Dist T t 0 DH (p 0 , v 0 ) = t 0 .
Given a process P , we denote P the process obtained from P by removing reset instructions, and replacing all the occurrences of in <t (x) by in(x). Theorem 3. Let I 0 be a template, P prox be a protocol, t 0 ∈ R + , and V 0 (z 0 , z 1 ) be a parametrised role obtained using the following grammar:

P, Q := end(z 0 , z 1 ) | in(x).P | let x = v in P | new n.P | out(u).P | reset.out(u ).in <t (x).P where x ∈ X , n ∈ N , u, u ∈ T (Σ + c , X ∪N ∪{z 0 , z 1 }), v ∈ T (Σ + , X ∪N ∪{z 0 , z 1
}) and t ≤ 2 × t 0 . If P prox admits a distance hijacking attack w.r.t. t 0 -proximity, then P prox admits an attack against t 0 -proximity in the topology T t0 DH . In order to establish such a result, the idea is to move honest participants in the neighbourhood of v 0 at the same location as v 0 . However, this will lengthen the distance between such an agent and those that are far away from v 0 , and thus some messages will be forgeable only after some extra delay. This can be a problem in case such a message is useful to pass the guarded input. Thus, we will first transform the initial attack trace into an "attack" trace in an untimed model. This model (with no timing constraints to fullfill) is more suitable to reorder some actions in the trace. We will show in a second step how to come back in the original timed model.

As briefly explained above, we consider the untimed configuration associated to a configuration K = (P; Φ; t). Formally, we have untimed(K) = (P ; Φ ) with:

-P = { P a | P t a ∈ P for some t}, and

-Φ = {w a -→ u | w a,t --→ u ∈ Φ for some t}.
Then, we consider a relaxed semantics over untimed configurations: K a,α T K if there exist K 0 and K 0 such that K 0 a,α --→ T K 0 (for some rule other than the TIM rule), and for which K = untimed(K 0 ) (resp. K = untimed(K 0 )).

Under the same hypotheses as those stated in Theorem 3, we establish a result that allows one to "clean" an attack trace by pushing instructions (before or after) outside the rapid phase delimited by a reset and its following guarded input. In the resulting trace, the only remaining actions in the rapid phase are those performed by agents who are close to v 0 . Proposition 2. Let K 0 be a valid initial configuration for P prox and V 0 w.r.t. a topology T = (A 0 , M 0 , Loc, v 0 , p 0 ) and

I 0 . If K 0 tr -→ T K 1 then there exists an execution K 0 tr K 1 such that K i = untimed(K i ) for i ∈ {0, 1}.
Moreover, for any sub-execution of K 0 tr K 1 of the form

( reset.P v0 P; Φ reset ) v0,τ ( P v0 P; Φ reset ) tr 0 K - in v0,in <t (u) K in
where tr 0 only contains actions (a, α) with α ∈ {τ, out(u), in(u)}, we have that:

-2Dist T (v 0 , a) < t for any (a, α) ∈ tr 0 ; for any (a, in (v)) occurring in tr 0 .(v 0 , in <t (u)), the agent b responsible of the output and the recipe R (as defined in Figure 1) are such that either 2Dist T (v 0 , b) < t, or vars(R) ⊆ dom(Φ reset ).

We are now able to prove our result regarding distance hijacking frauds.

Proof. (Sketch)

1. We start by removing reset instructions and by transforming any guarded input (but those in V 0 ) into simple inputs. The resulting trace is still an attack trace w.r.t. P prox . 2. Then, we apply Proposition 2 in order to obtain an attack trace in the relaxed semantics. We will exploit the extra conditions given by Proposition 2 in order to lift the trace in the timed model at step 4.

We now consider another topology T with two locations (as T t0

DH ) and such that agents close to v 0 are now located with v 0 , and those that are far away from v 0 in T are now located with p 0 . This execution is still a valid trace in T since we consider the relaxed semantics. 4. Then, to lift this execution trace into our timed model, the basic idea is to wait enough time before a reset instruction to allow messages to be received by all the participants before starting the rapid phase. 5. To conclude, as in the previous attack scenarios, we reduce the initial knowledge and the number of agents by applying a renaming on agent names.

In (i : in(x).P P; φ; i)

in(u)
= == ⇒ (i : P {x → u} P; φ; i) where R is a recipe such that Rφ↓ = u is a message.

Out (i : out(u).P P; φ; i)

phase i = === ⇒ (P; φ; i ) with i > i.
Phase (i : i : P P; φ; i) τ = ⇒ (i : P P; φ; i) Fig. 4: Semantics for processes with phases 6 Getting rid of the topology

We have reduced the topology but we have still to take into account it when analysing the protocol preventing us to use automatic verification tool dedicated to traditional security protocol such as ProVerif [START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF]. In this section, we will explain how to get rid of the resulting topology and obtain interesting results on timed protocols relying on the notion of phases that is offered to us in ProVerif.

ProVerif in a nutshell

We consider a subset of the ProVerif calculus defined as follows:

P, Q := 0 | in(x).P | let x = v in P | new n.P | out(u).P | i : P | !P where x ∈ X , n ∈ N , u ∈ T (Σ + c , X ∪ N ∪ A), v ∈ T (Σ + , X ∪ N ∪ A) and i ∈ N.
The semantics is similar to the one introduced earlier, and formally defined through a relation, denoted = ⇒, over configurations. A configuration is a tuple (P; φ; i) where P is a multiset of processes (as given by the grammar), φ is a frame as usual (with no decoration on the arrow), and i ∈ N is an integer that indicates the current phase. Intuitively, the process !P executes P an arbitrary number of times (in parallel), and only processes in the current phase are allowed to evolve. We often write P instead of 0 : P .

Our transformation

Given a topology T (typically one in Figure 3), a protocol P prox , a role V 0 , and a template I 0 , we build a configuration (P; φ; 0) on which the security analysis could be done using ProVerif. From now on, we assume that V 0 (v 0 , p 0 ) only contains one block of the form reset.out(m).in <t (x), i.e. it is of the form: block 1 . reset . out(m) . in <t (x) . block 2 . end(v 0 , p 0 ) where block i is a sequence of actions (only simple inputs, outputs, let, and new instructions are allowed).

The main idea is to use phase 1 to represent the critical phase. Such a phase starts when V 0 performs its reset instruction, and ends when V 0 performs its in <t (x) instruction. During this critical phase, only participants that are close enough to V 0 can manipulate messages outputted in this critical phase. The other ones are intuitively too far. Therefore, we mainly consider two transformations, namely F < and F ≥ , whose purposes are to transform a parametrised role of our process algebra given in Section 3.1 (with no reset instruction and no guarded input) into a process in the ProVerif calculus.

transformation F < : this transformation introduces the phase instructions with i = 0, 1 and 2 considering all the possible ways of splitting the role into three phases (0, 1, and 2). Each phase instruction is placed before an in instruction. Such a slicing is actually sufficient for our purposes. transformation F ≥ : this transformation does the same but we forbid the use of the instruction phase 1, jumping directly from phase 0 to phase 2.

The configuration, denoted F(T , P prox , V 0 , I 0 , t 0 ), is the tuple (P; φ; 0) where φ is such that img(φ) = a∈M0 Knows(I 0 , a, A 0 ), and P is the multiset that contains the following processes (assuming in addition that a 0 = v 0 when considering the simple distance fraud scenario):

-block 1 . 1 : out(m) . in <t (x) . 2 : block 2 . end(v 0 , p 0 ); -!R(a 0 , .., a n ) when R(z 0 , .., z n ) ∈ F < (P prox ), a 0 , .., a n ∈ A 0 , Dist T (v 0 , a 0 ) < t 0 ; -!R(a 0 , .., a n ) when R(z 0 , .., z n ) ∈ F ≥ (P prox ), a 0 , .., a n ∈ A 0 , Dist T (v 0 , a 0 ) ≥ t 0 ;
Relying on Proposition 2, we are able to establish the following result that justifies the transformation presented above. Proposition 3. Let T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) be a topology, P prox a protocol, t 0 ∈ R + , I 0 a template, and V 0 (z 0 , z 1 ) a parametrised process of the form: block 1 . reset . out(m) . in <t (x) . block 2 . end(z 0 , z 1 ) with t ≤ 2 × t 0 Let K 0 be a valid initial configuration for the protocol P prox and V 0 w.r.t. T and I 0 . If K 0 admits an attack w.r.t. t 0 -proximity in T , then we have that:

F(T 0 , P prox , V 0 , I 0 , t 0 ) tr = ⇒ ({2 : end(v 0 , p 0 )} P; φ; 2).
Moreover, in case there is no a ∈ M 0 such that Dist T0 (a, v 0 ) < t 0 , we have that for any in(u) occurring in tr during phase 1, the underlying recipe R is either of the form w, or only uses handles ouputted in phase 0.

We will see in the following section how this result can be used to turn any attack scenario corresponding to a distance fraud (resp. mafia fraud) into a reachability property, namely the reachability of the event end. Regarding distance hijacking, in order to avoid false attacks, we will exploit the additional condition stated at the end of Proposition 3. In particular, a slight modification of the ProVerif code consisting in discarding some attacker behaviours will give us enough precision to obtain meaningful results.

7 Case studies using ProVerif

Methodology

Let P prox be a protocol for which we want to establish the absence of attacks w.r.t. t 0 -proximity. Regardless of the type of the considered attack, thanks to our reduction results (Section 5), we only need to consider a single topology (one depicted in Figure 3). Once down to this single topology, we can apply Proposition 3, and analyse the configuration (P; φ; 0) = F(T t0 XX , P prox , V 0 , I 0 , t 0 ) with XX ∈ {DF, MF, DH} in ProVerif. If the protocol is proved secure, then P prox is resistant to the class of attacks we have considered. Otherwise, the trace returned by ProVerif can be analysed to see if it is executable in our timed semantics, and thus corresponds to a real attack.

Actually, to obtain meaningful results regarding scenarios that only involved honest participants in the neighbourhood of v 0 , we have to go one step further. Indeed, the attacker model behind ProVerif allows him to interact with any participant (even those that are far away) with no delay. To avoid these behaviours that are not possible in the rapid phase, we slightly modify the ProVerif code taking advantage of the extra condition stated in Proposition 3. During phase 1, we consider an attacker who is only able to forward messages previously sent, and forged new messages using his knowledge obtained in phase 0. We also note that, due to some optimisations in ProVerif code, we couldn't prevent the attacker from using native tuples in phase 1, therefore, we model tuples using our own function symbols.

Application to distance bounding protocol

In this section, we apply our methodology to a number of well-known distance bounding protocols. However, they may have been abstracted to be analysed in the symbolic framework. In particular, in symbolic models, it is not possible to reason at the bit-level, and therefore we replace the bit-sized exchanges by a single challenge-response exchange using a fresh nonce (as done in Example 4). Sometimes, we also abstract the answer from the prover relying on an uninterpreted function symbol with relevant arguments. Finally, in order to rely on ProVerif, the xor operator has been abstracted (even if our theoretical development is generic enough to deal with such an operator). In constrast with [START_REF] Mauw | Distance-bounding protocols: Verification without time and location[END_REF] in which the xor operator is fully abstracted relying on a non interpreted function symbol, we actually model it through the following rewriting rules:

(x ⊕ y) ⊕ x → y (x ⊕ y) ⊕ y → x x ⊕ (x ⊕ y) → y y ⊕ (x ⊕ y) → x
In Figure 5, we present the protocols we have analysed using our methodology (plain arrows denote the rapid exchange phase). The Meadows et al. protocol [START_REF] Meadows | Distance bounding protocols: Authentication logic analysis and collusion attacks[END_REF] has been studied with two different functions F (n V , n P , P ) = (n V ⊕ n P , P ) and F (n V , n P , P ) = (n V , n P ⊕ P ) using the weaken xor operator: the first one has been proved secure, while the second one is vulnerable to an attack. All the results are presented in Table 1. We can note that due to the abstractions we Hancke and Kuhn × × Swiss-Knife [START_REF] Kim | The swiss-knife RFID distance bounding protocol[END_REF] Munilla et al. [START_REF] Munilla | Distance bounding protocols for rfid enhanced by using void-challenges and analysis in noisy channels[END_REF] TREAD-Asymmetric [START_REF] Avoine | A terrorist-fraud resistant and extractor-free anonymous distancebounding protocol[END_REF] × × × TREAD-Symmetric [START_REF] Avoine | A terrorist-fraud resistant and extractor-free anonymous distancebounding protocol[END_REF] × × CRCS [START_REF] Rasmussen | Realization of rf distance bounding[END_REF] × ×

V(k) P(k) new s, s commit(s, s ) new b r b ⊕ s s , Mac k (b, s) MAD (One-Way) V(k) P(k) new nV new nP nV nP new b b Z0 = h0(nP , k) Z1 = Z0 ⊕ k f(b, Z0, Z1) h1(c, nV , nP , k), b Swiss-Knife V(k) P(k) new nV new nP nP nV D = h0(nV , nP , k) w = h1(nV , nP , k) new b S = h2(b, D) f(S, w) h3(w, k),
Hancke and Kuhn [START_REF] Hancke | An RFID distance bounding protocol[END_REF] Tree-based [START_REF] Avoine | An efficient distance bounding rfid authentication protocol: balancing false-acceptance rate and memory requirement[END_REF] Poulidor [START_REF] Trujillo-Rasua | The poulidor distance-bounding protocol[END_REF] Uniform [START_REF] Mauw | A class of precomputation-based distance-bounding protocols[END_REF] Table 1: Results on our case studies (×: attack found, : proved secure) (s)DF = (simple) Distance Fraud, MF = Mafia Fraud, DH = Distance Hijacking comparison, the methodology proposed by Mauw et al. in [START_REF] Mauw | Distance-bounding protocols: Verification without time and location[END_REF] requires to use a specific model of the protocol to retrieve it (e.g. some rules need to be duplicated to simulate some algebraic properties of the xor operator). Another interesting point is that we succeed in proving resistance against mafia fraud for the first version of the Meadows et al. protocol (using our weakened xor) which could not be proved using the framework proposed in [START_REF] Meadows | Distance bounding protocols: Authentication logic analysis and collusion attacks[END_REF].

Our analysis has been performed using a 64-bit MacOs HighSierra computer with 16 Go of RAM memory and a processor Intel Core i5-7287U CPU 3.30GHz. ProVerif always answers in less than one seconds, and we may note that all the traces retuned by ProVerif correspond to real traces (no false positive).

Application to the Paysafe protocol

In addition to standard distance bounding protocol, we studied an EMV payment protocol, PaySafe [START_REF] Chothia | Relay cost bounding for contactless EMV payments[END_REF], designed to be resistant against mafia fraud attacks. More generally, contactless payment protocols need to prevent relay attacks where malicious agents would abuse from an honest agent to perform a payment, which is the mafia fraud scenario.

The Paysafe protocol is schematised in Figure 6 where plain arrows represents the rapid exchange phase. During the initialisation phase, the reader and the card exchange some identifiers, while during the authentication exchange, the reader ensures that the card is legitimate using signatures and certificates verifications. The main idea is to send nonces and constants during the rapid exchange phase (and perform verifications later) since this can always be done in a short amount of time, therefore, increasing the accuracy on the proximity property needed to ensure the security of the protocol. We also considered two other versions of PaySafe, also described in [START_REF] Chothia | Relay cost bounding for contactless EMV payments[END_REF], where nonces from the Reader and the Card are removed. Our results, obtained using our methodology with ProVerif, confirmed those presented in [START_REF] Chothia | Relay cost bounding for contactless EMV payments[END_REF]. One would note that their methodology and ours, especially when it comes down to the use of ProVerif, are quite similar but we would like to emphasise the fact that our use of ProVerif is a consequence of our formal development. This protocol has also been verified in [START_REF] Mauw | Distance-bounding protocols: Verification without time and location[END_REF]. The authors of [START_REF] Mauw | Distance-bounding protocols: Verification without time and location[END_REF] reported a distance fraud attack which is not relevant in this context. Their methodology does not allow them to restrict their analysis to the case of mafia fraud scenario. In contrast, our methodology is flexible enough and thus more suitable in this context.

Conclusion

Regarding physical proximity we have shown several reduction results: if there is an attack on an arbitrary topology then there is an attack on a simple one having at most four nodes. Relying on these reduction results, we have shown how to use ProVerif to analyse several protocols provided they make use of primitives supported by the tool. Moreover, our methodology is flexible enough to draw meaningful conclusion on each class of attacks (distance fraud, hijacking attack, mafia fraud).

Our model suffers from some restrictions that prevents it to be used to analyse some scenarios. For instance, we do not consider the notion of terrorist fraud since this would require to consider dishonest participants who only share a part of their knowledge. Another possible extension would be to take also into account the fact that computing messages takes time as it was done e.g. in [START_REF] Cheval | Timing attacks in security protocols: symbolic framework and proof techniques[END_REF], or to consider channels having different speeds. To go even further, quantitative analysis relying on probabilistic models such as those developed in [START_REF] Chadha | Verification of randomized security protocols[END_REF] would be beneficial.

A Proof of Proposition 1

Proposition 1 is a direct consequence of Proposition 4 stated and proved below. Indeed, it is easy to see that when K is a valid initial configuration then K 0 is also a valid initial configuration, and K 0 is actually a zero-configuration. Moreover, in case the execution K -→ * T K under study is an attack trace, then the resulting execution K 0 = (P 0 ; Φ 0 ; 0) -→ * T K 0 is also an attack trace.

Proposition 4. Let T = (A 0 , M 0 , Loc, v 0 , p 0 ) be a topology and K = (P; Φ; t) be a configuration such that any guarded input in P is preceded by a reset. Let K = (P ; Φ ; t ) be a configuration such that K tr -→ T K .

Let

P 0 = { P 0 a | P ta a ∈ P}, and Φ 0 = {w a,0 --→ u | w a,ta
--→ u ∈ Φ}. We have that K 0 = (P 0 ; Φ 0 ; 0) tr -→ T K 0 for some K 0 = (P 0 ; Φ 0 ; t 0 ) such that:

1. {(P, a) | P a ∈ P } = {(P, a) | P a ∈ P 0 }; 2. {(w, a, u) | w a, --→ u ∈ Φ } = {(w, a, u) | w a, --→ u ∈ Φ 0 }.
Proof. We prove the result together with the additional properties stated below by induction on the length of the derivation K tr -→ T K = (P ; Φ Ψ ; t ).

(i) if P ta a ∈ P and P contains a guarded input that is not preceded by a reset then P ta a ∈ P 0 (with the same value for t a ); (ii) t 0 = t -t + δ where δ = max({Dist

T (a, b) | a, b ∈ A 0 } ∪ {t}); (iii) Φ 0 = Φ 0 Shift(Ψ , δ -t).
Base case: In such a case, we have that K = K, and thus t = t, P = P, Φ = Φ, and Ψ = ∅. Let K 0 = (P 0 ; Φ 0 ; δ) where δ = max({Dist

T (a, b) | a, b ∈ A 0 } ∪ {t}).
We have that K 0 -→ T K 0 using the TIM rule. Note that item (i) is satisfied since by hypothesis in P , any guarded input is preceded by a reset. Regarding (ii), we have that t 0 = δ = t -t + δ since t = t. Since Φ 0 = Φ 0 , and Ψ = ∅, item (iii) is also satisfied.

Induction step:

In such a case, we have that K tr -→ T K a,α --→ T K with K = (P ; Φ ; t ) and Φ = Φ Ψ . By induction hypothesis, we know that there exists K 0 = (P 0 ; Φ 0 ; t 0 ) such that K 0 tr -→ T K 0 with:

1. {(P, a) | P a ∈ P } = {(P, a) | P a ∈ P 0 }; 2. {(w, a, u) | w a, --→ u ∈ Φ } = {(w, a, u) | w a, --→ u ∈ Φ 0 }.
We have also that:

(i) if P ta a ∈ P and P contains a guarded input that is not preceded by a reset then

P ta a ∈ P 0 ; (ii) t 0 = t -t + δ where δ = max({Dist T (a, b) | a, b ∈ A 0 } ∪ {t}); (iii) Φ 0 = Φ 0 Shift(Ψ , δ -t).
We have to establish that there exists K 0 = (P 0 ; Φ 0 ; t 0 ) that satisfies the five properties stated above and such that K 0 a,α --→ T K 0 . We consider the rule involved in K a,α --→ T K and we show that the same rule can be applied on K 0 , and allows one to get K 0 with the five properties stated above. Case TIM rule with δ 0 . In such a case, we have that K = (P ; Φ ; t + δ 0 ), and we apply the same rule with the delay δ 0 on K 0 . We obtain K 0 = (P 0 ; Φ 0 ; t 0 +δ 0 ), and we easily check that all the properties are satisfied.

Case OUT rule. In such a case, K = (P ; Φ {w a,t --→ u}; t ) (for some P , w, a, and u). We apply the same rule on K 0 , and obtain K 0 = (P 0 ; Φ 0 {w a,t 0 --→ u}; t 0 ) (for some P 0 ). We have that items 1 and 2 are clearly satisfied as well as item (i). Now, regarding item (ii), we have that t 0 = t 0 and t = t . Therefore, we conclude that t 0 = t -t + δ thanks to our induction hypothesis. Now, to establish that Φ 0 = Φ 0 Shift(Ψ , δ -t), relying on our iduction hypothesis, it only remains to show that t 0 = t + (δ -t) (this is item ii). Case LET and NEW rules. In such a case, K = (P ; Φ ; t ) (for some P ), and we apply that same rule on K 0 , and obtain K 0 = (P 0 ; Φ 0 ; t 0 ). We conclude easily (for each property) relying on our induction hypothesis. Case RST rule. In such a case, K = (P ; Φ ; t ) (for some P ), and we know that P = { reset.P t a a } ∪ Q , and P = { P 0 a } ∪ Q for some P, a, t a and Q . We apply the same rule on K 0 , and obtain K 0 = (P 0 ; Φ 0 ; t 0 ), and we know that P 0 = { reset.P t a 0 a } ∪ Q 0 , and P 0 = { P 0 a } ∪ Q 0 for some t a 0 and Q 0 . Relying on our induction hypothesis, we easily obtain the fact that items 1 and 2 are satisfied. Regarding item (i), we conclude using our induction hypothesis for processes in Q 0 , and the property is satisfied for P 0 a . Regarding items (ii) and (iii), since the global time and the frame have not evolved, we conclude relying on our induction hypothesis. Case IN rule. In such a case, K = (P ; Φ ; t ) (for some P ), and we apply the same rule on K 0 to get K 0 = (P 0 ; Φ 0 ; t 0 ). The difficult part is to show that the rule can indeed be applied on K 0 . By hypothesis, we know that K a,in (u) -----→ T K , and thus P = in (x).P t a a ∪Q for some x, a, t a and Q, and we know that there exists b ∈ A 0 and t b ∈ R + such that t b < t -Dist T (b, a) and:

-if b ∈ A 0 M 0 then u ∈ img( Φ t b b ); -if b ∈ M 0 then u = RΦ↓ for some recipe R such that for all w ∈ vars(R) there exists c ∈ A 0 such that w ∈ dom( Φ t b -Dist T (c,b) c ).
Moreover, in case is < t g for some t g , we know in addition that t a < t g .

We first assume that in (u) is a simple input (not a guarded one). We show that we can apply on K 0 the same rule using the same recipe R. The message will be sent by the same agent b ∈ A 0 . The time t b 0 at which the message is t b + (δ -t). Note that t b 0 ≥ t b since δ -t ≥ 0. We distinguish two cases:

-if b ∈ A 0 M 0 then we know that u ∈ img( Φ t b b ) = img( Φ t b b ) ∪ img( Ψ t b b ). Actually, we have that img( Φ t b b ) ⊆ img( Φ 0 t b 0 b ) since t b 0 ≥ 0 and by definition Φ 0 = {w a,0 --→ u | w a,
--→ u ∈ Φ}. We have also that ). To conclude, it is sufficient to show that w ∈ dom( Φ 0

img( Ψ t b b ) ⊆ img( Ψ 0 t b 0 b ) since Ψ 0 = Shift(Ψ , δ -t),
t b 0 -Dist T (c,b) c
). Again, we distinguish two cases. In case w ∈ dom( Φ

t b -Dist T (c,b) c ), then w ∈ dom( Φ 0 t b 0 -Dist T (c,b) c ) since t b 0 ≥ 0 and by definition Φ 0 = {w a,0 --→ u | w a, --→ u ∈ Φ}. In case w ∈ dom( Ψ t b -Dist T (c,b) c
), then w ∈ dom( Ψ 0

t b 0 -Dist T (c,b) c
) since

Ψ 0 = Shift(Ψ , δ -t), and t b 0 = t b + (δ -t).
In case is < t g , by hypothesis we know that t a < t g , and thanks to item (i), we know that P 0 = in (x).P t a a ∪ Q 0 . This allows us to conclude.

B Proof of Theorem 1 (Distance Fraud)

We show this result in two main steps:

1. We move the agents (keeping p 0 far away from v 0 ) in a way that will only shorten the distance between any two of them. 2. We rename agents preserving their location (Lemma 1), and we show that the resulting initial configuration is still a valid one.

Lemma 1. Let K = (P; Φ; t) be a configuration on T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) and ρ : A → A 0 be a renaming such that Loc 0 (ρ(a)) = Loc 0 (a) for any a ∈ A 0 , and if a ∈ M 0 then ρ(a) ∈ M 0 . Let K = (P ; Φ ; t ) be a configuration such that K tr -→ T K . We have that:

Kρ trρ --→ T K ρ
Proof. We show this result by induction on the length of K tr -→ T K . The base case, i.e. tr is the empty trace, is trivial. To conclude, it is sufficient to show that K 1 a,α --→ T K 2 with K 1 a configuration built on T implies that: K 2 is a configuration built on T , and

K 1 ρ ρ(a),ρ(α) ------→ T K 2 ρ.
K 1 only involves processes located at a ∈ A 0 , and therefore actions along the derivation are only executed by agents in A 0 whose locations remain unchanged by ρ. We consider each rule of the semantics one by one. The only rules that are not trivial are the rules LET and IN.

Case of the rule LET. In such a case, we have that K 1 = (P 1 ; Φ 1 ; t 1 ) and K 2 = (P 2 ; Φ 2 ; t 2 ) with P 1 = let x = u in P ta a P, P 2 = P {x → u↓} ta a P, Φ 2 = Φ 1 , and t 2 = t 1 . We know that u↓ ∈ T (Σ + c , N A), and therefore we have that (uρ)↓ ∈ T (Σ + c , N A) by applying the same rewriting rule at each step. This allows us to apply the rule LET and to obtain the expected result.

Case of the rule IN.

In such a case, we have that K 1 = (P 1 ; Φ 1 ; t 1 ) and K 2 = (P 2 ; Φ 2 ; t 2 ) with P 1 = in (x).P ta a P, P 2 = P {x → u} ta a P, Φ 2 = Φ 1 , and t 2 = t 1 . We know that there exists b ∈ A 0 , t b ∈ R + such that t b ≤ t 1 -Dist T (b, a), and a recipe R such that u = RΦ 1 ↓, and for all w ∈ vars(R) there exists c ∈ A 0 such that w ∈ dom( Φ 1

t b -Dist T (c,b) c
). Moreover, when b ∈ A 0 M 0 , we know that R ∈ W. To conclude that the rule IN can be applied, we simply have to show that R(Φρ)↓ = uρ. Note that the renaming ρ keeps the locations of the agents in A 0 unchanged, and therefore the conditions about distance are still satisfied. We have that R(Φρ)↓ = (RΦ)ρ↓ since R ∈ T (Σ + pub , W). We know that (RΦ)↓ = u, and therefore we have that (RΦ)ρ↓ = uρ by applying the same rewriting rule at each step. Note that uρ does not contain any destructor symbol and is thus in normal form. To conclude, it remains to ensure that when ρ(b) ∈ A 0 M 0 , then R ∈ W. Actually, we know that if ρ(b) ∈ M 0 then b ∈ M 0 by hypothesis, and this allows us to conclude.

Theorem 1. Let P prox be a protocol, V 0 (z 0 , z 1 ) be a parametrised role containing the special event end(z 0 , z 1 ), and I 0 be a template. We have that P prox admits a distance fraud attack w.r.t. t 0 -proximity, if and only if, there is an attack against t 0 -proximity in the topology T t0 DF .

Proof. Since T 0 DF ∈ C DF , one direction is trivial. We consider the other one. Let T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) ∈ C DF and K 0 = (P 0 ; Φ 0 ; t init ) be a valid initial configuration for the protocol P prox and V 0 w.r.t. T and I 0 . We have that:

K 0 - → * T ( end(v 0 , p 0 ) tv v0 P; Φ; t) with Dist T (v 0 , p 0 ) ≥ t 0
We consider T = (A 0 , M 0 , Loc , v 0 , p 0 ) such that Loc (v 0 ) = Loc 0 (v 0 ), and:

Loc (a) = Loc (b) for any a, b ∈ A 0 {v 0 } with Dist T (v 0 , p 0 ) = t 0 .
Note that, since Dist T (v 0 , a) ≥ t 0 for any a ∈ A 0 {v 0 , p 0 } by definition of T ∈ C DF , we have that Dist T (a, b) ≤ Dist T (a, b) for any a, b ∈ A 0 . Thus:

K 0 - → * T ( end(v 0 , p 0 ) tv v0 P; Φ; t) with Dist T (v 0 , p 0 ) ≥ t 0
Then, we consider the renaming ρ : A → A 0 such that ρ(v 0 ) = v 0 , and ρ(a) = p 0 otherwise. We have that Loc (ρ(a)) = Loc (a) for any a ∈ A 0 , and in case a ∈ M 0 , we know that a = v 0 , and thus we have that ρ(a) = p 0 ∈ M 0 (since T ∈ C DF ). Thus, we can apply Lemma 1, we obtain that:

K 0 ρ - → * T ( end(v 0 , p 0 ) tv v0
Pρ; Φρ; t) with Dist T (v 0 , p 0 ) ≥ t 0 .

Since T and T 0 DF coincide on img(ρ) = {p 0 , v 0 }, we have that:

K 0 ρ - → * T 0 DF ( end(v, p) tv v Pρ; Φρ; t) with Dist T 0 DF (v 0 , p 0 ) ≥ t 0 .
To conlude, it remains to show that K 0 ρ is a valid initial configuration for P prox , and V 0 w.r.t. T 0 DF and I 0 . We have to prove that img( Φρ t init v0 ) = ∅, and img( Φρ

t init p0 ) = 29
Knows(I 0 , p 0 , {v 0 , p 0 }). We have that:

img( Φ 0 ρ t init p0 ) = {a∈A0 | ρ(a)=p0} (img( Φ 0 t init a )ρ = {a∈A0 | ρ(a)=p0} Knows(I 0 , a, A 0 )ρ = {a∈A0 | ρ(a)=p0} Knows(I 0 , ρ(a), ρ(A 0 )) = {a∈A0 | ρ(a)=p0} Knows(I 0 , p 0 , {p 0 , v 0 }) Moreover, we have that img( Φ 0 ρ t init v0 ) = img( Φ 0 t init v0 )ρ = ∅.
This allows us to conclude.

C Proof of Theorem 2 (Mafia Fraud)

We show this result in three main steps:

1. We reduce the number of active agents and show that it is sufficient to keep only 2 active agents, namely v 0 and p 0 . More precisely we first transform honest agents into dishonest ones (Lemma 2). Then, relying on our executability hypothesis, we discard processes executed by malicious agents (Proposition 5). 2. We control the number of attackers by placing them ideally, i.e. right next each active agent (Proposition 6). 3. We rename agents preserving their location (Lemma 1), and we show that the resulting initial configuration is still a valid one.

Reducing the number of active agents.

Lemma 2. Let T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) be a topology, and K 0 be a configuration built on T . Let H 0 ⊆ A 0 M 0 . Let K be a configuration such that K 0 tr -→ T K. We have that K 0 tr -→ T K where T = (A 0 , M 0 ∪ H 0 , Loc 0 , v 0 , p 0 ).

Proof. We show this result by induction on the length of the derivation K 0 tr -→ T K. The base case, i.e. tr is the empty trace, is trivial. To conclude, it is sufficient to show that:

K 1 a,α --→ T K 2 implies K 1 a,α --→ T K 2 .
Let K 1 = (P 1 ; Φ 1 , t 1 ). We consider each rule of the semantics one by one. Actually, the only rule that depends on the status (honest/dishonest) of the agents of the underlying topology is the rule IN. In such a case, we have that α = in (u) for some u. Moreover, following the notation introduced in Section 3.3, we know that there exist b ∈ A 0 (the agent responsible of the corresponding output) and t b ∈ R + (the time at which the output has been triggered). The only interesting case is when b ∈ H 0 , and therefore b is now a malicious agent in the topology T whereas b was an honest one in the topology T . Since, the IN rule was triggered in T , we know that u ∈ img( Φ 1 Definition 8. A closed process P without new construction is executable w.r.t. a frame Φ if for any term u (resp. v) occurring in an output or a let there exists a term R ∈ T (Σ + pub , dom(Φ) ∪ X ) such that u = RΦ↓ (resp. v↓ = RΦ↓).

Proposition 5. Let T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) be a topology, K 0 = (P 0 ; Φ 0 ; t 0 ) be a configuration built on T , and D 0 ⊆ M 0 . We assume that for any P a ta a ∈ P 0 with a ∈ D 0 , we have that P a is executable w.r.t. Φ 0 t0 a . Let K be a configuration such that K 0 tr -→ T K = (P; Φ 0 Φ + ; t). We have that (P 0 ; Φ 0 , t 0 ) tr -→ T (P; Φ 0 Φ + ; t) where P 0 (resp. P, Φ + , tr) is obtained from P 0 (resp. P, Φ + , tr) by removing processes (resp. frame or trace elements) located in a ∈ D 0 .

Proof. We will show this result assuming that D 0 contains a unique element a 0 . The general result can then easily be obtained by a simple induction on the size of D 0 . More precisely, we show the following results by induction on the length of K 0 tr -→ T K = (P; Φ 0 Φ + ; t):

1. for all P ta a0 ∈ P, P is executable w.r.t. Ψ (t); 2. for all w a0,ta ---→ u ∈ Φ + , there exists R ∈ T (Σ + pub , dom(Ψ (t a ))) such that RΨ (t a )↓ = u;

(P

0 ; Φ 0 , t 0 ) tr -→ T (P; Φ 0 Φ + ; t); where Ψ (t) = Φ 0 { Φ + t-Dist T (b,a0) b | b = a 0 }.
The base case, i.e. when tr is empty, is trivial. Now, we assume that K 0 tr -→ T K = (P; Φ 0 Φ + ; t) a,α --→ K = (P ; Φ 0 Φ ; t ) and thanks to our induction hypothesis, we know that the three properties above hold on K. We do a case analysis on the rule involved in the last step. Rule TIM. In such a case, we have that Φ = Φ + and P = P. Since t ≥ t, we have that Ψ (t) ⊆ Ψ (t ), and this allows us to conclude. Rule OUT. Items 1 and 3 are quite obvious. Regarding item 2, the only non trivial case is when a = a 0 . We have to show that the element added to the frame, namely w a0,t --→ u satisfies the expected property. By hypothesis, we know that the process out(u).P responsible of this output is executable w.r.t. Ψ (t), and thus there exists R ∈ T (Σ + pub , dom(Ψ (t))) such that RΨ (t)↓ = u↓. Rule LET. The only non trivial point is to establish item 1 when a = a 0 . We have that P = let x = v in P ta a0 P 1 , P = P {x → v↓} ta a0 P 1 , Φ = Φ + , and t = t. By hypothesis, we know that the process let x = v in P in P is executable w.r.t. Ψ (t), thus there exists R ∈ T (Σ + pub , dom(Ψ (t))) such that RΨ (t)↓ = v↓. To prove item 1, we have to show that P {x → v↓} is executable w.r.t. Ψ (t ) = Ψ (t). Let u be a term occurring in an output (resp. a let) in P {x → v↓}. We have that there exists u 0 that occurs in an ouput (resp. a let) in P such that u 0 {x → v↓} = u, and by hypothesis, we know that let x = v in P is executable w.r.t. Ψ (t), i.e. there exists

R 0 ∈ T (Σ + pub , dom(Ψ (t)) ∪ X ) such that u 0 ↓ = R 0 Ψ (t)↓. Let R = R 0 {x → R}. We have that R Ψ (t )↓ = (R 0 {x → R})Ψ (t)↓ = (R 0 Ψ (t){x → v↓})↓ = (u 0 {x → v↓})↓ = u↓.
Note that u = u 0 {x → v↓} is in normal form when u 0 is is normal form. Thus, no normalisation is needed in case u is a term occurring in an output.

Rule NEW. We know that a = a 0 , and thus the result trivially holds.

Rule RST. In such a case, the result trivially holds.

Rule IN.

In case a = a 0 , the only non trivial point is to establish item 1, and this can be done in a similar way as it was done in Rule LET. Otherwise, i.e. when a = a 0 , the non trivial point is to establish item 3. Let α = in (u). We have to establish that the IN rule can still be fired with the same value u despite the fact that some frame elements have been removed from Φ + . Following the notations introduced in Section 3.3, we know that there exist b ∈ A 0 and t b ∈ R + such that t b ≤ t -Dist T (b, a) and a recipe R such that R(Φ 0 Φ + )↓ = u and for all w ∈ vars(R) there exists c

∈ A 0 such that w ∈ dom( Φ 0 Φ + t b -Dist T (c,b) c ).

If b /

∈ M 0 then we know that R = w and we have that

Φ 0 Φ + t b b = Φ 0 Φ + t b
b because b = a 0 . Thus, the rule can be applied. 2. If b ∈ M 0 , then in case c = a 0 , or c = a 0 with w ∈ Φ 0 , then it is straightforward. The interesting case is when w ∈ dom(

Φ + t b -Dist T (a0,b) a0
), and we have to reconstruct wΦ + with elements available in Φ 0 Φ + . To do so, we apply item 2: we obtain that there exists a time t a ≤ t b -Dist T (a 0 , b) and a recipe R w ∈ T (Σ pub , dom(Ψ (t a ))) such that R w Ψ (t a )↓ = wΦ + . By definition of Ψ (t a ), we have that

Ψ (t a ) = Φ 0 { Φ + ta-Dist T (c,a0) c | c = a 0 }. Moreover, we know that t a -Dist T (c, a 0 ) ≤ t b -(Dist T (c, a 0 ) + Dist T (a 0 , b)) ≤ t b -Dist T (c, b). Thus, we have that vars(R w ) ⊆ dom(Φ 0 ) dom({ Φ + t b -Dist T (c,b) c | c = a 0 }.
We consider the substitution σ with dom(σ) = dom( Φ + t b -Dist T (a0,b)

a0

) and such that σ(w) = R w . We have that Rσ ∈ T (Σ + pub , dom(Φ 0 Φ + )) and

Rσ(Φ 0 Φ + )↓ = R(Φ 0 {w → R w (Φ 0 Φ + ) | w ∈ dom(σ)})↓ = R(Φ 0 {w → wΦ + | w ∈ dom(σ)})↓ = R(Φ 0 Φ + )↓ = u.
Therefore the IN rule can be applied.

In order to be able to apply Proposition 5, we will have to clean the process by removing new instructions, and applying a suitable renaming. Lemma 3. Let K = (P; Φ; t) be a configuration built on T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ), and D ⊆ A 0 . Let K = (P ; Φ ; t ) be a configuration such that K tr -→ T K , and N be the set of names that have been freshly generated to trigger all the rules NEW executed by agents in D. We have that:

( P; Φ; t) trρ --→ T ( P ρ; Φ ρ; t )
where ρ replaces any name from N with c 0 ∈ Σ 0 , and P is the process obtained from P by removing "new" instructions of the form new n and replacing the occurrence of n by c 0 in any process located in a ∈ D.

Proof. We show this result by induction on the length of K tr -→ T K . The base case, i.e. when tr is the empty trace, is trivial. To conclude, it is sufficient to show that (P 1 ; Φ 1 ; t 1 ) a,α --→ T (P 2 ; Φ 2 ; t 2 ) implies that:

1. either ( P1 ρ; Φ 1 ρ; t 1 ) = ( P2 ρ; Φ 2 ρ; t 2 ); 2. or ( P1 ρ; Φ 1 ρ; t 1 ) a,αρ ---→ T ( P2 ρ; Φ 2 ρ; t 2 )
Note that since ρ has no effect on the initial configuration K, this will allow us to conclude. We consider each rule of the semantics one by one.

-Rule TIM: In such a case, the same rule applies.

-Rule OUT: In such a case, we have that P 1 = out(u).P ta a P 0 and u↓ will be added into the frame. Actually the same rule applies on the configuration ( P1 ρ; Φ 1 ρ; t 1 ) and uρ↓ = u↓ρ will be added into the frame.

-Rule LET: In such a case, we have that P 1 = let x = u in P ta a P 0 and u↓ is a message. Actually the same rule applies on the configuration ( P1 ρ; Φ 1 ρ; t 1 ) since uρ↓ = u↓ρ is also a message.

-Rule NEW: In case a ∈ D, since the freshly generated name n will be in N, we have that ( P1 ρ; Φ 1 ρ; t 1 ) = ( P2 ρ; Φ 2 ρ; t 2 ). Otherwise, the same rule applies. -Rule RST: The same rule applies.

-Rule IN: In such a case, we have that P 1 = in(x).P ta a P 0 , and we have a recipe R such that RΦ 1 ↓ = u together with some extra conditions. The same rule applies using the same recipe R. We have that R(Φ 1 ρ)↓ = uρ. This allows us to conclude.

Controlling the number of intuders.

Given a mapping Loc from a set of agents A 0 = {a 1 , . . . , a p } to R 3 , we define the canonical topology T Loc associated to Loc as (A 0 M 0 , M 0 , Loc Loc 0 , v 0 , p 0 ) where:

-M 0 = {i 1 , . . . , i p } where i 1 , . . . , i p ∈ A A 0 ; -Loc 0 (i j ) = Loc(a j ) for j ∈ {1, . . . , p}. Proposition 6. Let T = (A 0 , M 0 , Loc 0 , v o , p 0 ) be a topology, K 0 = (P 0 ; Φ 0 ; t 0 ) be a configuration built on T 0 , and V be a set of agents such that:

{a | P t a ∈ P 0 or Φ 0 t a = ∅} ⊆ V ⊆ A 0 .
Let K = (P; Φ; t) be a configuration such that K 0 tr -→ T K. We have that (P 0 ; Φ 0 ; t 0 ) tr -→ T Loc V (P; Φ; t) where Loc V = Loc 0|V .

Proof. We show this result by induction on the length of the derivation K 0 tr -→ T K. The base case, i.e. tr is the empty trace, is trivial. To conclude, it is sufficient to show that:

K 1 a,α --→ T K 2 implies K 1 a,α --→ T K 2 where T = (A , M , Loc , v 0 , p 0 ) = T Loc V .
We consider each rule of the semantics one by one. Actually, the only rule that depends on the underlying topology is the rule IN. In such a case, we have that α = in (u) for some u. Moreover, we denote K 1 = (P 1 ; Φ 1 ; t 1 ) and following the notations introduced in Section 3.3, we know that there exist b ∈ A 0 (the agent responsible of the corresponding output) and t b ≤ t 1 -Dist T (b, a) (the time at which the output has been triggered) that satisfy the conditions of the rule. We distinguish two cases:

1. In case b ∈ A 0 M 0 , then we know that there exists w ∈ img( Φ ). We show that the same rule applies using the same recipe R. However, the agent responsible of the output will be the agent i a such that Loc (i a ) = Loc (a) = Loc 0 (a) (note that a ∈ V ), and this output will be performed at time t 1 (instead of t b ). We have that

RΦ 1 ↓ = u. Now, let w ∈ vars(R). Let c ∈ A 0 such that w ∈ dom( Φ 1 t b -Dist T (c,b) c
). We have that c ∈ V . It remains to show that w ∈ dom( Φ 1 t1-Dist T (c,ia) c

). For this, it is actually sufficient to establish that t 1 -Dist T (c, i a ) ≥ t b -Dist T (c, b). We know that:

t 1 -Dist T (b, a) ≥ t b ⇒ t 1 -Dist T (b, a) -Dist T (c, b) ≥ t b -Dist T (c, b) ⇒ t 1 -(Dist T (b, a) + Dist T (c, b)) ≥ t b -Dist T (c, b) ⇒ t 1 -Dist T (c, a) ≥ t b -Dist T (c, b)
The last implication comes from the triangle inequality for the distance. Then, we obtain the expected result since Loc (i a ) = Loc (a), and

Dist T (c, a) = Dist T (c, a) since a, c ∈ V .
This concludes the proof.

We are now able to establish our main result regarding mafia fraud.

Theorem 2. Let I 0 be a template, P prox be a protocol I 0 -executable, and V 0 (z 0 , z 1 ) be a parametrised role containing the special event end(z 0 , z 1 ). We have that P prox admits a mafia fraud attack w.r.t. t 0 -proximity, if and only if, there is an attack against t 0 -proximity in the topology T t0 MF . Proof. Consider a topology T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) such that P prox admits an attack. Let K 0 = (P 0 ; Φ 0 ; t init ) be an initial configuration that is valid for P prox , V 0 w.r.t. T 0 and I 0 such that K 0 admits an attack w.r.t. t 0 -proximity in T 0 . We consider the execution witnessing this fact:

K 0 tr -→ T0 ( end(v 0 , p 0 ).P ta v0 P; Φ 0 ∪ Φ; t) with Dist T0 (v 0 , p 0 ) ≥ t 0 .
To establish this result, we combine the previous lemmas to show that there exists a corresponding trace of execution in T t0

MF . As already announced, the proof is performed in three steps, and the first step is done in two stages.

Step 1-a. Applying Lemma 2 with H = A 0 (M 0 ∪ {v 0 , p 0 }), we obtain a topology T 1 = (A 1 , M 1 , Loc 1 , v 0 , p 0 ) where A 1 = A 0 , M 1 = A 0 {v 0 , p 0 }, and Loc 1 = Loc 0 . We have that:

K 0 tr -→ T1 ( end(v 0 , p 0 ) ta v0 P; Φ 0 ∪ Φ; t) with Dist T1 (v 0 , p 0 ) = Dist T0 (v 0 , p 0 ) ≥ t 0 .
We now consider the configuration K + 0 = (P 0 ; Φ + 0 ; t init ) where we extend Φ 0 into Φ + 0 such that img( Φ + 0 t init a ) = Knows(I 0 , a, A 1 ) when a ∈ M 1 . Since we only increase the knowledge, we have that:

K + 0 tr -→ T1 ( end(v 0 , p 0 ) ta v0 P; Φ + 0 ∪ Φ; t)
with Dist T1 (v 0 , p 0 ) = Dist T0 (v 0 , p 0 ) ≥ t 0 .

Step 1-b. Since the configuration K 0 is valid, we know that for all P ta a0 ∈ P 0 , there exists a role Q ∈ P prox such that P = Qτ with τ = {z 0 → a 0 , . . . , z n → a n }, z 0 , . . . , z n ∈ Z, and a 0 , . . . , a n ∈ A 0 = A 1 . Moreover, we know that for any term u occurring in an output or a let construction in P , there exists a corresponding term u occurring in an output or a let construction in Q and such that u = u τ . Let I 0 = {v 1 , . . . , v k }, and σ = {w 1 → v 1 , . . . , w k → v k }. Since Q is I 0 -executable, there exists a term R ∈ T (Σ + pub , {w 1 , . . . , w k } ∪ N ∪ X ) such that u = Rσ↓. Thus, we know that u↓ = u τ ↓ = Rσ↓τ ↓ = Rστ ↓. Actually, we have that img(στ ) ⊆ Knows(I 0 , a 0 , A 1 ). Therefore, since Knows(I 0 , a 0 , A 1 ) ⊆ img( Φ + 0 t init a0 ), we have that there exists R ∈ T (Σ + pub , W ∪ N ∪ X ) such that u↓ = R Φ + 0 t init a0 ↓. Now, we can apply Lemma 3 with K + 0 = (P 0 ; Φ + 0 ; t init ) and D = M 1 and conclude that:

-( P0 ; Φ + 0 ; t init ) trρ2 --→ T1 ( end(v 0 , p 0 ) ta v0
Pρ 2 ; Φ + 0 ∪ Φρ 2 ; t) where P is the mutiset of extended processed obtained from P by removing new instructions of the form new n and replacing the occurrence of n by c 0 in processes located in a ∈ D = M 1 , and ρ 2 replaces any name that has been generated to trigger a rule NEW executed by an agent in D by c 0 .

any P ta a0 ∈ P0 with a 0 ∈ M 1 does not contain new construction and is executable w.r.t. Φ + 0 t init a0 because c 0 ∈ Σ 0 ⊆ Σ + pub and therefore R in which we replace any occcurrence of a name in N by c 0 is a recipe in T (Σ + pub , Φ + 0 t init a0 ∪ X ) that allows one to conclude.

We are now able to apply Proposition 5 with D 0 = M 1 and we have that:

(P 0 ; Φ + 0 ; t init ) trρ2 --→ T1 ( end(v 0 , p 0 ) ta v0 Pρ 2 ; Φ + 0 ∪Φρ 2 ; t) with Dist T1 (v 0 , p 0 ) ≥ t 0 .
where Pρ 2 (resp. Φρ 2 , trρ 2 ) is obtained from Pρ 2 (resp. Φρ 2 , trρ 2 ) by removing processes (frame elements, actions) located in a ∈ D 0 = M 1 . We may note that the transformation • has some effect on processes that are removed by the transformation • , and thus can easily be removed.

Step 2. We now consider Φ ++ 0 the same as Φ + 0 but frame elements located at a ∈ M 1 are moved to v 0 . Let δ 0 = M ax(Dist T1 (v 0 , a)) for any a ∈ M 1 . Clearly, we have that:

(P 0 ; Φ ++ 0 ; t init + δ 0 ) trρ2 --→ T1 ( end(v 0 , p 0 ) ta v0 Pρ 2 ; Φ ++ 0 ∪ Shift(Φρ 2 , δ 0 ); t + δ 0 )
with Dist T1 (v 0 , p 0 ) ≥ t 0 . Indeed, shifting by +δ 0 the initial configuration, all the messages moved from an agent a ∈ M 1 to v 0 can be used by a at the time t init of the initial frame. Then we can apply Proposition 6 on T 1 and (P 0 ; Φ ++ 0 ; t init + δ 0 ) with V = {v 0 , p 0 }. We deduce that (where T 1 = ({v 0 , p 0 , i P , i V }, {i P , i V }, Loc {v0,p0} )):

(P 0 ; Φ ++ 0 ; t init + δ 0 ) trρ2 --→ T 1 ( end(v 0 , p 0 ) ta v0 Pρ 2 ; Φ ++ 0 ∪ Shift(Φρ 2 , δ 0 ); t + δ 0 ) with Dist T 1 (v 0 , p 0 ) = Dist T1 (v 0 , p 0 ) ≥ t 0 .
Step 3. To reduce the size of the initial frame, now we apply Lemma 1 on K 0 = (P 0 ; Φ ++ 0 ; t init + δ 0 ) using ρ 3 : A → A 1 = {v 0 , p 0 , i P , i V } such that ρ 3 (a) = i V for any a ∈ A 1 . We have that:

(P 0 ρ 3 ; Φ ++ 0 ρ 3 ; t init + δ 0 ) trρ2ρ3 ----→ T 1 ( end(v 0 , p 0 ) ta v0 Pρ 2 ρ 3 ; Φ ++ 0 ρ 3 ∪ Shift(Φρ 2 ρ 3 , δ 0 ); t + δ 0 )
with Dist T 1 (v 0 , p 0 ) ≥ t 0 . Now, we show that (P 0 ρ 3 ; Φ ++ 0 ρ 3 ; t init + δ 0 ) is almost valid. Indeed to turn this configuration into a valid one, we simply have to move frame elements (those that we have added during Step 1-a and moved during Step 2) located in v 0 to i V . This will not change the underlying execution since both nodes are located at the exact same place. Then, we add some frame elements in i P , more precisely Knows(I 0 , i P , A 1 ). These additional elements will not alter the underlying execution.

We may note that P 0 ρ 3 satisfies the first item of Definition 2: since P 0 is valid, there exits t such that V 0 (v 0 , p 0 ) t v0 ∈ P 0 and by construction P 0 ρ 3 36 still contains V 0 (v 0 , p 0 ) t v0 . Moreover, for all P t a ∈ P 0 ρ 3 , by construction, we know that a ∈ {v 0 , p 0 } = A 1 \ M 1 . Finally, we have that there exists P t a ∈ P 0 such that P = P (a , a 1 , . . . , a n ) for P ∈ P prox and P = P ρ 3 = P (a , ρ 3 (a 1 ), . . . , ρ 3 (a n )) with ρ 3 (a 1 ), . . . , ρ 3 (a n ) ∈ A 1 .

To conclude, we have to shorten the distance between v 0 , i V and p 0 , i P . To do so, we consider a new topology T

= (A 1 , M 1 , Loc, v 0 , p 0 ) such that Loc(v 0 ) = Loc(i v ), Loc(p 0 ) = Loc(i p ) and Dist T (v 0 , p 0 ) = t 0 .

D Proof of Theorem 3 (Distance hijacking attack)

To establish this result, we will first show that we can transform any attack trace into an attack trace having a specific format. For this, we need to show that some actions can be swapped without breaking the underlying action, and thus preserving the fact that the trace is an attack.

We first introduce annotations in the semantics of our processes, in order to ease their analysis.

D.1 Annotations

We shall now define an annotated semantics whose transitions are equipped with more informative actions. The annotated actions will feature labels identifying which process in the multiset has performed the action (session identifier). This will allow us to identify which specific agent performed some action. We also put in the annotation the global time at which the action has been done. In case of an output, the annotation will indicate the name of the handle w that has been used to store the output in the frame. In case of an input, the annotation will indicate by a triple (b, t b , R) the name b of the agent responsible of the corresponding output, the time at which this output has been performed, as well as the recipe R used to build this output.

Formally, an action is either empty (for the TIM rule) or of the form a, α with α ∈ {τ, out(u), in (u)}, and thus an annotated action is:

empty for the TIM rule; -(a, α, s, t, w) when the underlying action a, α is of the form a, out(u). In such a case, s is the session identifier of the agent responsible of this action, t is the global time at which this output has been done, and w is the handle added in the frame. α,s,t,(b,t b ,R)) when the underlying action a, α is of the form a, in (u).

In such a case, s is the session identifier of the agent responsible of this action, t is the global time at which this input has been done, b is the agent responsible of the corresponding output, t b the time at which this output has been done (t b ≤ t), and R the recipe that has been used to forge this output. -(a, α, s, t, ∅) otherwise.

In the relaxed semantics, similar annotations can be added. Of course, in such a case, information about time is not relevant. Thus annotations are either of the form (a, α, s, w) (case of the output) or of the form (a, α, s, (b, R)) (case of the input), or (a, α, s, ∅) otherwise. Note that in the relaxed semantics, the TIM rule does not exist. Lemma 4. Let T be a topology, and K 0 L1 T • • • Ln T K n be an execution such that for all L i = (a i , α i , s i , r i ) we have that α i = in <t (x) for some t. Let K 0 be a configuration such that untimed(K 0 ) = K 0 . We have that there exists a configuration K n such that untimed(K n ) = K n , and

K 0 tr -→ T K n with tr = (a 1 , α 1 ) . . . (a n , α n ).
Proof. Let T = (A 0 , M 0 , Loc, v 0 , p 0 ) be a topology. This proof is quite straightforward and can be formally done by induction on the length of the execution. Before each application of the rule IN, we apply the TIM rule with a delay δ = max a,b∈A0 (Dist T (a, b)) to be sure that all the messages necessary to build the inputted term are available.

D.2 Permutations of independent actions

Definition 9. Given an execution K 0 and: either s i = s j (and thus a i = a j ), and in that case L j is sequentiallydependent of L i , denoted L j → s L i ; or α i = out(v), α j = in (u), and r i ∈ vars(r j ), and in that case

L1 T • • • Ln T K n with L i = (a i , α i , s i , r i ), L j = (a j , α j , s j , r j ), we say that L j is dependent of L i , denoted L j → L i , if i < j,
L j is data-dependent of L i , denoted L j → d L i .
We note L j → L i when L j is not dependent of L i , i.e. L j → s L i and L j → d L i .

Lemma 5. Given a topology T , and an execution K 0

L1 T K 1 L2 T K 2 such that L 2 → L 1 . We have that K 0 L2 T K i L1 T K 2 for some K i .
Proof. Let K 0 = (P 0 ; Φ 0 ), K 1 = (P 1 ; Φ 1 ), and K 2 = (P 2 ; Φ 2 ) be three un-

timed configurations such that K 0 L1 T K 1 L2 T K 2 with L 2 → L 1 . Let L 1 = (a 1 , α 1 , s 1 , r 1 ) and L 2 = (a 2 , α 2 , s 2 , r 2 )
. By hypothesis, we know that L 2 → L 1 , and thus we have that s 1 = s 2 . Therefore, we have that:

-P 0 = c 1 .P 1 a1 ∪ c 2 .P 2 a2 Q, -P 1 = P 1 a1 ∪ c 2 .P 2 a2 Q, -P 2 = P 1 a1 ∪ P 2 a2 Q where c 1 , c 2 ∈ {in (x), new n, out(u), reset, let x = v in }.
First, in case α 1 = out(v) and α 2 = in (u), we have that

Φ 2 = Φ 1 = Φ 0 {r 1 a1 -→ v} and since L 2 → d L 1 , we know that r 1 /
∈ vars(r 2 ). Therefore, we deduce that vars(r 2 ) ⊆ dom(Φ 0 ). Now, let K i = ( c 1 .P 1 a1

P 2 a2 Q; Φ 0 ). Relying on the fact that r 1 / ∈ vars(r 2 ) in case α 1 = out(v) and α 2 = in (u), it is easy to see that K 0 L2 T K i L1 T K 2 .
Corollary 1. We consider a topology T , an execution K 0

L1 T • • •
Ln T K n , and two sets I and J such that I = {i 1 , . . . , i p }, J = {j 1 , . . . , j q }, I J = {0, . . . , n}, i 1 < • • • < i p , and j 1 < • • • < j q . Moreover, we assume that L i → L j for any i ∈ I, and j ∈ J. In such a case, we have that:

K 0 Li 1 T • • • Li p T Lj 1 T • • • Lj q T K n Proof. Given a trace K 0 L1 • • •
Ln K n and the two ordered sets I and J, we can translate the trace as a two-letters (i and j) word, each transition either converted into i or j depending on the set in which its index belongs. We consider the lexicographical order induced by the fact that i < j, e.g. iijjii < ijijii.

Let us suppose that there exists a trace satisfying all the hypotheses but such that the result does not hold. We consider the minimal one in the sense of the lexicographical order of the corresponding 2-letters word. This trace is a word w of the form • • • ji • • • , and the portion of it corresponding to the pattern ji is:

K 0 Lj q K 1 Li p K 2
for some q and some p . Since L i p → L j q , we can use Lemma 5, and rewrite this trace as

K 0 Li p K i Lj q K 2 .
Inserting such a trace into the whole exection trace we had at the beginning, we obtain a trace whose corresponding word w is smaller than w (according to the lexicographical order), and this would lead to a contradiction.

D.3 Proof of Proposition 2

Given a configuration K, φ(K) denotes its second component. Proposition 7. Let T = (A 0 , M 0 , Loc, v 0 , p 0 ) be a topology, and consider an execution trace of the following form:

K 0 Lreset ---→ T tr1 --→ T K out Lout --→ T tr2 --→ T K in Lin --→ T K 1 where L reset = (v 0 , reset, s 0 , t reset , ∅), L out = (v 0 , out(v), s 0 , t out , w 0 ), and L in = (v 0 , in <tg (u), s 0 , t in , (b 0 , t 0 b , R 0 ))
, and these are the only actions executed with the session identifier s 0 .

Then, there exists an execution trace:

K 0 tr 0 T K reset L reset T tr 1 T K out L out T tr 2 T K in L in T tr 3 T K 1
where:

-K 0 (resp. K 1 ) is the untimed counterpart of K 0 (resp. K 1 ), i.e. K i = untimed(K i ) with i ∈ {0, 1}; -L reset , L out , and L in are the untimed counterpart of the annotations L reset , L out , and L in , i.e. L reset = (v 0 , reset, s 0 , ∅), L out = (v 0 , out(v), s 0 , w 0 ), and L in = (v 0 , in <tg (u), s 0 , (b 0 , R 0 )); for any L = (a, α, s, r) occurring in tr 1 .L out .tr 2 .L in , 2Dist T (v 0 , a) < t g .

Moreover, when α = in (u), we have that r = (b , R ) for some b and some R such that 2Dist T (v 0 , b ) < t g or vars(R ) ⊆ dom(φ(K reset )).

Proof. Let T = (A 0 , M 0 , Loc, v 0 , p 0 ) be a topology and

K 0 Lreset ---→ T tr1 --→ T K out Lout --→ T tr 2 < ---→ T K tr 2 ≥ ---→ T K in Lin --→ T K 1
be a trace as defined in the proposition such that tr 2 = tr 2 < tr 2 ≥ ; t < t out + t g /2 for any L = (a, α, s, t, r) occurring in tr 2 < , and t ≥ t out + t g /2 for any L = (a, α, s, t, r) occurring in tr 2 ≥ . By Definition of the relaxed semantics, we have that

K 0 L reset T tr1 T K out L out T tr 2 < T K tr 2 ≥ T K in L in T K 1
where K 0 (resp. K 1 ) is the untimed counterpart of K 0 (resp. K 1 ), L reset , L out , and L in are the untimed counterpart of the annotations L reset , L out , and L in and tr 1 (resp. tr 2 < , tr 2 ≥ ) is the untimed counterpart of tr 1 (resp. tr 2 < , tr 2 ≥ ). In the following, we consider:

tr = L reset .tr 1 .L out .tr 2 < .tr 2 ≥ .L in the timed trace, and tr = L reset .tr 1 .L out .tr 2 < .tr 2 ≥ .L in its untimed counterpart.

Finally, we define Close(v 0 ) = {a ∈ A 0 | 2Dist T (v 0 , a) < t g }.

In order to obtain an execution trace in the relaxed semantics that satisfies all the requirements, we proceed in two main steps. We first show that we can push the actions from tr 2 < that do not satisfy the requirements before L reset , and then we will establish that we can push those from tr 2 ≥ after L in .

Step 1: cleaning of tr 2 < . Let S 1 a be the set of actions in tr such that their corresponding timed action in tr is executed by agents a / ∈ Close(v 0 ) and before t out + t g /2. Formally, we have that:

S 1 a = {(a, α, s, r) ∈ tr | a / ∈ Close(v 0
) and (a, α, s, t, r ) ∈ tr and t < t out + t g /2}.

We also define S 2 a the set of actions in tr such that their corresponding timed action in tr is an input for which the inputted message has been forged by an agent b / ∈ Close(v 0 ) at a time t b < t out + t g /2. Formally, we have that:

S 2 a = (a, in (u), s, r) ∈ tr L = (a, in (u), s, t, (b, t b , R)) ∈ tr b / ∈ Close(v 0 ), t b < t out + t g /2.
Then, we build BD(S 1 a , S 2 a ) as follows:

1. S := S 1 a . 2. For each γ ∈ S 2 a , for all transition β in tr, if γ → d β, then S := S ∪ {β}. 3. For each γ ∈ S, for all transition β in tr if γ → β, then S := S ∪ {β}. 4. BD(S 1 a , S 2 a ) := S.

We may note that at step 3, a fix point will be reached since we are working on a finite trace tr. We may also note that BD(S 1 a , S 2 a ) only contains actions from tr 2 < . Indeed, let

L 1 = (a 1 , α 1 , s 1 , t 1 , (b 1 , t 1 b , R 1
)) be such that its untimed counterpart L 1 belongs to S 2 a . Let us consider L 2 = (a 2 , α 2 , s 2 , t 2 , w 2 ) such that its untimed counterpart L 2 satisfies L 1 → d L 2 then we can deduce that

t 2 ≤ t 1 b -Dist T (a 2 , b 1 ) ≤ t 1 b < t out + t g /2.
Therefore, we can deduce that for all action L ∈ BD(S 1 a , S 2 a ), and this allows us to conclude.

Let BD(S 1 a , S 2 a ) be the set of transitions β such that β / ∈ BD(S a ) and β ∈ L reset .tr 1 .L out .tr 2 < .

1. For all α ∈ BD(S 1 a , S 2 a ) and β ∈ BD(S 1 a , S 2 a ), we have that α → β.

Proof. By construction of BD(S 1 a , S 2 a ).

Claim. 2. We have that L reset ∈ BD(S 1 a , S 2 a ).

Proof. If L reset ∈ BD(S 1 a , S 2 a ), then we must have that L out ∈ BD(S 1 a , S 2 a ). Therefore, there exists a sequence of actions such that

L 1 → • • • → L n → L out with L 1 ∈ S 1
a ∪ S 2 a . For i ∈ {1, . . . , n}, we note a i the name of the agent executing L i and t i the time at which the timed counterpart of this action occurs in tr. We distinguish two cases:

-L 1 ∈ S 1
a . We have that:

t 1 -t out ≥ Dist T (v 0 , a n ) + n-1 i=1 Dist T (a i , a i+1 ) ≥ Dist T (v 0 , a 1 ) ≥ t g /2
since we know that a 1 / ∈ Close(v 0 ) by Definition of S 1 a . We also have that t 1 < t out + t g /2 by Definition of S 1 a , and thus t 1 -t out < tg/2, yielding to a contradiction.

-

L 1 = (a 1 , in (u), s 1 , (b 1 , R 1 )) ∈ S 2 a . Let L 1 = (a 1 , in (u), s 1 , t 1 , (b 1 , t 1 b , R 1
)) its counterpart action in tr. By construction, we have that L 1 → d L 2 . According to the semantics of the rule IN, we have that t 1 b ≥ t 2 + Dist T (a 2 , b 1 ). We also know that t 2 -t out ≥ Dist T (v 0 , a 2 ). Thus we have t

1 b -t out ≥ Dist T (v 0 , a 2 ) + Dist T (a 2 , b 1 ) ≥ Dist T (v 0 , b 1
K 0 tr0 T K reset L reset T tr1 T K out L out T tr 2 < T K tr 2 ≥ T K in L in T K 1
Step 2: cleaning of tr 2 ≥ . We proceed in a similar way to clean the other part of the trace. Let S 1 b be the set of actions in the relaxed trace tr such that their corresponding action in the initial trace is executed by agents who are not in Close(v 0 ) between L reset and L in and after t out + t g /2. Formally, we have that:

S 1 b = {(a, α, s, r) ∈ tr | a / ∈ Close(v 0
) and (a, α, s, t, r ) ∈ tr and t ≥ t out + t g /2}.

We also define S 2 b the set of actions in tr such that their corresponding timed action in tr is an input in which the inputted message has been forged by an agent b / ∈ Close(v 0 ) at a time t b ≥ t out + t g /2. Formally, we have that:

S 2 b = (a, in (u), s, r) ∈ tr L = (a, in (u), s, t, (b, t b , R)) ∈ tr b / ∈ Close(v 0 ), t b ≥ t out + t g /2.
Let Proof. If L in ∈ FD(S b ), then there exists a sequence of actions

L in → L 1 → • • • → L n with L n ∈ S b .
For i ∈ {1, . . . , n}, we not a i the name of the agent executing L i and t i the time at which this action occurs in tr. We distinguish two cases:

-L n ∈ S 1
b . In such a case, we have that

t in -t n ≥ Dist T (v 0 , a 1 ) + n-1 i=1 Dist T (a i , a i+1 ) ≥ Dist T (v 0 , a n ) ≥ t g /2
since we know that a n / ∈ Close(v 0 ). By definition of S 1 b , we know that t n ≥ t out + t g /2. Thus, we have that t in ≥ t out + t g . However, the semantics gives us t in -t out < t g yielding a contradiction.

-L n = (a n , in (u), s n , (b n , R n )) ∈ S 2 b . Let L n = (a n , in (u), s n , t n , (b n , t n b , R n )) its counterpart action in tr. We have that t in -t n ≥ Dist T (v 0 , a 1 ) + n-1 i=1 Dist T (a i , a i+1 ) ≥ Dist T (v 0 , a n ).
We also have that t n ≥ t n b + Dist T (b n , a n ) ≥ t out + t g /2 + Dist T (b n , a n ). Therefore, we have that:

t in ≥ t out + t g /2 + Dist T (b n , a n ) + Dist T (v 0 , a n ) ≥ t out + t g /2 + Dist T (v 0 , b n ). Since b n / ∈ Close(v 0 ), we know that Dist T (v 0 , b n ) ≥ t g /2.
Thus, we have that t in ≥ t out + t g . This yields to a contradiction since the semantics gives us t in -t out < t g . This allows us to conclude the proof of this claim.

With Claim 3 and Claim 4, we can apply Corollary 1 on the trace tr, and thus, we can move all transitions in FD(S b ) right after L in leading us to a partially cleaned trace:

K 0 L reset T tr1 T K out L out T tr 2 < T K tr 2 ≥ T K in L in T tr3 K 1
Therefore, we have that:

K 0 tr0 T K reset L reset T tr1 T K out L out T tr 2 < T K tr 2 ≥ T K in L in T tr3 T K 1 .
To conclude, it remains to check that for any L = (a, in (u), s, r) occurring in tr 1 .L out . tr 2 < . tr 2 ≥ .L in , we have that r = (b , R ) for some b and some R such that 2Dist T (v 0 , b ) < t g or vars(R ) ⊆ dom(φ( K reset )).

Let us consider L = (a, in (u), s, t, (b , t b , R )) the timed counterpart of L, and assume that 2Dist T (v 0 , b ) ≥ t g . We distinguish two cases:

-Case t b < t out + t g /2. In such a case, we know that L ∈ S 2 a . For all w ∈ vars(R ), there exists L w ∈ tr such that L → d L w . Therefore, by construction, L w ∈ BD(S 1 a , S 2 a ), and this action has been moved before L reset . Thus, we have that vars(R ) ⊆ dom(φ(K reset )).

-Case t b ≥ t out + t g /2. In such a case, we know that L ∈ S 2 b ⊆ FD(S b ) and thus has been moved after L in . This concludes the proof. Proposition 2. Let K 0 be a valid initial configuration for P prox and V 0 w.r.t. a topology T = (A 0 , M 0 , Loc, v 0 , p 0 ) and I 0 . If K 0 tr -→ T K 1 then there exists an execution K 0 tr K 1 such that K i = untimed(K i ) for i ∈ {0, 1}.

Moreover, for any sub-execution of K 0 tr K 1 of the form ( reset.P v0 P; Φ reset ) v0,τ ( P v0 P; Φ reset )

tr 0 K - in v0,in <t (u)
K in where tr 0 only contains actions (a, α) with α ∈ {τ, out(u), in(u)}, we have that:

-2Dist T (v 0 , a) < t for any (a, α) ∈ tr 0 ; for any (a, in (v)) occurring in tr 0 .(v 0 , in <t (u)), the agent b responsible of the output and the recipe R (as defined in Figure 1) are such that either 2Dist T (v 0 , b) < t, or vars(R) ⊆ dom(Φ reset ).

Proof. Let K 0 be a valid initial configuration for P prox and V 0 w.r.t. a topology T = (A 0 , M 0 , Loc, v 0 , p 0 ) and I 0 . Let K 0 tr -→ K 1 be a trace. Because of the specific grammar generating V 0 we can decompose tr into several pieces of the form: L reset .tr 1 .L out .tr 2 .L in where L reset is a reset transition, L out the following output and L in the following guarded input. Therefore, we can apply Proposition 7 on each piece. Finally we can concatenate all these relaxed sub-traces to obtain a full trace as described in Proposition 2.

Theorem 3. Let I 0 be a template, P prox be a protocol, t 0 ∈ R + , and V 0 (z 0 , z 1 ) be a parametrised role obtained using the following grammar:

P, Q := end(z 0 , z 1 ) | in(x).P | let x = v in P | new n.P | out(u).P | reset.out(u ).in <t (x).P where x ∈ X , n ∈ N , u, u ∈ T (Σ + c , X ∪N ∪{z 0 , z 1 }), v ∈ T (Σ + , X ∪N ∪{z 0 , z 1
}) and t ≤ 2 × t 0 . If P prox admits a distance hijacking attack w.r.t. t 0 -proximity, then P prox admits an attack against t 0 -proximity in the topology T t0 DH .

Proof. Let T = (A 0 , M 0 , Loc, v 0 , p 0 ) ∈ C DH and K 0 = (P 0 ; Φ 0 ; t init ) be a valid initial configuration for the protocol P prox and V 0 w.r.t. T and I 0 . We have that:

K 0 tr -→ T ( end(v 0 , p 0 ) tv v0 ∪ P; Φ; t) = K 1 with Dist T (v 0 , p 0 ) ≥ t 0 .
Step 1: We first replace guarded inputs occurring in processes other than V 0 by simple inputs. Denoting K 0 (resp. K 1 , tr) the counterpart of K 0 (resp. K 1 and tr) in which guarded inputs have been replaced by simple inputs, we have that:

K 0 tr -→ T ( end(v 0 , p 0 ) tv v0 ∪ P; Φ; t) = K 1 with Dist T (v 0 , p 0 ) ≥ t 0 .
Indeed, all the required conditions to trigger a simple input will be satsified since a guarded input is like a simple input with a constraint regarding time. Moreoever, we have that K 0 is a valid initial configuration for P prox and V 0 w.r.t. T and I 0 .

Step

2: Let Close(v 0 ) = {a ∈ A 0 | Dist T (v 0 , a) < t 0 }. Applying Proposition 2,
we obtain a relaxed trace K 0 tr

T K 1 such that untimed(K i ) = K i for i ∈ {0, 1}.
Moreover, for any sub-execution K reset v0,τ tr 0 v0,in <t (u)

K in of K 0 tr K 1
starting with an application of the rule RESET and whose only guarded input is the one occurring at the end, we have that:

-2Dist T (v 0 , a) < t for any (a, α) ∈ tr 0 ;

for any (a, in (v)) occurring in tr 0 .(v 0 , in <t (u)), the agent b responsible of the output (as defined in Figure 4) is such that either 2Dist T (v 0 , b) < t, or vars(R) ⊆ dom(φ(K reset )).

Since t ≤ 2 × t 0 , we have that:

-Dist T (v 0 , a) < t 0 for any (a, α) ∈ tr 0 ; for any (a, in (v)) occurring in tr 0 .(v 0 , in <t (u)), the agent b responsible of the output (as defined in Figure 4) is such that either Dist T (v 0 , b) < t 0 , or vars(R) ⊆ dom(φ(K reset )).

Step 3: We consider the topology T = (A 0 , M 0 , Loc , v 0 , p 0 ) such that Loc (v 0 ) = Loc(v 0 ), Loc (p 0 ) is such that Dist T (v 0 , p 0 ) = t 0 and:

Loc (a) = Loc (v 0 ) if a ∈ Close(v 0 ) Loc (p 0 ) otherwise.
In this topology, the agents far away from v 0 are moved to p 0 , and agents in the neighborhood of v 0 are moved to v 0 . In this topology T , we only have two locations, and we have that K 0 tr T K 1 since the locations of the agents are no longer relevant in the relaxed semantics.

Step 4: We show that we can come back to a timed execution trace, i.e. one executable in the timed semantics by induction on the number of guarded inputs in the trace. Given a configuration K 0 such that untimed( K 0 ) = K 0 , we show that there exists a configuration K 1 such that untimed( K 1 ) = K 1 . To show this result, we split our execution trace K 0 tr T K 1 on several blocks of actions: a block is either a trace with no guarded input, or a sequence of actions starting with a reset and ending at the first occurrence of a guarded input. To lift such a block in the timed semantics, we either rely on Lemma 4, or on the properties established at Step 2.

To conclude this step, it only remains to show how to lift a block in the timed semantics. Let K reset v0,τ tr 0 v0,in <t (u)

K in be such a block, and let K be such that untimed( K) = K reset , and we denote t the global time of configuration K.

We have to show that there exists K in such that K (v0,τ ).tr 0 .(v0,in <t (u) -------------→ K in , and untimed( K in ) = K in . We start by applying the rule TIM with the delay δ equals to 2 × t 0 . Let K + be the resulting configuration.

Then we have to show that the sequence of actions L reset .tr 1 .L out .tr 2 .L in can be executed without introducing any delay. Moreover, we show that the resulting configuration K in is such that untimed( K in ) = K in . Actually, the correspondence between timed and untimed configurations is maintained along the trace.

The only difficult part is when the underlying action is an input. We know that this input is performed by a ∈ Close(v 0 ). Let in (u) be an input occurring in the block and let Φ the current frame in the relaxed semantics when this action occurs and Φ its corresponding frame in the timed trace. By definition of the relaxed semantics, we know that there exists a recipe R such that RΦ ↓ = u.

Thus, we know that R Φ↓ = u. To conclude, it remains to show that the timing constraints are satisfied. We distinguish two cases:

-The input has been forged by an agent b ∈ Close(v 0 ). Any w used in R is either in dom(φ(K reset )) or outputted after L reset by an agent located at the same place as v 0 . In both cases, since the global time has elapsed of 2t 0 between K and K + , we know that all these w will be available at time t + 2t 0 for b. Since a and b are located at the same place, we also have that this input can be done at time t + 2t 0 . -The input has been forged by an agent b ∈ Close(v 0 ). In such a case, we know that vars(R ) ⊆ dom(φ(K reset )), and thus thanks to the delay of 2t 0 that has been applied between K and K + , we know that the input can be received at time t + 2t 0 . Indeed, b can forge the message at time t + t 0 and thus it can be received at time t + 2t 0 .

Note that, regarding the guarded input, the guard is trivially satisfied since the global time remains unchanged since the reset action has been performed.

Step 5: To finish, we first reduce the topology to T t0 DH = (A DH , M DH , Loc DH , v 0 , p 0 ). Let us consider the renaming

ρ(a) =    v 0 if a ∈ Close(v 0 ) p 0 if a / ∈ Close(v 0 ) and a ∈ M 0 e 0 if a / ∈ Close(v 0 ) and a ∈ M 0 Since Loc DH (ρ(a)) = Loc (a)
for any a ∈ A 0 , and ρ(a) ∈ M DH if, and only if a ∈ M 0 , thanks to Lemma 1, we have that:

K 0 ρ tr0ρ --→ T t 0 DH K reset ρ Lresetρ; tr1ρ;Loutρ; tr2ρ;Linρ -----------------→ T t 0 DH K in ρ tr3ρ --→ T t 0 DH K 1 ρ.
To conclude, it remains to show that K 0 ρ is a valid initial configuration for P prox , and V 0 w.r.t. T t0 DH and I 0 . Denoting Φ 0 the frame of K 0 and t init the global time, we have to prove that img( Φ 0 ρ t init v0 ) = ∅, img( Φρ t init e0 ) = ∅ and img( Φρ t init p0 ) = Knows(I 0 , p 0 , {v 0 , p 0 , e 0 }). First, we have that img( Φ 0 ρ t init v0 ) = a∈Close(v0) img( Φ 0 t init a )ρ = ∅ since all these agents are honest.

Then we have that:

img( Φ 0 ρ t init e0 ) = {a∈A0 | ρ(a)=e0} img( Φ 0 t init a )ρ = {a∈A0 | ρ(a)=e0} ∅ = ∅
Finally we have that:

img( Φ 0 ρ t init p0 ) = {a∈A0 | ρ(a)=p0} img( Φ 0 t init a )ρ = {a∈A0 | ρ(a)=p0} Knows(I 0 , a, A 0 )ρ = {a∈A0 | ρ(a)=p0} Knows(I 0 , ρ(a), ρ(A 0 )) = {a∈A0 | ρ(a)=p0} Knows(I 0 , p 0 , {p 0 , v 0 , e 0 })
This allows us to conclude.

E Proof of Proposition 3

A process is said initial if it starts with an input action. Lemma 6. Let T = (A 0 , M 0 , Loc, v 0 , p 0 ) be a topology, and consider an execution trace of the following form:

K 0 tr0 --→ T K reset Lreset ---→ T tr1 --→ T K out Lout --→ T tr2 --→ T K in Lin --→ T K in + tr3 --→ T K 1
where L reset = (v 0 , reset, s 0 , t reset , ∅), L out = (v 0 , out(v), s 0 , t out , w 0 ), and L in = (v 0 , in <tg (u), s 0 , t in , (b 0 , t 0 b , R 0 )), and these are the only actions executed with the session identifier s 0 .

Then, there exists an execution trace:

K 0 tr 0 T K reset L reset T tr 1 T K out L out T tr 2 T K in L in T tr 3 T K 1
where:

1. K 0 (resp. K 1 ) is the untimed counterpart of K 0 (resp. K 1 ), i.e. K i = untimed(K i ) with i ∈ {0, 1}; 2. L reset , L out , and L in are the untimed counterpart of the annotations L reset , L out , and L in , i.e. L reset = (v 0 , reset, s 0 , ∅), L out = (v 0 , out(v), s 0 , w 0 ), and

L in = (v 0 , in <tg (u), s 0 , (b 0 , R 0 )); 3. for any L = (a, α, s, r) occurring in tr 1 .L out .tr 2 .L in , 2Dist T (v 0 , a) < t g .
Moreover, when α = in (u), we have that r = (b , R ) for some b and some R such that 2Dist T (v 0 , b ) < t g or vars(R ) ⊆ dom(φ(K reset )); 4. denoting K reset = (P reset , Φ reset ), if P a ∈ P reset with session identifier s i = s 0 , then P is an initial process or is left unchanged after K reset ; 5. denoting K in = (P in , Φ in ), if P a ∈ P in with session identifier s i = s 0 , then P is an initial process or is left unchanged after K in .

Proof. This proposition is an extension of Proposition 7. Indeed, applying Proposition 7 to the subtrace between K reset and K in + we obtain that there exists a trace satisfying items 2 and 3

K reset trreset T K reset L reset T tr1 T K out L out T tr2 T K in L in T trin T K in + such that K reset = untimed(K reset ) and K in + = untimed(K in + ). Let K 0 = untimed(K 0 ) and K 1 = untimed(K 1 )
. By definition of the relaxed semantics, we have K 0 tr0 T K reset and K in + tr3

T K 1 with tr 0 (resp. tr 3 ) the untimed counterpart of tr 0 (resp. tr 3 ). Let tr 0 = tr 0 . tr reset and tr 3 = tr in .tr 3 , we have that:

K 0 tr0 T K reset L reset T tr1 T K out L out T tr2 T K in L in T tr3 T K 1
Moreover, we know that items 1, 2, and 3 are satisfied.

Let tr = tr 0 .L reset . tr 1 .L out . tr 2 .L in . tr 3 . Let us prove item 4 and 5 in two steps: first we modify the trace tr into a trace tr satisfying items 1 to 4. Then we modify tr into a trace tr satisfying all the items (including item 5).

Step 1. In case, all the processes in K reset satisfy our requirement, we are done. Otherwise, there exists a process with session identifier s i (s i = s 0 ) which does not satisfy our requirement. Let K be the first configuration in the execution trace

K reset Lreset. tr1.L out . tr2.L in . tr3
T K 1 such that the process with session identifier s i is initial. If such a configuration does not exist, let K = K 1 . Then, we consider the following set S: S = {(a, α, s, r) ∈ tr before K | s = s i or (a, α, s, r) ∈ tr 0 }.

Let S be the set of transitions β such that β / ∈ S and β ∈ tr.

Claim. 1. For all L ∈ S and L ∈ S, we have that L → L .

Proof. We note L = (a, α, s, r) and L = (a , α , s , r ). By definition of S, we know that either L ∈ tr 0 , or s = s i and α = in (u). Otherwise, K is not the first configuration in which the process with session identifier s i is initial. In case, L ∈ tr 0 , then we know that L occurs before L in tr and thus L ∈ tr 0 , and thus in S, leading to a contradiction. In case, s = s i and thus α = in (u), then we have that L → L implies L → s L and thus L ∈ S, leading to a contradiction. This concludes the proof of the claim.

We now apply Corollary 1, and obtain a trace

K 0 tr 0 T K reset tr T K 1
such that the process with session identifier s i is initial in K reset or is left unchanged in the following of the trace.

We then apply the same construction on each process which does not satisfy our requirement in K reset . This construction leads to a trace tr which is:

K 0 tr0 T K reset L reset T tr1 T K out L out T tr2 T K in L in T tr3 T K 1
satisfying item 4. We can note that item 1, 2, and 3 are still satisfied. Indeed, we de not add any action between L reset and L in .

Step 2. We now need to turn the trace into one that also satisfies item 5. In case K in satisfies our requirement, we are done. Otherwise, there exists a process with session identifier s i (s i = s 0 ) which does not satisfy our requirement. First, we consider the case where the agent a i executing session s i is such that Dist T (a i , v 0 ) ≥ t g . Actually, such a case is not possible. Indeed, according to item 3, this would mean that K reset does not satisfy our requirement. Thus, we know that the agent a i executing session s i is such that Dist T (a i , v 0 ) < t g . In such a case, we proceed as in Step 1. Note that actions that will be added between L reset and L in are only outputs or τ actions executed by agents in the neighbourhood of v 0 , i.e. such that Dist T (a, v 0 ) < t g . Thus, item 3 is still satisfied.

Proposition 3. Let T = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) be a topology, P prox a protocol, t 0 ∈ R + , I 0 a template, and V 0 (z 0 , z 1 ) a parametrised process of the form: block 1 . reset . out(m) . in <t (x) . block 2 . end(z 0 , z 1 ) with t ≤ 2 × t 0 Let K 0 be a valid initial configuration for the protocol P prox and V 0 w.r.t. T and I 0 . If K 0 admits an attack w.r.t. t 0 -proximity in T , then we have that: F(T 0 , P prox , V 0 , I 0 , t 0 ) tr = ⇒ ({2 : end(v 0 , p 0 )} P; φ; 2). Moreover, in case there is no a ∈ M 0 such that Dist T0 (a, v 0 ) < t 0 , we have that for any in(u) occurring in tr during phase 1, the underlying recipe R is either of the form w, or only uses handles ouputted in phase 0.

Proof. Let T = (A 0 , M 0 , Loc, p 0 , v 0 ) be a topology, P prox a protocol, I 0 a template and V 0 a parametrised process of the right form. Let K 0 be a valid initial configuration for the protocol P prox and V 0 w.r.t. T and I 0 such that K 0 tr -→ T ({ end(v 0 , p 0 ) tv 0 v0 } P; Φ; t) = K 1 with Dist T (v 0 , p 0 ) ≥ t 0 .

Let K 0 the configuration obtained from K 0 by removing reset instructions, and replacing guarded inputs by simple inputs for processes other than V 0 . We have that K 0 is a valid initial configuration for P prox and V 0 w.r.t. T and I 0 . Moreover, the trace tr is still executable (up to some reset instructions) and leads to K 1 , i.e. K 1 in which reset instructions have been removed and guarded inputs have been replaced by simple inputs.

Therefore, we have that:

K 0 tr -→ T ({ end(v 0 , p 0 ) tv 0 v0 } P; Φ; t) = K 1 with Dist T (v 0 , p 0 ) ≥ t 0 .

Due to the specific form of V 0 we know that tr has the right form to apply Lemma 6. Thus, we know that there exists a trace tr such that:

K 0 tr 0 T K reset L reset T tr 1 T K out L out T tr 2 T K in L in T tr 3
T K 1 with:

1. K 0 (resp. K 1 ) is the untimed counterpart of K 0 (resp. K 1 ), i.e. K i = untimed(K i ) with i ∈ {0, 1}; 2. L reset , L out , and L in correspond to the reset.out(u).in <t (x) block occurring in V 0 ; 3. for any L = (a, α, s, r) occurring in tr 1 .L out .tr 2 .L in , 2Dist T (v 0 , a) < t. Moreover, when α = in (u), we have that r = (b , R ) for some b and some R such that 2Dist T (v 0 , b ) < t or vars(R ) ⊆ dom(φ(K reset ));

4. denoting K reset = (P reset , Φ reset ), if P a ∈ P reset with session identifier s i = s 0 , then P is an initial process or is left unchanged after K reset ; 5. denoting K in = (P in , Φ in ), if P a ∈ P in with session identifier s i = s 0 , then P is an initial process or is left unchanged after K in .

To conclude, it remains to show that such a trace tr can actually be mimicked from the configuration F(T , P prox , V 0 , I 0 , t 0 ). Actually, some τ actions (REP rule) have to be added, L reset is replaced by phase 1, and L in is followed by a phase 2 action.

Let P t a be a process occurring in K 0 , we know that P = R(a, a 1 , . . . , a n ) with R(z 0 , z 1 , . . . , z n ) a role of P prox . We know consider all the actions performed by this process along the trace tr , and in particular, we pay attention on the slicing of all these actions w.r.t. L reset and L in . This gives us the corresponding process that we have to consider in our translation, so that it will be able to mimic all the actions of P t a . Items 4 and 5 allow one to ensure that our slicing (just before the inputs) is indeed sufficient. Our transformation F ≥ also forbid actions to be executed during phase 1, and this is justified by our item 3.

Finally, it remains to establish that in case there is no a ∈ M 0 such that Dist T (a, v 0 ) < t 0 , we have that for any in(u) occurring in the trace during phase 1, the underlying recipe R is either of the form w, or only uses handles outputted in phase 0.

To establish this, we rely on item 3. We know that for any in(u) (with annotation (a, in (u), s, r)) occurring in the trace during phase 1, we have that r = (b , R ) for some b and some R such that 2Dist T (v 0 , b ) < t or R only uses handles outputted in phase 0. Since, by hypothesis, we know that there is no a ∈ M 0 such that Dist T (a, v 0 ) < t 0 , thus we know that there is no a ∈ M 0 such that 2Dist T (a, v 0 ) < 2t 0 , and thus there is no a ∈ M 0 such that 2Dist T (a, v 0 ) < t (since t ≤ 2×t 0 ). Thus, we deduce that either b is honest or R only uses handles outputted in phase 0, which implies that R is either of the form w, or only uses handles outputted in phase 0.

F Model with restricted agents

In this appendix we want to study how our previous results can be extend/modified to consider a restricted model in which an agent cannot play the role of a verifier and the role of a prover at the same time.

F.1 Model

In this model we split the set of agent names A into two subsets A p A v containing respectively the identity of the agents being able to execute a prover role and those of agents being able to execute a verifier role. Similarly, when considering a topology T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) we split A 0 (resp. M 0 ) into A p 0 A v 0 (resp. M p 0 M v 0 ) representing prover and verifier identities. Moreover, we enforce that p 0 ∈ A p 0 and v 0 ∈ A v 0 .

The definition of a configuration remains the same but we must precise the definition of a valid initial configuration.

First, because we consider provers and verifiers separately we have to consider two templates I p 0 and I v 0 that will be used to derive the initial knowledge of respectively a prover and a verifier. Definition 10. Let P prox = {P (z 0 , . . . , z k ), V (z 0 , . . . , z k )} be a protocol, V 0 (z 0 , z 1 ) be a parametrised role containing the special action end(z 0 , z 1 ), (I p 0 , I v 0 ) be templates, and T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) be a topology. A configuration K = (P; Φ; t) is a valid initial configuration for the protocol P prox and V 0 w.r.t. T 0 and (I p 0 , I v 0 ) if:

1. P = V 0 (v 0 , p 0 ) t v0

P for some t and for each P t a ∈ P if a ∈ A p 0 there exists a 1 , . . . , a k ∈ A 0 such that P = P (a , a 1 , . . . , a k ) else a ∈ A v 0 and there exists a 1 , . . . , a k ∈ A 0 such that P = V (a , a 1 , . . . , a k ) 2. img( Φ t a ) = Knows(I x 0 , a, A 0 ) when a ∈ M x 0 with x ∈ {p, v}, and img( Φ t a ) = ∅ otherwise.

When t = 0 and t = 0 for each P t a ∈ P and each {w a ,t ---→ u} ∈ Φ, we say that K is a zero-configuration.

The definition of an attack (Definition 5) can be immediately adapted replacing the template I 0 by (I p 0 , I v 0 ). Except this modification, everything remain the same.

We must do exactly the same modification for Proposition 1 (zero-attacks) and it stays correct. Indeed in Proposition 4 if K is a valid initial configuration in the new model it is immediate that K 0 is also a valid initial configuration (we just set all the clocks equal to zero; we do not modify the identity of an agent executing a process/role).

F.2 Reducing the topology

Preventing agents from playing a prover and a verifier role at the same time, we cannot obtain the same reduction results as presented in Section 5. We obtain similar reduced topologies in which we have duplicated almost all the agents in order to have one honest (resp. dishonest) prover representative and one honest (resp. dishonest) verifier representative at each location. The two topologies are presented in Figure 7 and explained in the corresponding subsections. MF in which the two dishonest identities i 1 and i 2 have been duplicated to represent dishonest provers and dishonest verifiers at each locations.

We keep the same definition of executability for a role (Definition 7). A protocol P = {P (z 0 , . . . , z k ), V (z 0 , . . . , z k )} is (I p 0 , I v 0 )-executable if P (z 0 , . . . , z k ) is I p 0 -executable and V (z 0 , . . . , z k ) is I v 0 -executable.

Theorem 4. Let (I p 0 , I v 0 ) be two templates, P prox be a protocol (I p 0 , I v 0 )-executable, and V 0 (z 0 , z 1 ) be a parametrised role containing the special event end(z 0 , z 1 ). We have that P prox admits a mafia fraud attack w.r.t. t 0 -proximity, if and only if, there is an attack against t 0 -proximity in the topology T t0 MFnew .

Proof. (Sketch) This proof is very similar to the one we did for Theorem 2.

In this restricted model, restrictions only concern the definition of valid initial configurations. It does not modify the semantic of the model. Therefore,

Fig. 1 :

 1 Fig. 1: Semantics of our calculus

Fig. 2 :

 2 Fig. 2: Distance hijacking attack on the Brands and Chaum's protocol

Fig. 3 :DH 5 . 1

 351 Fig. 3: Topologies T t 0 DF , T t 0 MF , and T t 0 DH

F

  (nV , nP , P ) P, nP , nV Mac k (P, nP , nV ) Meadows et al. nP , nV , k)

Fig. 5 :

 5 Fig. 5: Description of our case studies

Fig. 6 :

 6 Fig. 6: PaySafe (simplified)

and t b 0 =

 0 t b +(δ -t). if b ∈ M 0 then let w ∈ vars(R). By hypothesis, we know that there exists c ∈ A 0 such that w ∈ dom( Φ t b -Dist T (c,b) c

  and therefore there exists w ∈ dom( Φ 1 t b b ) such that wΦ 1 ↓ = u. Actually, it is easy to see that choosing the recipe R = w (and c = b) allows us to conclude. Indeed, we have that t b -Dist T (b, b) = t b , and therefore we conclude since we have already shown that w ∈ dom( Φ 1 t b b ).

  that wΦ = u. By definition of V , we have that b ∈ V , and therefore b ∈ A M . The same rule applies for the same reason. 2. In case b ∈ M 0 , then we know that there exists a recipe R such that RΦ 1 ↓ = u, and for all w ∈ vars(R) there exists c ∈ A 0 such that w ∈ dom( Φ 1 t b -Dist T (c,b) c

  S b = S 1 b ∪ S 2 b , and we consider the set FD(S b ) built as follows: 1. S := S b . 2. For each γ ∈ S, for all transition β in tr, if β → γ, then S := S ∪ {β}. 3. FD(S b ) := S.Let FD(S b ) be the set of transitions β such that β / ∈ FD(S b ) and β ∈ tr 2 ≥ .L in . We can note that for all action in L ∈ FD(S b ), its counterpart timed action L is executed at time t such that t ≥ t out + t g /2.Claim. 3. For all α ∈ FD(S b ) and β ∈ FD(S b ), we have that β → α.Proof. By construction of FD(S b ).Claim. 4. We have that L in ∈ FD(S b ).

Fig. 7 :

 7 Fig. 7: Topologies T t 0 MFnew , and T t 0 DHnew

  ∈ A0 and t b ∈ R+ such that t b ≤ t -DistT 0 (b, a) and:

	TIM	(P; Φ; t) -→T 0 (Shift(P, δ); Φ; t + δ)	with δ ≥ 0
	OUT	( out(u).P ta a ) P; Φ; t)	a,out(u) -----→T 0 ( P ta a	P; Φ {w	a,t --→ u}; t)
							with w ∈ W fresh
	LET	( let x = u in P ta a	P; Φ; t)	a,τ --→T 0 ( P {x → u↓} ta a when u↓ ∈ T (Σ + P; Φ; t) c , N A)
	NEW	( new n.P ta a	P; Φ; t)	a,τ --→T 0 ( P {n → n }	ta a	P; Φ; t) with n ∈ N fresh
	RST	( reset.P ta a	P; Φ; t)	a,τ --→T 0 ( P 0 a	P; Φ; t)
	IN	( in (x).P ta a	P; Φ; t)	a,in (u) -----→T 0 ( P {x → u} ta a	P; Φ; t)
	when there exist b

  ) . By Definition of S 2 a , we know that b 1 / ∈ Close(v 0 ) and thus Dist T (v 0 , b 1 ) ≥ t g /2, and thus t 1 b -t out ≥ t g /2. However, by definition of S 2 a , we know that t 1 b < t out + t g /2, yielding to a contradiction. This allows us to conclude the proof of this claim. With Claim 1 and Claim 2, we can apply Corollary 1, and thus, we can move all transitions in BD(S 1 a , S 2 a ) right before L reset , leading us to a partially-cleaned trace tr:

This work has been partially supported by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No 714955-POPSTAR).

Lemma 2, Proposition 5, Lemma 3 and Proposition 6 remain true. Hence all the proof can be followed similarly. A difference occurs in Step 3 in which we must proceed as follows:

1. we add two agents in the topology one close to v 0 and one close to p 0 2. we reduce the initial frame applying a projection more cleverly respecting honesty and roles.

Proof. (Detailed proof ) Consider a topology T 0 = (A 0 , M 0 , Loc 0 , v 0 , p 0 ) such that P prox admits an attack. Let K 0 = (P 0 ; Φ 0 ; t init ) be an initial configuration that is valid for P prox , V 0 w.r.t. T 0 and (I p 0 , I v 0 ) such that K 0 admits an attack w.r.t. t 0 -proximity in T 0 . We consider the execution witnessing this fact: K 0 tr -→ T0 ( end(v 0 , p 0 ).P ta v0 P; Φ 0 ∪ Φ; t) with Dist T0 (v 0 , p 0 ) ≥ t 0 .

We follow exactly the same shape of the proof of Theorem 2 presented in Appendix C.

Step 1-a. Applying Lemma 2 with H = A 0 (M 0 ∪ {v 0 , p 0 }), we obtain a topology

and Loc 1 = Loc 0 . We have that:

We now consider the configuration K + 0 = (P 0 ; Φ + 0 ; t init ) where we extend Φ 0 into Φ + 0 taking into account the role of each agent such that img( Φ + 0 t init a ) = Knows(I x 0 , a, A 1 ) when a ∈ M x 1 with x ∈ {p, v}. Since we only increase the knowledge, we have that:

with Dist T1 (v 0 , p 0 ) = Dist T0 (v 0 , p 0 ) ≥ t 0 .

Step 1-b. We follow exactly the same reasoning as in the previous proof. We successively apply Lemma 3 and Proposition 5 to obtain that:

where P 0 is obtained from P 0 by removing processes located in a ∈ M 1 .

Step 2. We now consider Φ ++ 0 the same as Φ + 0 but frame elements located at a ∈ M v 1 are moved to v 0 and frame elements located at a ∈ M p 1 are moved to p 0 . Let δ 0 = M ax(Dist T1 (v 0 , a)) for any a ∈ M 1 . Clearly, we have that:

with Dist T1 (v 0 , p 0 ) ≥ t 0 . Indeed, shifting by +δ 0 the initial configuration, all the messages moved from an agent a ∈ M 1 to v 0 or p 0 can be used by a at the time t init of the initial frame. Then we can apply Proposition 6 on T 1 and (P 0 ; Φ ++ 0 ; t init + δ 0 ) with V = {v 0 , p 0 }. We deduce that:

where

Arbitrarily we can assume that i v0 , i p0 ∈ A p (it does not modify the correctness of Proposition 6 because the Proposition does not talk about valid initial configuration and the semantic does not make difference between provers and verifiers).

Before enter in step 3, let us consider two new identities i v0 , i p0 ∈ A v \ A 0 and the extended topology

It is easy to see that the trace is still valid in this new topology because we just add two new agents:

Step 3. To reduce the size of the initial frame, we apply Lemma 1 on K 0 = (P 0 ; Φ ++ 0 ; t init + δ 0 ) using ρ 3 : A → A + 1 = {v 0 , p 0 , i v0 , i p0 , i v0 , i p0 } such that ρ 3 (a) = i v0 for any a ∈ A p \ A + 1 and ρ 3 (a) = i v0 for any a ∈ A v \ A + 1 . We have that:

with Dist T 1 (v 0 , p 0 ) ≥ t 0 . Now, we show that (P 0 ρ 3 ; Φ ++ 0 ρ 3 ; t init + δ 0 ) is almost valid. Indeed to turn this configuration into a valid one, we simply have to move frame elements (those that we have added during Step 1-a and moved during Step 2) located in v 0 (resp. p 0 ) to i v0 (resp. i p0 ). This will not change the underlying execution since both nodes are located at the exact same place and we have that img( Φ ++ 0

. Then, we add some frame elements in i v0 and i p0 , more precisely Knows(I p 0 , i p0 , A + 1 ) and Knows(I v 0 , i v0 , A + 1 ). These additional elements will not alter the underlying execution.

We may note that P 0 ρ 3 satisfies the first item of Definition 2: since P 0 is valid, there exits t such that V 0 (v 0 , p 0 ) t v0 ∈ P 0 and by construction P 0 ρ 3 still contains V 0 (v 0 , p 0 ) t v0 . Moreover, for all P t a ∈ P 0 ρ 3 , by construction, we know that a ∈ {v 0 , p 0 } = A + 1 \ M + 1 . Finally, we have that there exists P t a ∈ P 0 such that P = P (a , a 1 , . . . , a n ) for P ∈ P prox and P = P ρ 3 = P (a , ρ 3 (a 1 ), . . . , ρ 3 (a n )) with ρ 3 (a 1 ), . . . , ρ 3 (a n ) ∈ A 1 .

To conclude, we have to shorten the distance between v 0 , i v0 , i v0 and p 0 , i p0 , i p0 . To do so, we consider a new topology

We have that T = T t0 MFnew applying the renaming:

Distance hijacking attack

Theorem 5. Let (I p 0 , I v 0 ) be templates, P prox be a protocol, t 0 ∈ R + , and V 0 (z 0 , z 1 ) be a parametrised role obtained using the following grammar:

}) and t ≤ 2 × t 0 . If P prox admits a distance hijacking attack w.r.t. t 0 -proximity, then P prox admits an attack against t 0 -proximity in the topology T t0 DHnew .

Proof. Let T = (A 0 , M 0 , Loc, v 0 , p 0 ) ∈ C DH and K 0 = (P 0 ; Φ 0 ; t init ) be a valid initial configuration for the protocol P prox and V 0 w.r.t. T and (I p 0 , I v 0 ) such that we have an attack:

Lemma 4, Lemma 5, Corollary 1, Proposition 7 and thus Proposition 2 are still correct when restraining agent capabilities (because they do not talk about valid initial configuration).

Therefore Steps 1 to 4 of the proof of Theorem 3 in Appendix D can be repeated. We define the set Close(v 0 ) = {a ∈ A 0 | Dist T (v 0 , a) < t 0 } and the topology T = (A 0 , M 0 Loc , v 0 , p 0 ) in which Dist T (v 0 , p 0 ) = t 0 and:

We have that K 0 tr -→ T K1 where tr is a sequence of action and K1 is such that: untimed( K1 ) = untimed(K 1 ) where K 0 (resp. K 1 ) is the counterpart of K 0 (resp. K 1 ) in which guarded inputs have been replaced by simple inputs.

To finish we reduce the topology to T t0 DHnew = (A DH , M DH , Loc DH , v 0 , p 0 ). Let us consider the renaming:

for any a ∈ A 0 and ρ(a) ∈ M DH = {p 0 , v 1 } if and only if a ∈ M 0 , thanks to Lemma 1, we have that:

To conclude, it remains to show that K 0 ρ is a valid initial configuration for P prox and V 0 w.r.t. T t0

DHnew and (I p 0 , I v 0 ). Denoting Φ 0 the frame of K 0 (it is the same as in K 0 ) and t init the initial global time, we have to prove that img( Φ 0 ρ