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
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
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
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
Formal reasoning about physical properties of security protocols, ACM Transactions on Information and System Security (TISSEC), vol.14, issue.2, p.16, 2011. ,
OFMC: A symbolic model checker for security protocols, International Journal of Information Security, vol.4, issue.3, pp.181-208, 2005. ,
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
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
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
Distance-bounding protocols, Workshop on the Theory and Application of Cryptographic Techniques, pp.344-359, 1993. ,
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
Automated verification of equivalence properties of cryptographic protocol, ACM Transactions on Computational Logic, vol.23, issue.4, 2016. ,
Modelling and analysis of a hierarchy of distance bounding attacks, Proc. 27th USENIX Security Symposium (USENIX'18), pp.1563-1580, 2018. ,
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. ,
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
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 ,
, , 2005.
A comprehensive symbolic analysis of TLS 1.3, Proc. 24th ACM Conference on Computer and Communications Security (CCS'17), pp.1773-1788, 2017. ,
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) ,
, , 2018.
On the security of public key protocols, IEEE Transactions on information theory, vol.29, issue.2, pp.198-208, 1983. ,
Undecidability of bounded security protocols, Proc. Workshop on Formal Methods and Security Protocols (FMSP'99), 1999. ,
EMV contactless specifications for payment systems, version 2.6, 2016. ,
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. ,
Proximity check for communication devices, US Patent, vol.9, p.228, 2017. ,
The Swiss-Knife RFID distance bounding protocol, International Conference on Information Security and Cryptology, pp.98-115, 2008. ,
Distance-bounding protocols: Verification without time and location, Proc. 39th IEEE Symposium on Security and Privacy (S&P'18)), pp.152-169, 2018. ,
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. ,
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 ,
, , 2013.
Constraint solving for bounded-process cryptographic protocol analysis, Proc. 8th ACM Conference on Computer and Communications Security (CCS'01), 2001. ,
Constraint differentiation: Searchspace reduction for the constraint-based analysis of security protocols, Journal of Computer Security, vol.18, issue.4, pp.575-618, 2010. ,
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. ,
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. ,