University of Oxford Logo University of OxfordDepartment of Computer Science - Home
On Facebook
Facebook
Follow us on twitter
Twitter
Linked in
Linked in
Flickr
Flickr
Google plus
Google plus
Digg
Digg
Pinterest
Pinterest
Stumble Upon
Stumble Upon

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 FDR3. 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.

There is also a compiler COSPJ available, that produces Java implementations of protocols from Casper-like descriptions.

If you encounter any difficulties, please get in touch.


Gavin Lowe / Department of Computer Science, University of Oxford, Parks Road, Oxford, OX1 3QD, UK / gavin.lowe@cs.ox.ac.uk