An interface specification language for automatically analyzing cryptographic protocols

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.