A HOL extension of GNY for automatically analyzing cryptographic protocols

CC
CSFW
1996
Ninth IEEE Computer Security Foundations Workshop
Abstract - A HOL extension of GNY for automatically analyzing 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
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by S.H. Brackin

Ninth IEEE Computer Security Foundations Workshop

Dromquinna Manor, Kenmare, County Kerry, Ireland

March 10-March 12

ISBN: 0-8186-7522-5

	ASCII Text	x
	S.H. Brackin, "A HOL extension of GNY for automatically analyzing cryptographic protocols," Computer Security Foundations Workshop, IEEE, pp. 62, Ninth IEEE Computer Security Foundations Workshop, 1996.

	BibTex	x
	@article{ 10.1109/CSFW.1996.503691, author = {S.H. Brackin}, title = {A HOL extension of GNY for automatically analyzing cryptographic protocols}, journal ={Computer Security Foundations Workshop, IEEE}, volume = {0}, year = {1996}, issn = {1063-6900}, pages = {62}, doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.1996.503691}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Computer Security Foundations Workshop, IEEE TI - A HOL extension of GNY for automatically analyzing cryptographic protocols SN - 1063-6900 SP EP A1 - S.H. Brackin, PY - 1996 KW - message authentication; cryptography; access protocols; belief maintenance; formal specification; HOL extension; automatically analyzing cryptographic protocols; higher order logic theory; belief logic; authentication properties; protocol properties; multiple encryption; hash operations; message authentication codes; key-exchange algorithms VL - 0 JA - Computer Security Foundations Workshop, IEEE ER -

S.H. Brackin, Arca Syst. Inc., Hanscom AFB, MA, USA

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

This paper describes a Higher Order Logic (HOL) theory formalizing an extended version of the Gong, Needham, Yahalom (GNY) belief logic, a theory used by software that automatically proves authentication properties of cryptographic protocols. The theory's extensions to the GNY logic include being able to specify protocol properties at intermediate stages and being able to specify protocols that use multiple encryption and hash operations, message authentication codes, computed values (e.g., hash codes) as keys, and key-exchange algorithms.

Index Terms:

message authentication; cryptography; access protocols; belief maintenance; formal specification; HOL extension; automatically analyzing cryptographic protocols; higher order logic theory; belief logic; authentication properties; protocol properties; multiple encryption; hash operations; message authentication codes; key-exchange algorithms

Citation:

S.H. Brackin, "A HOL extension of GNY for automatically analyzing cryptographic protocols," csfw, pp.62, Ninth IEEE Computer Security Foundations Workshop, 1996

Peer Review Notice | Give Us Feedback

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