The Modelling and Analysis of Security Protocols: the CSP Approach

From December 2010 an online version of the book has been made available for personal reference. It is also available for purchase from sites such as Amazon.com and Amazon.co.uk.

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 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 now hosted by Bruno Dutertre.

This site also provides the following material (not maintained since December 2000):

• 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