Casper: A compiler for the analysis of security protocols

Article type: Research Article

Authors: Lowe, Gavin

Affiliations: Department of Mathematics and Computer Science, University of Leicester, University Road, Leicester LE1 7RH, UK. E-mail: gavin.lowe@mcs.le.ac.uk

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.

DOI: 10.3233/JCS-1998-61-204

Journal: Journal of Computer Security, vol. 6, no. 1-2, pp. 53-84, 1998