Title :
An interface specification language for automatically analyzing cryptographic protocols
Author :
Brackin, Stephen H.
Author_Institution :
Arca Syst. Inc., Hanscom AFB, MA, USA
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;
Conference_Titel :
Network and Distributed System Security, 1997. Proceedings., 1997 Symposium on
Conference_Location :
San Diego, CA
Print_ISBN :
0-8186-7767-8
DOI :
10.1109/NDSS.1997.579219
