A new logic for electronic commerce protocols

M. Abadi, A.D. Gordon, A calculus for cryptographic protocols: The spi calculus, Technical Report, DEC/SRC, 1996. Abadi, 1997, A calculus for cryptographic protocols, 36 M. Abadi, M.R. Tuttle, A semantics for a logic of authentication, in: Proc. 10th Annu. ACM Symp. on Principles of Distributed Computing, 1991, pp. 201–216. Bieber, 1993, Abstract machines for communication security, 137 Bolignano, 1996, An approach to the formal verification of cryptographic protocols, 106 Boyd, 1990, Security architectures using formal methods, J. Select. Areas Commun., 11, 694, 10.1109/49.223872 C.Boyd, 1992, A framework for authentication, Vol. 648, 273 Burrows, 1990, Rejoinder to nessett, ACM Oper. Systems Rev., 24, 39, 10.1145/382258.382790 M. Burrows, M. Abadi, R. Needham, A logic of authentication, in: Proc. Royal Society of London A, Vol. 426, 1998, pp. 233–271. L. Buttyan, Formal methods in the design of cryptographic protocols (state of the art), Technical Report No. SSC/1999/38, Swiss Federal Institute of Technology (EPFL), Lausanne, 1999. U. Carlsen, Formal specification and analysis of cryptographic protocols, Ph.D. Thesis, Université PARIS XI, 1994. J. Clark, J. Jacob, A survey of authentication protocol literature, 1996, unpublished article. E. Clarke, W. Marrero, S. Jha, A machine checkable logic of knowledge for specifying security properties of electronic commerce protocols, in: Proc. IFIP Working Conf. on Programming Concepts and Methods, PROCOMET. Cleaveland, 1990, Tableau-based model checking in the propositional mu-calculus, Acta Inform., 27, 725, 10.1007/BF00264284 Diffie, 1992, Authentication and authenticated key exchanges, Designs, Codes Cryptography J., 2, 107, 10.1007/BF00124891 Dill, 1996, The murphi verification system, Vol. 1102, 390 D. Dolev, A. Yao, On the security of public key protocols, in: IEEE Transactions on Information Theory, 1983, pp. 198–208. Gaarder, 1991, Applying a formal analysis technique to the CCITT X.509 Strong two-way authentication protocol, J. Cryptol., 3, 81, 10.1007/BF00196790 P. Gardiner, D. Jackson, J. Hulance, B. Roscoe, Security modeling in CSP and FDR: Deliverable bundle 2, Technical Report, Formal Systems (Europe) Ltd, 1996. P. Gardiner, D. Jackson, B. Roscoe, Security modeling in CSP and FDR: Deliverable bundle 3, Technical Report, Formal Systems (Europe) Ltd, 1996. V.D. Gligor, R. Kailar, On belief evolution in authentication protocols, in: Proc. IEEE Computer Security Foundations Workshop IV, Franconia, 1991, pp. 103–116. Gollman, 1996, What do we mean by entity authentication, 46 Gong, 1990, Reasoning about belief in cryptographic protocols, 234 Goubault-Larrecq, 1997, Proof Theory and Automated Deduction, Vol. 6 Hoare, 1985 Iliano, 2000, Relating strands and multiset rewriting for security protocol analysis, 35 Kemmerer, 1987, Using formal verification techniques to analyze encryption protocols, 134 Kemmerer, 1989, Analyzing encryption protocols using formal verification techniques, IEEE J. Select. Areas Commun., 7, 448, 10.1109/49.17707 Kemmerer, 1994, Three systems for cryptographic protocol analysis, J. Cryptol., 7, 79, 10.1007/BF00197942 Liebl, 1993, Authentication in distributed systems, Oper. Systems Rev., 27, 122 Lowe, 1995, An attack on the Needham–Schroeder public key authentication protocol, Inform. Process. Lett., 56, 131, 10.1016/0020-0190(95)00144-2 G. Lowe, SPLICE-AS: A case study in using CSP to detect errors in security protocols, Technical Report, Programming Research Group, Oxford, 1996. G. Lowe, Some new attacks upon security protocols, in: Proc. 9th IEEE Computer Security Foundations Workshop, 1996, pp. 162–169. Lowe, 1997, A hierarchy of authentication specifications, 31 Mao, 1993, Towards the formal analysis of security protocols, 147 C. Meadows, Formal verification of cryptographic protocols: A survey, in: ASIACRYPT: Advances in Cryptology—ASIACRYPT: Internat. Conf. on the Theory and Application of Cryptology, Lecture Notes in Computer Science, Vol. 917, Springer, Berlin, 1994, pp. 133–150. Meadows, 1996, The NRL protocol analyzer: an overview, J. Logic Programming, 26, 113, 10.1016/0743-1066(95)00095-X R. Milner, The polyadic π-calculus: A tutorial, Technical Report, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1991. R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, Technical Report, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1989. Milner, 1992, A calculus of mobile processes (Parts I and II), Inform. Comput., 100, 1, 10.1016/0890-5401(92)90008-4 Mitchell, 1997, Automated analysis of cryptographic protocols using murphi, 141 J.C. Mitchell, V. Shmatikov, U. Stern, Finite-state analysis of SSL 3.0, in: Proc. DIMACS Workshop on Design and Formal Verification of Security Protocols, September 3–5, 1997, DIMACS Center, CoRE Building, Rutgers University, New Jersey, USA, 1997, pp. 1–20. Paulson, 1998, The inductive approach to verifying cryptographic protocols, J. Comput. Security, 6, 85, 10.3233/JCS-1998-61-205 Roscoe, 1996, Intentional specifications of security protocols, 28 B. Roscoe, P. Gardiner, Security modeling in CSP and FDR: Final Report, Technical Report, Formal Systems Europe, 1995. A.D. Rubin, P. Honeyman, Formal methods for the analysis of authentication protocols, Technical Report No. 93-7, Internal Draft, Center for Information Technology Integration, University of Michigan, MI, 1993. Schneider, 1996, Security properties and CSP, 174 V. Shmatikov, J.C. Mitchell, Analysis of a fair exchange protocol, Proc. 7th Annu. Symp. on Network and Distributed System Security, San Diego, 2000, pp. 119–128. E. Snekkenes, Authentication in open systems, 10th IFIP WG 6.1 Symp. on Protocol Specification, Testing and Verification (1990) 313–324. E. Snekkenes, Formal specification and analysis of cryptographic protocols, Ph.D. Thesis, Faculty of Mathematics and Natural Sciences, University of Oslo, Norwegian Defense Research Establishment, P.O. Box 25, N-2007, Kjeller, Norway, 1995. Syverson, 1991, The use of logic in the analysis of cryptographic protocols, 156 Syverson, 1992, Knowledge, belief, and semantics in the analysis of cryptographic protocols, J. Comput. Security, 1, 317, 10.3233/JCS-1992-13-407 Syverson, 1996, A formal language for cryptographic protocol requirements, Designs, Codes Cryptography, 7, 27, 10.1023/A:1018069220646 P. Syverson, C. Meadows, C. Iliano, Dolev-Yao is no better than Machiavelli, in: P. Degano (Ed.), Proc. 1st Workshop on Issues in the Theory of Security—WITS’00, Geneva, Switzerland, 2000, pp. 87–92. Tarski, 1955, A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 5, 285, 10.2140/pjm.1955.5.285 The commission of the European Communities CEC DG-XIII, Security Investigation Final Report, Technical Report No. S2011/7000/D010 7000 1000, CEC, 1993. V. Varadharajan, Formal specification of a secure distributed system, in: Proc. 12th National Computer Security Conference, 1989, pp. 146–171. Varadharajan, 1990, Use of formal techniques in the specification of authentication protocols, Comput. Standards Interfaces, 9, 203, 10.1016/0920-5489(89)90022-6 Woo, 1994, A lesson on authentication protocol design, Oper. Systems Rev., 28, 24, 10.1145/182110.182113