A semantics for a logic of authentication (extended abstract)

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback
Take a look at the new version of this page: [ beta version ]. Tell us what you think.

A semantics for a logic of authentication (extended abstract)

Full text

Pdf (1.63 MB)

Source

Annual ACM Symposium on Principles of Distributed Computing archive
Proceedings of the tenth annual ACM symposium on Principles of distributed computing table of contents

Montreal, Quebec, Canada

Pages: 201 - 216

Year of Publication: 1991

ISBN:0-89791-439-2

Authors

Martín Abadi	Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue, Palo Alto, CA
Mark R. Tuttle	Digital Equipment Corporation, Cambridge Research Lab, One Kendall Square, Bldg. 700, Cambridge, MA

Sponsors

SIGOPS: ACM Special Interest Group on Operating Systems
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 40, Citation Count: 39

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/112600.112618 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	ABKL90	Martin Abadi, Michael Burrows, Charles Kaufman, and Butler Lampson. Authentication and delegation with smart-cards. Research Report 67, DEC Systems Research Center, October 1990.
	AM90	Collin I'Anson , Chris Mitchell, Security defects in CCITT recommendation X.509: the directory authentication framework, ACM SIGCOMM Computer Communication Review, v.20 n.2, p.30-34, April, 1990 [doi>10.1145/378570.378623]
	BAN89	Michael Burrows, Martin Abadi, and Roger M. Needham. A logic of authentication. Proceedings of the Royal Society of London A, 426:233-271, 1989. A preliminary version appeared as Research Report 39, DEC Systems Research Center, Palo Alto, February 1989.
	BAN90	Michael Burrows , Martín Abadi , Roger Needham, Rejoinder to Nessett, ACM SIGOPS Operating Systems Review, v.24 n.2, p.39-40, April 1990 [doi>10.1145/382258.382790]
	Bie89	P. Bieber. Aspect Epist&niques des Protocols Cryptographiques. PhD thesis, Universite Paul-Sabatier de Toulouse, 1989.
	Boy90	C. Boyd. Towards a formal framework for authentication. Manuscript, University of Manchester, 1990.
	CG90	P.-C. Cheng and V. D. Gligor. On the formal specification and verification of a multiparty session protocol. In Proceedings of the 1990 IEEE Symposium on Security and Privacy, Oakland, CA, 1990.
	CM86	K. M. Chandy , Jayadev Misra, How processes learn, Distributed Computing, v.1 n.1, p.40-52, Jan. 1986 [doi>10.1007/BF01843569]
	DS90	D. Davis and R. Swick, Kerberos authentication and workstation services and Kerberos authentication at Project Athena. Technical Memorandum 424, MIT Laboratory for Computer Science, 1990.
	Eng90	U. Engberg. Analyzing authentication protocols. Technical Report DAIMI IR- 97, Aarhus University, 1990.
	FH87	Ronald Fagin and Joseph Y. Halpern. I'm OK if you're OK: On the notion of trusting communication. In Proceedings of the 2nd IEEE Symposium on Logic in Computer Science, pages 280-292, 1987. Also available as IBM Research Report RJ 5600.
	FH88	R. Fagin , J. Y. Halpern, Belief, awareness, and limited reasoning, Artificial Intelligence, v.34 n.1, p.39-76, Dec. 1987 [doi>10.1016/0004-3702(87)90003-8]
	GKSG91	V. D. Gligor, R. Kailar, S. Stubblebine, and L. Gong. Logics for cryptographic protocols-virtures and limitations. In Proceedings of the Computer Security Foundations Workshop IV, Franconia, NH, June 1991.
	GNY90	L. Gong, R, M, Needham, and R. Yahalom. Reasoning about belief in cryptographic protocols. In Proceedings of the 1990 IEEE Symposium on Security and Privacy, Oakland, CA, 1990.
	Gro90	Adam Grove. Semantics for cryptographic protocols (early draft, sections 1-3 only). Manuscript, August 1990.
	GS90	Klaus Gaarder , Einar Snekkenes, On the formal analysis of PKCS authentication protocols, Proceedings of the international conference on cryptology on Advances in cryptology, p.106-121, September 1990, Sydney, Australia
	Hin62	J. Hintikka. Knowiedge and Belief. Cornell University Press, 1962.
	HM84	J. Halpern , Y. Moses, Towards a theory of knowledge and ignorance: preliminary report, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
	HM90	Joseph Y. Halpern , Yoram Moses, Knowledge and common knowledge in a distributed environment, Journal of the ACM (JACM), v.37 n.3, p.549-587, July 1990 [doi>10.1145/79147.79161]
	KG91	Rajashekar Kailar and Virgil D. Gligor. On belief evolution in authentication protocols. University of Maryland, College Park, MD, February 1991.
	KNS90	J. Kohl, C. Neuman, and J, Steiner. The Kerberos network authentication service (version 5, draft 3). Available by anonymous ft p from at hens-dist.mit.edu as/Pub/doc/kerberos/V5 DRAFT3- RFC.{PS,TXT}, October 1990.
	MNSS87	S. P. Miller, C, Neuman, J. I. Schiller, and J. H. Saltzer. Kerberos authentication and authorization system. Project Athena Technical Plan Section E.2.1, MIT, July 1987.
	MT88	Yoram Moses and Mark R. Tuttle. Programming simultaneous actions using common knowledge. Algorithmic, 3:121- 169, 1988.
	Nes90	Dan M. Nessett, A critique of the Burrows, Abadi and Needham logic, ACM SIGOPS Operating Systems Review, v.24 n.2, p.35-38, April 1990 [doi>10.1145/382258.382789]
	Rac89	Racal Research Ltd. Private communication from John Walker, 1989.
	SM89	Yoav Shoham and Yoram Moses. Belief as defensible knowledge. In Proceedings of the llth International Joint Conference on Artijiciai Intelligence, pages 1168-1173, August 1989.
	Sne91	Einar Snekkenes. Exploring the BAN approach to protocol analysis. In Proceedings of the 1991 IEEE Symposium on Research in Security and Privacy, Oakland, CA, 1991. IEEE.
	Syv91	Paul Syverson. The use of logic in the analysis of cryptographic protocols. In Proceedings of the 1991 IEEE Symposium on Research in Security and Privacy, Oakland, CA, 1991. IEEE.

CITED BY 42

	Paul van Oorschot, Extending cryptographic logics of belief to key agreement protocols, Proceedings of the 1st ACM conference on Computer and communications security, p.232-243, November 03-05, 1993, Fairfax, Virginia, United States
	Birgit Pfitzmann, Sorting out signature schemes, Proceedings of the 1st ACM conference on Computer and communications security, p.74-85, November 03-05, 1993, Fairfax, Virginia, United States
	Paul F. Syverson, Adding time to a logic of authentication, Proceedings of the 1st ACM conference on Computer and communications security, p.97-101, November 03-05, 1993, Fairfax, Virginia, United States
	Yongxing Sun , Xinmei Wang, An approach to finding the attacks on the cryptographic protocols, ACM SIGOPS Operating Systems Review, v.34 n.3, p.19-28, July 2000
	Dominique Bolignano, An approach to the formal verification of cryptographic protocols, Proceedings of the 3rd ACM conference on Computer and communications security, p.106-118, March 14-15, 1996, New Delhi, India
	Kamel Adi , Mourad Debbabi , Mohamed Mejri, A new logic for electronic commerce protocols, Theoretical Computer Science, v.291 n.3, p.223-283, 6 January 2003
	Stuart G. Stubblebine , Rebecca N. Wright, An authentication logic supporting synchronization, revocation, and recency, Proceedings of the 3rd ACM conference on Computer and communications security, p.95-105, March 14-15, 1996, New Delhi, India
	Luigia Carlucci Aiello , Fabio Massacci, Verifying security protocols as planning in logic programming, ACM Transactions on Computational Logic (TOCL), v.2 n.4, p.542-580, Oct. 2001
	Fabio Martinelli, Analysis of security protocols as open systems, Theoretical Computer Science, v.290 n.1, p.1057-1106, 1 January 2003
	Raphael Yahalom, Optimality of multi-domain protocols, Proceedings of the 1st ACM conference on Computer and communications security, p.38-48, November 03-05, 1993, Fairfax, Virginia, United States
	Alec Yasinsac, Dynamic analysis of security protocols, Proceedings of the 2000 workshop on New security paradigms, p.77-87, September 18-21, 2000, Ballycotton, County Cork, Ireland
	Stuart G. Stubblebine , Rebecca N. Wright, An Authentication Logic with Formal Semantics Supporting Synchronization, Revocation, and Recency, IEEE Transactions on Software Engineering, v.28 n.3, p.256-285, March 2002
	David Monniaux, Abstracting cryptographic protocols with tree automata, Science of Computer Programming, v.47 n.2-3, p.177-202, May 2003
	Yan Zhang , Vijay Varadharajan, A logic for modeling the dynamics of beliefs in cryptographic protocols, Australian Computer Science Communications, v.23 n.1, p.215-222, January-February 2001
	Nevin Heintze , J. D. Tygar, A Model for Secure Protocols and Their Compositions, IEEE Transactions on Software Engineering, v.22 n.1, p.16-30, January 1996
	Riccardo Pucella, Specifying confidentiality, ACM SIGACT News, v.35 n.4, December 2004
	Paul Syverson , Catherine Meadows, A Formal Language for Cryptographic Protocol Requirements, Designs, Codes and Cryptography, v.7 n.1-2, p.27-59, Jan. 1996
	Rajashekar Kailar, Accountability in Electronic Commerce Protocols, IEEE Transactions on Software Engineering, v.22 n.5, p.313-328, May 1996
	R. Ramanujam , S. P. Suresh, Deciding knowledge properties of security protocols, Proceedings of the 10th conference on Theoretical aspects of rationality and knowledge, June 10-12, 2005, Singapore
	Chiara Bodei , Mikael Buchholtz , Pierpaolo Degano , Flemming Nielson , Hanne Riis Nielson, Static validation of security protocols, Journal of Computer Security, v.13 n.3, p.347-390, May 2005
	Qingfeng Chen , Chengqi Zhang , Shichao Zhang, ENDL: A Logical Framework for Verifying Secure Transaction Protocols, Knowledge and Information Systems, v.7 n.1, p.84-109, January 2005
	Danny Dolev, Century papers at the first quarter-century milestone, Proceedings of the twenty-fifth annual ACM symposium on Principles of distributed computing, p.3-4, July 23-26, 2006, Denver, Colorado, USA
	R. Ramanujam , S. P. Suresh, A (restricted) quantifier elimination for security protocols, Theoretical Computer Science, v.367 n.1, p.228-256, 24 November 2006
	Alessio Lomuscio , Bozena Woźna, A complete and decidable security-specialised logic and its application to the TESLA protocol, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
	Clare Dixon , Mari-Carmen Fernández Gago , Michael Fisher , Wiebe van der Hoek, Temporal Logics of Knowledge and their Applications in Security, Electronic Notes in Theoretical Computer Science (ENTCS), 186, p.27-42, July, 2007
	Mirosław Kurkowski , Marian Srebrny, A Quantifier-free First-order Knowledge Logic of Authentication, Fundamenta Informaticae, v.72 n.1-3, p.263-282, January 2006
	Yuqing Zhang , Jihong Li , Guozhen Xiao, An approach to the formal verification of the two-party cryptographic protocols, ACM SIGOPS Operating Systems Review, v.33 n.4, p.48-51, Oct. 1999
	Shouhuai Xu , Gendu Zhang , Hong Zhu, On the properties of cryptographic protocols and the weaknesses of the BAN-like logics, ACM SIGOPS Operating Systems Review, v.31 n.4, p.12-23, Oct. 1997
	Paul F. Syverson, A new look at an old protocol, ACM SIGOPS Operating Systems Review, v.30 n.3, p.1-4, July 1996
	Ulf Carlsen, Optimal privacy and authentication on a portable communications system, ACM SIGOPS Operating Systems Review, v.28 n.3, p.16-23, July 1994
	Paul Syverson, On key distribution protocols for repeated authentication, ACM SIGOPS Operating Systems Review, v.27 n.4, p.24-30, Oct. 1993
	Sabina Petride , Riccardo Pucella, Perfect cryptography, S5 knowledge, and algorithmic knowledge, Proceedings of the 11th conference on Theoretical aspects of rationality and knowledge, June 25-27, 2007, Brussels, Belgium
	Michael Backes , Birgit Pfitzmann , Michael Waidner, The reactive simulatability (RSIM) framework for asynchronous systems, Information and Computation, v.205 n.12, p.1685-1720, December, 2007
	Wouter Teepe, On BAN logic and hash functions or: how an unjustified inference rule causes problems, Autonomous Agents and Multi-Agent Systems, v.19 n.1, p.76-88, August 2009
	Aaron Hunter , James P. Delgrande, Belief change and cryptographic protocol verification, Proceedings of the 22nd national conference on Artificial intelligence, p.427-433, July 22-26, 2007, Vancouver, British Columbia, Canada
	Kai-Le Su , Qing-Liang Chen , Abdul Sattar , Wei-Ya Yue , Guan-Feng Lv , Xi-Zhong Zheng, Verification of authentication protocols for epistemic goals via SAT compilation, Journal of Computer Science and Technology, v.21 n.6, p.932-943, November 2006
	Ji Ma , Mehmet A. Orgun , Abdul Sattar, Analysis of authentication protocols in agent-based systems using labeled tableaux, IEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics, v.39 n.4, p.889-900, August 2009
	Sigrid Gürgens , Peter Ochsenschläger , Carsten Rudolph, On a formal framework for security properties, Computer Standards & Interfaces, v.27 n.5, p.457-466, June, 2005
	Kaile Su , Abdul Sattar , Guanfeng Lv , Yan Zhang, Variable forgetting in reasoning about knowledge, Journal of Artificial Intelligence Research, v.35 n.1, p.677-716, May 2009
	Arjen Hommersom , John-Jules Meyer , Erik de Vink, Toward Reasoning about Security Protocols: A Semantic Approach, Electronic Notes in Theoretical Computer Science (ENTCS), 126, p.53-75, March, 2005
	Mike Bond , Jolyon Clulow, Extending Security Protocol Analysis: New Challenges, Electronic Notes in Theoretical Computer Science (ENTCS), v.125 n.1, p.13-24, March, 2005
	Chen Hao , John A. Clark , Jeremy L. Jacob, Synthesising Efficient and Effective Security Protocols, Electronic Notes in Theoretical Computer Science (ENTCS), v.125 n.1, p.25-41, March, 2005