Extending formal security protocol specification languages for use with new verifications techniques

Cryptographic protocols are designed to provide security services, such as key distribution, authentication and non-repudiation, over insecure networks. The verification of cryptographic protocols is highly complex. In particular, the translation from the informal protocol description to the formal protocol specification is an error-prone step, as the exact meaning of the requirements of the security protocol need to be conveyed. This paper discusses the extension of specification languages towards new verification techniques. As a case study, this paper presents an extension of the Common Authentication Protocol Specification Language (CAPSL) to enable it to be used with logic-based formal verification tools for security protocols. Extending an existing language, rather than developing an entirely new specification language, can preserve the virtues of well-established languages. Further, this significantly reduces the effort and time needed to gain a specification language with new features.