A HOL extension of GNY for automatically analyzing cryptographic protocols

Author

Brackin, Stephen H.

Author_Institution

Arca Syst. Inc., Hanscom AFB, MA, USA

fYear

1996

fDate

10-12 Jun 1996

Firstpage

62

Lastpage

76

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Security Foundations Workshop, 1996. Proceedings., 9th IEEE

Conference_Location

Kenmare

ISSN

1063-6900

Print_ISBN

0-8186-7522-5

Type

conf

DOI

10.1109/CSFW.1996.503691

Filename

503691