×

A new logic for electronic commerce protocols. (English) Zbl 1008.68047

Summary: The primary objective of this paper is to present the definition of a new dynamic, linear and modal logic for security protocols. The logic is compact, expressive and formal. It allows the specification of classical security properties (authentication, secrecy and integrity) and also electronic commerce properties (non-repudiation, anonymity, good atomicity, money atomicity, certified delivery, etc.). The logic constructs are interpreted over a trace-based model. Traces reflect valid protocol executions in the presence of a malicious smart intruder. The logic is endowed with a tableau-based proof system that leads to a modular denotational semantics and local model checking.

MSC:

68P25 Data encryption (aspects in computer science)

Software:

NRL; Murphi
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] M. Abadi, A.D. Gordon, A calculus for cryptographic protocols: The spi calculus, Technical Report, DEC/SRC, 1996.; M. Abadi, A.D. Gordon, A calculus for cryptographic protocols: The spi calculus, Technical Report, DEC/SRC, 1996. · Zbl 0924.68073
[2] Abadi, M.; Gordon, A. D., A calculus for cryptographic protocolsThe spi calculus, (4th ACM Conf. on Computer and Communications Security (1997), ACM Press: ACM Press New York), 36-47
[3] 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.; 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. · Zbl 1314.68019
[4] Bieber, P.; Boulahia-Cuppens, N.; Lehmann, T.; van Wickeren, E., Abstract machines for communication security, (Proc. Computer Security Foundations Workshop VI (CSFW ’93) (1993), IEEE Computer Society Press: IEEE Computer Society Press Washington, Brussels, Tokyo), 137-146
[5] Bolignano, D., An approach to the formal verification of cryptographic protocols, (Proc. 3rd ACM Conf. on Computer and Communication Security, CCS’96, New Delhi, India (1996), ACM Press: ACM Press New York), 106-118
[6] Boyd, C., Security architectures using formal methods, J. Select. Areas Commun., 11, 5, 694-701 (1990)
[7] C. Boyd, C., A framework for authentication, (Proc. European Symp. on Research in Computer Security, ESORICS 92, Lecture Notes in Computer Science, Vol. 648 (1992), Springer: Springer Berlin), 273-292 · Zbl 1457.68028
[8] Burrows, M.; Abadi, M.; Needham, R., Rejoinder to nessett, ACM Oper. Systems Rev., 24, 2, 39-40 (1990)
[9] M. Burrows, M. Abadi, R. Needham, A logic of authentication, in: Proc. Royal Society of London A, Vol. 426, 1998, pp. 233-271.; M. Burrows, M. Abadi, R. Needham, A logic of authentication, in: Proc. Royal Society of London A, Vol. 426, 1998, pp. 233-271. · Zbl 0687.68007
[10] 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.; 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.
[11] U. Carlsen, Formal specification and analysis of cryptographic protocols, Ph.D. Thesis, Université PARIS XI, 1994.; U. Carlsen, Formal specification and analysis of cryptographic protocols, Ph.D. Thesis, Université PARIS XI, 1994.
[12] J. Clark, J. Jacob, A survey of authentication protocol literature, 1996, unpublished article.; J. Clark, J. Jacob, A survey of authentication protocol literature, 1996, unpublished article.
[13] 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.; 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.
[14] Cleaveland, R., Tableau-based model checking in the propositional mu-calculus, Acta Inform., 27, 8, 725-747 (1990) · Zbl 0676.03033
[15] Diffie, W.; Oorschot, P. C.V.; Wiener, M. J., Authentication and authenticated key exchanges, Designs, Codes Cryptography J., 2, 2, 107-125 (1992)
[16] Dill, D. L., The murphi verification system, (Alur, Rajeev; A. Henzinger, Thomas, Proc. 8th Internat. Conf. on Computer Aided Verification CAV, Lecture Notes in Computer Science, Vol. 1102 (1996), Springer: Springer New Brunswick, NJ, USA), 390-393
[17] D. Dolev, A. Yao, On the security of public key protocols, in: IEEE Transactions on Information Theory, 1983, pp. 198-208.; D. Dolev, A. Yao, On the security of public key protocols, in: IEEE Transactions on Information Theory, 1983, pp. 198-208. · Zbl 0502.94005
[18] Gaarder, K.; Snekkenes, E., Applying a formal analysis technique to the CCITT X.509 Strong two-way authentication protocol, J. Cryptol., 3, 2, 81-98 (1991) · Zbl 0726.68028
[19] 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, J. Hulance, B. Roscoe, Security modeling in CSP and FDR: Deliverable bundle 2, Technical Report, Formal Systems (Europe) Ltd, 1996.
[20] P. Gardiner, D. Jackson, B. Roscoe, Security modeling in CSP and FDR: Deliverable bundle 3, 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.
[21] V.D. Gligor, R. Kailar, On belief evolution in authentication protocols, in: Proc. IEEE Computer Security Foundations Workshop IV, Franconia, 1991, pp. 103-116.; V.D. Gligor, R. Kailar, On belief evolution in authentication protocols, in: Proc. IEEE Computer Security Foundations Workshop IV, Franconia, 1991, pp. 103-116.
[22] Gollman, D., What do we mean by entity authentication, (Proc. 1996 IEEE Symp. on Research in Security and Privacy (1996), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 46-54
[23] Gong, L.; Needham, R.; Yahalom, R., Reasoning about belief in cryptographic protocols, (Cooper, D.; Lunt, T., Proc. 1990 IEEE Symp. on Research in Security and Privacy (1990), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 234-248
[24] Goubault-Larrecq, J.; Mackie, I., Proof Theory and Automated Deduction, Applied Logic Series, Vol. 6 (1997), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht · Zbl 0896.03014
[25] Hoare, C. A.R., Communicating Sequential Process (1985), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[26] Iliano, C.; Durgin, N.; Lincoln, P.; Mitchell, J.; Scedrov, A., Relating strands and multiset rewriting for security protocol analysis, (Syverson, P., Proc. 13th IEEE Computer Security Foundations Workshop—CSFW’00 (2000), IEEE Computer Society Press: IEEE Computer Society Press Cambridge, UK), 35-51
[27] Kemmerer, R. A., Using formal verification techniques to analyze encryption protocols, (Proc. 1987 IEEE Symp. on Research in Security and Privacy (1987), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 134-139
[28] Kemmerer, R. A., Analyzing encryption protocols using formal verification techniques, IEEE J. Select. Areas Commun., 7, 4, 448-457 (1989)
[29] Kemmerer, R.; Meadows, C.; Millen, J., Three systems for cryptographic protocol analysis, J. Cryptol., 7, 2, 79-130 (1994) · Zbl 0814.94011
[30] Liebl, A., Authentication in distributed systemsa bibliography, Oper. Systems Rev., 27, 4, 122-136 (1993)
[31] Lowe, G., An attack on the Needham-Schroeder public key authentication protocol, Inform. Process. Lett., 56, 3, 131-136 (1995) · Zbl 0875.94114
[32] 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, SPLICE-AS: A case study in using CSP to detect errors in security protocols, Technical Report, Programming Research Group, Oxford, 1996.
[33] G. Lowe, Some new attacks upon security protocols, in: Proc. 9th IEEE Computer Security Foundations Workshop, 1996, pp. 162-169.; G. Lowe, Some new attacks upon security protocols, in: Proc. 9th IEEE Computer Security Foundations Workshop, 1996, pp. 162-169.
[34] Lowe, G., A hierarchy of authentication specifications, (Proc. 10th IEEE Computer Security Foundations Workshop (CSFW ’97) (1997), IEEE: IEEE Washington, Brussels, Tokyo), 31-44
[35] Mao, W.; Boyd, C., Towards the formal analysis of security protocols, (Proc. Computer Security Foundations Workshop VI (1993), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 147-158
[36] 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.; 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. · Zbl 0872.94035
[37] Meadows, C., The NRL protocol analyzer: an overview, J. Logic Programming, 26, 113-131 (1996) · Zbl 0871.68052
[38] R. Milner, The polyadic \(π\); R. Milner, The polyadic \(π\)
[39] 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.; 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. · Zbl 0752.68037
[40] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes (Parts I and II), Inform. Comput., 100, 1-77 (1992)
[41] Mitchell, J. C.; Mitchell, M.; Stern, U., Automated analysis of cryptographic protocols using murphi, (Proc. 1997 IEEE Symp. on Security and Privacy (1997), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 141-153
[42] 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.; 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.
[43] Paulson, L. C., The inductive approach to verifying cryptographic protocols, J. Comput. Security, 6, 85-128 (1998)
[44] Roscoe, A. W., Intentional specifications of security protocols, (Proc. 9th IEEE Computer Security Foundations Workshop (1996), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 28-38
[45] B. Roscoe, P. Gardiner, Security modeling in CSP and FDR: Final Report, Technical Report, Formal Systems Europe, 1995.; B. Roscoe, P. Gardiner, Security modeling in CSP and FDR: Final Report, Technical Report, Formal Systems Europe, 1995.
[46] 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.; 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.
[47] Schneider, S., Security properties and CSP, (Proc. 1996 IEEE Symp. on Security and Privacy (1996), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 174-187
[48] 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.; 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.
[49] E. Snekkenes, Authentication in open systems, 10th IFIP WG 6.1 Symp. on Protocol Specification, Testing and Verification (1990) 313-324.; E. Snekkenes, Authentication in open systems, 10th IFIP WG 6.1 Symp. on Protocol Specification, Testing and Verification (1990) 313-324.
[50] 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.; 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.
[51] Syverson, P., The use of logic in the analysis of cryptographic protocols, (Lunt, T. F.; McLean, J., Proc. 1991 IEEE Symp. on Security and Privacy (1991), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 156-170
[52] Syverson, P., Knowledge, belief, and semantics in the analysis of cryptographic protocols, J. Comput. Security, 1, 3, 317-334 (1992)
[53] Syverson, P.; Meadows, C., A formal language for cryptographic protocol requirements, Designs, Codes Cryptography, 7, 1/2, 27-59 (1996) · Zbl 0843.94010
[54] 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.; 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.
[55] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 5, 285-309 (1955) · Zbl 0064.26004
[56] The commission of the European Communities CEC DG-XIII, Security Investigation Final Report, Technical Report No. S2011/7000/D010 7000 1000, CEC, 1993.; The commission of the European Communities CEC DG-XIII, Security Investigation Final Report, Technical Report No. S2011/7000/D010 7000 1000, CEC, 1993.
[57] V. Varadharajan, Formal specification of a secure distributed system, in: Proc. 12th National Computer Security Conference, 1989, pp. 146-171.; V. Varadharajan, Formal specification of a secure distributed system, in: Proc. 12th National Computer Security Conference, 1989, pp. 146-171.
[58] Varadharajan, V., Use of formal techniques in the specification of authentication protocols, Comput. Standards Interfaces, 9, 203-215 (1990)
[59] Woo, T. Y.C.; Lam, S. S., A lesson on authentication protocol design, Oper. Systems Rev., 28, 24-37 (1994)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.