The Modelling and Analysis of Security Protocols: the CSP Approach
Welcome to the web site which accompanies the book
"The Modelling and Analysis
of Security Protocols", published by Pearson Education,
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
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
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.
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):
Site maintained by Steve
Originally posted 13th December 2000; new links added 15th December 2010