Mobile values, new names, and secure communication, Proc. of the 28th ACM Symposium on Principles of Programming Languages (POPL'01), pp.104-115, 2001. ,
URL : https://hal.archives-ouvertes.fr/hal-01423924
An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001. ,
DOI : 10.1109/CSFW.2001.930138
Verification of cryptographic protocols: Tagging enforces termination, Foundations of Software Science and Computation Structures (FoSSaCS'03), 2003. ,
Protocol composition for arbitrary primitives, Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10), pp.322-336, 2010. ,
Safely composing security protocols. Formal Methods in System Design, pp.1-36, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00157889
Protocol Composition Logic (PCL), Electronic Notes in Theoretical Computer Science, vol.172, pp.311-358, 2007. ,
DOI : 10.1016/j.entcs.2007.02.012
The transport layer security (tls) protocol version 1.2 (rfc 5246), 2008. ,
Verifying layered security protocols, Journal of Computer Security, vol.23, issue.3, p.2015 ,
DOI : 10.3233/JCS-150526
Authentication tests and disjoint encryption: A design method for security protocols*, Journal of Computer Security, vol.12, issue.3-4, pp.3-4409, 2004. ,
DOI : 10.3233/JCS-2004-123-405
Establishing and preserving protocol security goals, Journal of Computer Security, vol.22, issue.2, pp.203-267, 2004. ,
DOI : 10.3233/JCS-140499
Protocol independence through disjoint encryption The TAMARIN Prover for the Symbolic Analysis of Security Protocols, Proc. 13th Computer Security Foundations Workshop (CSFW'00) Computer Aided Verification, 25th International Conference, CAV 2013, pp.24-34, 2000. ,
Lessons learned from previous ssl/tls attacks : A brief chronology of attacks and weaknesses, IACR Cryptology ePrint, 2013. ,
Sufficient conditions for vertical composition of security protocols, Proceedings of the 9th ACM symposium on Information, computer and communications security, ASIA CCS '14, pp.435-446, 2014. ,
DOI : 10.1145/2590296.2590330
Formal analysis of card-based payment systems in mobile services. In Fourth Australian information security workshop, conferences in research and practise in information security, pp.213-220, 2006. ,
The CL-Atse Protocol Analyser, Term Rewriting and Applications -Proc. of RTA, pp.277-286, 2006. ,
DOI : 10.1007/11805618_21
URL : https://hal.archives-ouvertes.fr/inria-00103573
F i ? i , d) ? tr and d Ch p is equivalent to all agents in ta are honest; and 2. for all roles R = r 1 . . . . .r n of P, for all , n}, if r i = out A (c pub , E?) (resp. r i = in A (c pub , E?)) for some agent A, some substitution ? and some encapsulation (E, F) ? S then there exists c, d, ta such that, X E ?)? = d and: ? either there exist j < i ,
F??, d) ? tr and d Ch p is equivalent to all agents in ta are honest ,