O'Reilly logo

The Modelling and Analysis of Security Protocols: the CSP Approach by S. A. Schneider, P. Y.A. Ryan

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

5.1. An example input file

In this section, we give a gentle introduction to the Casper syntax by explaining an example input script, and showing how to use Casper to compile the script into CSP, and then interpret the output from FDR.

Overview of input file

As we have seen in Chapter 4, FDR operates by explicitly enumerating and then exploring the state space of the system in question, and so this method can only be used to check a particular (typically fairly small) system running the protocol, for example, with a single initiator and a single responder, rather than being able to check an arbitrary system with an arbitrary number of initiators and responders; similarly, FDR can only deal with systems where the underlying atomic datatypes ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required