Extending CAPSL for Logic-Based Verifications

摘要

Cryptographic protocols are designed to provide security services, such as key distribution, authentication and non-repudiation, over insecure networks. The design process 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 presents a case study on extending the Common Authentication Protocol Specification Language (CAPSL) to enable it to be used with logic-based formal verification tools for security protocols.