Title :
Casper: a compiler for the analysis of security protocols
Author_Institution :
Dept. of Math. & Comput. Sci., Leicester Univ., UK
Abstract :
In recent years, a method for analyzing security protocols using the process algebra CSP (C.A.R. Hoare, 1985) and its model checker FDR (A.W Roscoe, 1994) has been developed. This technique has proved successful, and has been used to discover a number of attacks upon protocols. However the technique has required producing a CSP description of the protocol by hand; this has proved tedious and error prone. We describe Casper, a program that automatically produces the CSP description from a more abstract description, thus greatly simplifying the modelling and analysis process
Keywords :
communicating sequential processes; cryptography; message authentication; program compilers; protocols; CSP description; Casper compiler; abstract description; model checker FDR; process algebra CSP; security protocol analysis; Algebra; Authentication; Computer science; Control systems; Information security; Mathematics; Performance evaluation; Protocols; State-space methods; System testing;
Conference_Titel :
Computer Security Foundations Workshop, 1997. Proceedings., 10th
Conference_Location :
Rockport, MA
Print_ISBN :
0-8186-7990-5
DOI :
10.1109/CSFW.1997.596779
