M. Abadi and C. Fournet, Mobile values, new names, and secure communication, Proc. 28th Symposium on Principles of Programming Languages (POPL'01), pp.104-115, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01423924

G. Avoine, X. Bultel, S. Gambs, D. Gerault, P. Lafourcade et al., A terrorist-fraud resistant and extractor-free anonymous distancebounding protocol, Proc. 12th ACM Asia Conference on Computer and Communications Security (AsiaCCS'17), pp.800-814, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01588560

D. Baelde, S. Delaune, I. Gazeau, and S. Kremer, Symbolic verification of privacytype properties for security protocols with xor, Computer Security Foundations Symposium (CSF), 2017 IEEE 30th, pp.234-248, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01533694

D. Baelde, S. Delaune, and L. Hirschi, A reduced semantics for deciding trace equivalence, Logical Methods in Computer Science, vol.13, issue.2, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01906639

D. Basin, S. Capkun, P. Schaller, and B. Schmidt, Formal reasoning about physical properties of security protocols, ACM Transactions on Information and System Security (TISSEC), vol.14, issue.2, p.16, 2011.

D. A. Basin, S. Mödersheim, and L. Viganò, OFMC: A symbolic model checker for security protocols, International Journal of Information Security, vol.4, issue.3, pp.181-208, 2005.

K. Bhargavan, B. Blanchet, and N. Kobeissi, Verified models and reference implementations for the TLS 1.3 standard candidate, Proc. 38th IEEE Symposium on Security and Privacy (S&P'17), pp.483-502, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575920

B. Blanchet, Modeling and verifying security protocols with the applied pi calculus and proverif, Foundations and Trends in Privacy and Security, vol.1, issue.1-2, pp.1-135, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01423760

B. Blanchet, Symbolic and computational mechanized verification of the arinc823 avionic protocols, Proc. 30th IEEE Computer Security Foundations Symposium (CSF'17), pp.68-82, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575861

S. Brands and D. Chaum, Distance-bounding protocols, Workshop on the Theory and Application of Cryptographic Techniques, pp.344-359, 1993.

X. Bultel, S. Gambs, D. Gerault, P. Lafourcade, C. Onete et al., A proveranonymous and terrorist-fraud resistant distance-bounding protocol, Proc. 9th ACM Conference on Security & Privacy in Wireless and Mobile Networks, pp.121-133, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01510800

R. Chadha, V. Cheval, S. ¸. , and S. Kremer, Automated verification of equivalence properties of cryptographic protocol, ACM Transactions on Computational Logic, vol.23, issue.4, 2016.

T. Chothia, J. De-ruiter, and B. Smyth, Modelling and analysis of a hierarchy of distance bounding attacks, Proc. 27th USENIX Security Symposium (USENIX'18), pp.1563-1580, 2018.

T. Chothia, F. D. Garcia, J. De-ruiter, J. Van-den-breekel, and M. Thompson, Relay cost bounding for contactless EMV payments, Proc. 19th International Conference on Financial Cryptography and Data Security (FC'15), vol.8975, pp.189-206, 2015.

H. Comon-lundh, V. Cortier, and E. , Deciding security properties for cryptographic protocols. application to key cycles, ACM Transactions on Computational Logic, vol.11, issue.2, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00525775

H. Comon-lundh and S. Delaune, The finite variant property: How to get rid of some algebraic properties, Proc. 16th International Conference on Rewriting Techniques and Applications (RTA'05), vol.3467, pp.294-307

. Springer, , 2005.

C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. Van-der-merwe, A comprehensive symbolic analysis of TLS 1.3, Proc. 24th ACM Conference on Computer and Communications Security (CCS'17), pp.1773-1788, 2017.

A. Debant, S. Delaune, and C. Wiedling, A symbolic framework to analyse physical proximity in security protocols, Proc. 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'18)

. Lipics, , 2018.

D. Dolev and A. Yao, On the security of public key protocols, IEEE Transactions on information theory, vol.29, issue.2, pp.198-208, 1983.

N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov, Undecidability of bounded security protocols, Proc. Workshop on Formal Methods and Security Protocols (FMSP'99), 1999.

. Emvco, EMV contactless specifications for payment systems, version 2.6, 2016.

G. P. Hancke and M. G. Kuhn, An RFID distance bounding protocol, Proc. 1st International Conference on Security and Privacy for Emerging Areas in Communications Networks (SECURECOMM'05), pp.67-73, 2005.

P. Janssens, Proximity check for communication devices, US Patent, vol.9, p.228, 2017.

C. H. Kim, G. Avoine, F. Koeune, F. Standaert, and O. Pereira, The Swiss-Knife RFID distance bounding protocol, International Conference on Information Security and Cryptology, pp.98-115, 2008.

S. Mauw, Z. Smith, J. Toro-pozo, and R. Trujillo-rasua, Distance-bounding protocols: Verification without time and location, Proc. 39th IEEE Symposium on Security and Privacy (S&P'18)), pp.152-169, 2018.

C. Meadows, R. Poovendran, D. Pavlovic, L. Chang, and P. Syverson, Distance bounding protocols: Authentication logic analysis and collusion attacks. In Secure localization and time synchronization for wireless sensor and ad hoc networks, pp.279-298, 2007.

S. Meier, B. Schmidt, C. Cremers, and D. Basin, The Tamarin Prover for the Symbolic Analysis of Security Protocols, Proc. 25th International Conference on Computer Aided Verification (CAV'13), vol.8044, pp.696-701

. Springer, , 2013.

J. Millen and V. Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, Proc. 8th ACM Conference on Computer and Communications Security (CCS'01), 2001.

S. Mödersheim, L. Viganò, and D. A. Basin, Constraint differentiation: Searchspace reduction for the constraint-based analysis of security protocols, Journal of Computer Security, vol.18, issue.4, pp.575-618, 2010.

V. Nigam, C. Talcott, and A. A. Urquiza, Towards the automated verification of cyber-physical security protocols: Bounding the number of timed intruders, Proc. 21st European Symposium on Research in Computer Security (ESORICS'16), pp.450-470, 2016.

M. Rusinowitch, M. Turuani-;-?-{1, and .. .. N},-b-i-?-?-h, 0 )) with a proof tree ? i matching exec and R 1 ,. .. , R k and since ? is uniform we have that {? 1 ,. .. , ? n } is uniform. Let us distinguish two cases depending on the type of the statement f : ? {1,. .. , n}, there exists j ? Rcv(p) such that B i ? = k ?1,...,?j?1 (R |Rcv(j)| , u i ) for some term u i. Therefore, by hypothesis we have that R |Rcv(j)| is asap w.r.t. b |Rcv(j)| and exec. Moreover ? i (the proof of B i ? ? H(seed(T 0 ))) is uniform (as a subtree of ?). Our induction hypothesis applies with B i ?.-if f is a statement of type 4 then for all i ? {1,. .. , n}, B i ? = k ?1,...,?j?1 (S i , u i ) for some term u i , with S i a strict subterm of R. Since R is asap w.r.t. b |Rcv(j)| and exec, we deduce that S i is asap w.r.t. b |Rcv(j)| and exec (by Lemma 12), Protocol insecurity with a finite number of sessions and composed keys is NP-complete. Theoretical Computer Science, vol.299, pp.451-475, 2003.