The Modelling and Analysis of Security Protocols: the CSP Approach

You can download the table of contents (postscript, PDF, or text) and the preface to the book (postscript or PDF).

The material in the book is supported by the following tools:

Casper: a protocol to CSP compiler.  If you want to use it you are best off visiting the Casper home page; you can also download the Casper distribution here.

FDR is a model checker for CSP.  In the context of this book, it is used for checking files output from Casper.  You can download a demo copy of FDR which will run the CSP files available on this website.  For licencing and other information, visit the Formal Systems (Europe) Ltd. home page.

PVS is a generic theorem prover.  It has been used to provide mechanical support for verification proofs of protocols.  This work, and the PVS input files, are available here.

RankAnalyser is a prototype tool which provides automated rank function analysis of protocols.  For more information, and distribution files, visit the RankAnalyser home page.

This site also provides the following material:

• There are Casper scripts available for the protocols discussed in the Casper chapter
• Bibliography of security-related publications by the authors and closely related researchers
• Links to CSP-related sites
• Links to Security Related Sites
• Exercises