A symbolic decision procedure for cryptographic protocols with time stamps

Alur, 1994, A theory of timed automata, Theoretical Computer Science, 126, 10.1016/0304-3975(94)90010-8 R. Alur, T. Feder, T.A. Henzinger, The benefits of relaxing punctuality, in: Proceedings of the 10th ACM Symposium on Principles of Distributed Computing, ACM Press, 1991, pp. 139–152 R.M. Amadio, D.Lugiez, On the reachability problem in cryptographic protocols, in: International Conference on Concurrency Theory, LNCS, vol. 1877, 2000, pp. 380–394 G.Bella, L.C. Paulson, Mechanizing BAN Kerberos by the inductive method, in: A.J. Hu, M.Y. Vardi (Eds.), Proceedings of the 10th International Conference on Computer-Aided Verification (CAV’98), Vancouver, BC, Canada, June 1998, LNCS, Springer-Verlag, vol. 1427, pp. 416–427 M.Boreale, Symbolic trace analysis of cryptographic protocols, ICALP: Annual International Colloquium on Automata, Languages and Programming, 2001 A. Bouajjani, Y. Lakhnech, Temporal logic + timed automata: expressiveness and decidability, in: I. Lee, S.A. Smolka (Eds.), CONCUR’95: Concurrency Theory, LNCS, Springer-Verlag, vol. 962, 1995, pp. 531–546 L.Bozga, Automatic verification of cryptographic protocols, PhD thesis, University Joseph Fourier (Grenoble 1), 2004 Burrows, 1990, A logic of authentication, ACM Transactions on Computer Systems, 8, 18, 10.1145/77648.77649 J.A. Clark, J.L. Jacob, A survey of authentication protocol literature, Version 1.0, Department of Computer Science, University of York, November 1997 Ernie Cohen, Taps: a first-order verifier for cryptographic protocols, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW’00), IEEE Computer Society, 2000, p. 144 Comon, 1991, Disunification a survey Comon, 2002, Is it possible to decide whether a cryptographic protocol is secure or not?, Journal of Telecommunications and Information Technology H. Comon-Lundh, V. Cortier, New decidability results for fragments of first-order logic and application to cryptographic protocols, in: 14th Int. Conf. Rewriting Techniques and Applications (RTA’2003), LNCS, vol. 2706, 2003 Cortier, 2001, Proving secrecy is easy enough, IEEE Computer Security Foundations Workshop, 97 Dolev, 1983, On the security of public key protocols, IEEE Transactions on Information Theory, 29, 198, 10.1109/TIT.1983.1056650 Neil Evans, 2000, Analyzing time dependent security properties in CSP using PVS, ESORICS, 222 M. Fiore, M. Abadi, Computing symbolic models for verifying cryptographic protocols, in: 14th IEEE Computer Security Foundations Workshop (CSFW ’01), Washington–Brussels–Tokyo, June 2001, IEEE, pp. 160–173 Gong, 1992, A security risk of depending on synchronized clocks, Operating Systems Review, 26, 49, 10.1145/130704.130709 T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic model-checking for real-time systems, in: Seventh Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1992, pp. 394–406 Jouannaud, 1991, Solving equations in abstract algebras: a rule-based survey of unification G. Lowe, Breaking and fixing the Needham-Schroeder Public-Key protocol using FDR, in: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 1055, 1996, pp. 147–166 G. Lowe. A hierarchy of authentication specifications, in: 10th IEEE Computer Security Foundations Workshop (CSFW ’97), Washington–Brussels–Tokyo, June 1997, IEEE, pp. 31–44 Millen, 2001, Constraint solving for bounded-process cryptographic protocol analysis, ACM Conference on Computer and Communications Security, 166 Paulson, 1997, Proving properties of security protocols by induction, IEEE Computer Security Foundations Workshop, 70, 10.1109/CSFW.1997.596788 A.W. Roscoe. Intensional specification of security protocols, in: 9th IEEE Computer Security Foundations Workshop (CSFW ’96), Washington–Brussels–Tokyo, June 1996, IEEE, pp. 28–38 Rusinowitch, 2001, Protocol insecurity with finite number of sessions is NP-complete, IEEE Computer Security Foundations Workshop S. Schneider, Verifying authentication protocols with CSP, in: 10th IEEE Computer Security Foundations Workshop (CSFW ’97), Washington–Brussels–Tokyo, June 1997, IEEE, pp. 3–17 Alexander Schrijver, 1986 Thayer, 1998, Honest ideals on strand spaces, IEEE Computer Security Foundations Workshop, 66, 10.1109/CSFW.1998.683156 Venkataraman, 1987, Decidability of the purely existential fragment of the theory of term algebras, JACM, 10.1145/23005.24037 Woo, 1992, Authentication for distributed systems, Computer, 25, 39, 10.1109/2.108052