CVS: a compiler for the analysis of cryptographic protocols
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The Security Process Algebra (SPA) is a CCS-like specification language where actions belong to two different levels of confidentiality. It has been used to define several non-interference-like security properties whose verification has been automatized by means of the tool CoSeC. In recent years, a method for analyzing security protocols using SPA and CoSeC has been developed. Even if it has been useful in analyzing small security protocols, this method has shown to be error-prone as it requires the description by hand of the protocol and of the environment in which it will execute. This problem has been solved by defining a protocol specification language more abstract than SPA, called VSP, and a compiler CVS that generates in an automatic way the SPA specification for a given protocol described in VSP. The VSP/CVS technology is very powerful and its usefulness is shown with the case-study of the Woo-Lam one-way authentication protocol, for which an attack undocumented in the literature is found.Keywords
This publication has 13 references indexed in Scilit:
- Some new attacks upon security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A taxonomy of replay attacks [cryptographic protocols]Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Towards a completeness result for model checking of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Casper: a compiler for the analysis of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Using CSP to detect errors in the TMN protocolIEEE Transactions on Software Engineering, 1997
- The Compositional Security Checker: a tool for the verification of information flow security propertiesIEEE Transactions on Software Engineering, 1997
- A logic of authenticationPublished by Association for Computing Machinery (ACM) ,1989
- Integrating security in a large distributed systemACM Transactions on Computer Systems, 1989
- Efficient and timely mutual authenticationACM SIGOPS Operating Systems Review, 1987
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978