5.6. Summary
This chapter has introduced the protocol compiler Casper, and shown how it can be used to model security protocols and produce scripts for analysis in FDR with respect to a variety of secrecy and authentication properties.
Casper, and all the scripts used in this chapter, can be obtained from this book’s web page.
Casper was first described in [56] and in [58], although the Casper input language has evolved since those papers. A report on a number of case studies carried out using Casper and FDR appears in [26]. A recent extension to Casper, to include support for the data independence techniques discussed in Chapter 10, appears in [13].
The Kehne-Langendörfer-Schönwälder protocol of Section 5.2 first appeared in [46]; attacks upon ...
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.
