Abstract
In recent years, a method for analyzing security protocols usingthe process algebra CSP (Hoare, 1985) and its model checker FDR(Roscoe, 1994) has been developed. This technique has provedremarkably successful, and has been used to discover a number ofattacks upon protocols. However, the technique has requiredproducing a CSP description of the protocol by hand; thishas proved tedious and error-prone. In this paper we describeCasper, a program that automatically produces the CSP descriptionfrom a more abstract description, thus greatly simplifying themodelling and analysis process.

This publication has 19 references indexed in Scilit: