An interface specification language for automatically analyzing cryptographic protocols

Author

Brackin, Stephen H.

Author_Institution

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

fYear

1997

fDate

10-11 Feb 1997

Firstpage

40

Lastpage

51

Abstract

This paper describes a simple interface specification language (ISL) for cryptographic protocols and their desired properties, and an automatic authentication protocol analyzer (AAPA) that automatically either proves-using an extension of the Gong, Needham, Yahalom (1990) belief logic-that specified protocols have their desired properties, or identifies precisely where these proof attempts fail. The ISL and the AAPA make it easy for protocol designers to incorporate formal analysis into the protocol design process, where they clarify designs and reveals a large class of common errors. The ISL and the AAPA have already shown potential deficiencies in published protocols and been useful in designing new protocols

Keywords

cryptography; formal logic; formal specification; protocols; specification languages; automatic authentication protocol analyzer; belief logic; cryptographic protocols; formal analysis; interface specification language; network security; protocol design; secure communications; Authentication; Automatic logic units; Cryptographic protocols; Cryptography; Failure analysis; Information security; Memory management; Process design; Software reusability; Specification languages;

fLanguage

English

Publisher

ieee

Conference_Titel

Network and Distributed System Security, 1997. Proceedings., 1997 Symposium on

Conference_Location

San Diego, CA

Print_ISBN

0-8186-7767-8

Type

conf

DOI

10.1109/NDSS.1997.579219

Filename

579219