A compiler for analyzing cryptographic protocols using noninterference

The Security Process Algebra (SPA) is a CCS-like specification languag e where actions belong to two different levels of confidentiality. It has been used to define several noninterference-like security properties whose verification has been automated by the tool CoSeC. In recent years, a method for...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on software engineering and methodology 2000-10, Vol.9 (4), p.488-528
Main Authors: Durante, Antonio, Focardi, Riccardo, Gorrieri, Roberto
Format: Article
Language:English
Subjects:
Cross-computing tools and techniques
Empirical software validation
Formal methods
Formal software verification
General and reference
Logic
Model checking
Network protocols
Networks
Operational semantics
Process validation
Program semantics
Protocol correctness
Protocol testing and verification
Semantics and reasoning
Software and its engineering
Software creation and management
Software functional properties
Software organization and properties
Software verification and validation
Theory of computation
Validation
Verification by model checking
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The Security Process Algebra (SPA) is a CCS-like specification languag e where actions belong to two different levels of confidentiality. It has been used to define several noninterference-like security properties whose verification has been automated by 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 protocol description and its environment to be written by hand. This problem has been solved by defining a protocol specification language more abstract than SPA, called VSP, and a compiler CVS that automatically generates the SPA specification for a given protocol described in VSP. The VSP/CVS technology is very powerful, and its usefulness is shown with some case studies: the Woo-Lam one-way authentication protocol, for which a new attack to authentication is found, and the Wide Mouthed Frog protocol, where different kinds of attack are detected and analyzed.
ISSN:1049-331X
1557-7392
DOI:10.1145/363516.363532