, On Name Generation and Set-Based Analysis in the Dolev-Yao Model, Proceedings of CONCUR 02, number 2421 in Lecture Notes in Computer Science, pp.499-512, 2002.
DOI : 10.1007/3-540-45694-5_33
, On the Reachability Problem in Cryptographic Protocols, Proceedings of CONCUR'00, 2000.
DOI : 10.1007/3-540-44618-4_28
URL : https://hal.archives-ouvertes.fr/inria-00072738
, Lazy Infinite-State Analysis of Security Protocols, Secure Networking ? CQRE (Secure)'99, pp.30-42, 1999.
DOI : 10.1007/3-540-46701-7_3
, String-rewriting systems, 1993.
, Symbolic Trace Analysis of Cryptographic Protocols, Proceedings of the 28th International Conference on Automata, Language and Programming: ICALP'01, pp.667-681, 2001.
DOI : 10.1007/3-540-48224-5_55
, Automated Unbounded Verification of Security Protocols, 14th International Conference on Computer Aided Verification, pp.324-337, 2002.
DOI : 10.1007/3-540-45657-0_24
URL : https://hal.archives-ouvertes.fr/inria-00100916
, A survey of authentication protocol literature, 1997.
, Tree Automata with One Memory, Set Constraints, and Ping-Pong Protocols, Proceedings of the 28th International Conference on Automata, Language and Programming: ICALP'01, 2001.
DOI : 10.1007/3-540-48224-5_56
, On the security of public key protocols, Proc. IEEE Symp. on Foundations of Computer Science, pp.350-357, 1981.
, Undecidability of Bounded Security Protocols, Proceedings of the FLOC'99 Workshop on Formal Methods and Security Protocols, 1999.
, Computing symbolic models for verifying cryptographic protocols, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001.
DOI : 10.1109/CSFW.2001.930144
, On the decidability of cryptographic protocols with open-ended data structures, 13th International Conference on Concurrency Theory, pp.515-530, 2002.
, An attack on the Needham-Schroeder public-key authentication protocol, Information Processing Letters, vol.56, issue.3, pp.131-133, 1996.
DOI : 10.1016/0020-0190(95)00144-2
, Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.147-166, 1996.
DOI : 10.1007/3-540-61042-1_43
, A unification algorithm for the group Diffie-Hellman protocol, Workshop on Issues in the Theory of Security (in conjunction with POPL'02), 2002.
, Constraint solving for bounded-process cryptographic protocol analysis, Proceedings of the 8th ACM conference on Computer and Communications Security , CCS '01, pp.166-175, 2001.
DOI : 10.1145/501983.502007
, Finite-state analysis of SSL 3.0, Seventh USENIX Security Symposium, pp.201-216, 1998.
, Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, 1978.
DOI : 10.1145/359657.359659
, Mechanized proofs for a recursive authentication protocol, Proceedings 10th Computer Security Foundations Workshop, pp.84-95, 1997.
DOI : 10.1109/CSFW.1997.596790
, On the perfect encryption assumption In Workshop on Issues in the Theory of Security (in conjunction with ICALP'00), pp.42-45, 2000.
, Protocol insecurity with finite number of sessions is NP-complete, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001.
DOI : 10.1109/CSFW.2001.930145
URL : https://hal.archives-ouvertes.fr/inria-00100411
, An attack on a recursive authentication protocol, Information Processing Letters, vol.65, 1998.
, A new efficient automatic checker for security protocol analysis 8.2 XOR rules We now prove that the XOR rules form a set of oracle rules. We start to show Definition 4 To do so, we first prove a sufficient condition for a derivation to be well formed, Proceedings of The 12th Computer Security Foundations Workshop, 1999.
, E n?1 ? Ln E n be a derivation with goal g such that: 1. For every j with E j?1 ? Lj E j?1 , t the jth step in D and L j ? L d (t), there exists t ? E j?1 such that t is a subterm of t and either t ? E 0 or there exists i
, n} that L i ? L d (t) implies t ? Sub(E 0 ) for every message t Using (2), we prove by induction on n ? i that for all , n}, L i ? L c (t) implies t ? Sub(E 0 , g) If n ? i = 0, then t = g and therefore t ? Sub(E 0 , g) For the induction step) implies that there exists j > i such that L j is a t -rule and t ? Sub, If L j ? L d (t ), then t ? Sub(E 0 ) (see above). If L j ? L c (t ), then by induction t ? Sub(E 0 , g), and hence
, ? Ln E n be a derivation of goal g of minimal length. We prove that D satisfies (1) and (2) in Lemma 9 We first show
, Proof of the claim By definition of xor rules, u is a normalized xor sum of elements in F, t and t is a normalized xor sum of elements in F . Thus, u is an xor sum of elements in F . Thus, F ? Lo(u) F, u. This concludes the proof of the claim. By the claim w.l.o.g. we may assume that in D the terms used on the left hand-side of an XOR rules are not generated by XOR rules. Formally (*): For every i with L i ? L o (t) and L i = F ? t, there does not exist j ? {1, . . . , n} such that L j ? L o (t ) for some t ? F . Now, we prove (1) and (2) of Lemma 9: 1. If L j ? L d (s) ? L d (t), then L i / ? L oc (s), for all i < j, since rules in L oc do not create standard terms, and L i / ? L c (s), for all i < j, by the definition of derivation (since otherwise t would be in the left-hand side of L i ) Therefore
, then t is standard and, by (*) and the definition of L od , there exists a non standard term t in E j?1 with t subterm of t and such that L oc
, Otherwise, there exists i < j such that L i is a t -rule. Since t is non standard
, there exists j > i such that t belongs to the left-hand side of L j . By definition of a derivation, L j / ? L d (t) If L j ? L c (t ), then t ? Sub(t ), and if L j ? L o (t ), then since t is standard, either t is a factor of t , and thus, t ? Sub, or there exists t ? E j?1 non standard with t ? Sub(t ) (t is used to simplify t ). By (*), t was not generated by some rule in L o
, t) and i < n, then (*) implies that t = g or there exists j > i such that L i ? L c (t )