Title :
A HOL extension of GNY for automatically analyzing cryptographic protocols
Author :
Brackin, Stephen H.
Author_Institution :
Arca Syst. Inc., Hanscom AFB, MA, USA
Abstract :
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
Keywords :
access protocols; belief maintenance; cryptography; formal specification; message authentication; HOL extension; authentication properties; automatically analyzing cryptographic protocols; belief logic; hash operations; higher order logic theory; key-exchange algorithms; message authentication codes; multiple encryption; protocol properties; Automatic logic units; Cryptographic protocols; Cryptography; Explosions; Inference algorithms; Information security; Lifting equipment; Message authentication; Public key; Software reusability;
Conference_Titel :
Computer Security Foundations Workshop, 1996. Proceedings., 9th IEEE
Conference_Location :
Kenmare
Print_ISBN :
0-8186-7522-5
DOI :
10.1109/CSFW.1996.503691
