Title :
CVS: a compiler for the analysis of cryptographic protocols
Author :
Durante, Antonio ; Focardi, Riccardo ; Gorrieri, Roberto
Author_Institution :
Dipartimento di Sci. dell´´Inf., Bologna Univ., Italy
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 :
calculus of communicating systems; cryptography; data privacy; message authentication; process algebra; program compilers; protocols; specification languages; CCS; CVS compiler; CoSeC; SPA; Security Process Algebra; VSP; cryptographic protocols; data confidentiality; one-way authentication protocol; specification language; Algebra; Authentication; Computer security; Cryptographic protocols; ISO standards; Interference; Public key; Public key cryptography; Specification languages;
Conference_Titel :
Computer Security Foundations Workshop, 1999. Proceedings of the 12th IEEE
Conference_Location :
Mordano
Print_ISBN :
0-7695-0201-6
DOI :
10.1109/CSFW.1999.779774
