Abstract
In recent years, a method for analyzing security protocols using the process algebra CSP (Hoare, 1985) and its model checker FDR (Roscoe, 1994) has been developed. This technique has proved remarkably 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. In this paper we describe Casper, a program that automatically produces the CSP description from a more abstract description, thus greatly simplifying the modelling and analysis process.
Get full access to this article
View all access options for this article.