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 ...
Get The Modelling and Analysis of Security Protocols: the CSP Approach now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
