Using temporal logic to specify and verify cryptographic protocols

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by J.W. Gray, III Articles by J. McLean

The Eighth IEEE Computer Security Foundations Workshop (CSFW '95)

Kenmare, County Kerry, Ireland

March 13-March 15

ISBN: 0-8186-7033-9

	ASCII Text	x
	J.W. Gray, III, J. McLean, "Using temporal logic to specify and verify cryptographic protocols," Computer Security Foundations Workshop, IEEE, pp. 108, The Eighth IEEE Computer Security Foundations Workshop (CSFW '95), 1995.

	BibTex	x
	@article{ 10.1109/CSFW.1995.518557, author = {J.W. Gray, III and J. McLean}, title = {Using temporal logic to specify and verify cryptographic protocols}, journal ={Computer Security Foundations Workshop, IEEE}, volume = {0}, year = {1995}, issn = {1063-6900}, pages = {108}, doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.1995.518557}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Computer Security Foundations Workshop, IEEE TI - Using temporal logic to specify and verify cryptographic protocols SN - 1063-6900 SP EP A1 - J.W. Gray, III, A1 - J. McLean, PY - 1995 KW - temporal logic; protocols; cryptography; formal specification; formal verification; temporal logic; cryptographic protocols; specify; verify; system penetrator; correctness requirements; verification; formal methods VL - 0 JA - Computer Security Foundations Workshop, IEEE ER -

J.W. Gray, III, Dept. of Comput. Sci., Hong Kong Univ. of Sci. & Technol., Kowloon, Hong Kong

J. McLean, Dept. of Comput. Sci., Hong Kong Univ. of Sci. & Technol., Kowloon, Hong Kong

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSFW.1995.518557

We use standard linear-time temporal logic to specify cryptographic protocols, model the system penetrator, and specify correctness requirements. The requirements are specified as standard safety properties, for which standard proof techniques apply. In particular, we are able to prove that the system penetrator cannot obtain a session key by any logical or algebraic techniques. We compare our work to Meadows' method. We argue that using standard temporal logic provides greater flexibility and generality, firmer foundations, easier integration with other formal methods, and greater confidence in the verification results.

Index Terms:

temporal logic; protocols; cryptography; formal specification; formal verification; temporal logic; cryptographic protocols; specify; verify; system penetrator; correctness requirements; verification; formal methods

Citation:

J.W. Gray, III, J. McLean, "Using temporal logic to specify and verify cryptographic protocols," csfw, pp.108, The Eighth IEEE Computer Security Foundations Workshop (CSFW '95), 1995

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.