Casper: A Compiler for the Analysis of Security Protocols
Casper is a program that will take a description of a security protocol
in a simple, abstract language, and produce a CSP description of the same
protocol, suitable for checking using FDR2. It can be used
either to find attacks upon protocols, or to show that no such attack exists,
subject to the assumptions of the Dolev-Yao Model (i.e. that the intruder may
overhear or intercept messages, decrypt and encrypt messages with keys that he
knows, and fake messages, but not perform any cryptological attacks).
The following will give you some idea of how Casper works:
The Casper distribution can be obtained here, as a gzipped, tarred directory. Details
of installation are available here.
There is also a compiler COSPJ available, that
produces Java implementations of protocols from Casper-like
If you encounter any difficulties, please
get in touch.
Gavin Lowe / Oxford University Computing Laboratory, Parks Road, Oxford, OX1
3QD, UK / firstname.lastname@example.org