Chapter 5. Casper
In previous chapters we have seen how to produce CSP descriptions of security protocols, and how to analyze them using FDR. However, producing the CSP by hand is a rather time-consuming and error-prone process. We have therefore produced a compiler, called Casper, to help produce the CSP description. The user produces an input script – typically only about one page long – describing the protocol, in an abstract notation similar to that used to describe protocols earlier; Casper compiles this into CSP code, suitable for checking using FDR.
In this chapter, we give an overview of Casper, and how to use it to model protocols and different protocol features. The intricacies of the FDR encoding will be discussed in more detail in ...
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.
