6.1. CSP from Casper
As we have seen in Chapter 2, it is reasonably straightforward to encode the trustworthy principals involved in an execution of a crypto-protocol. Leaving aside the intruder until Section 6.2, the more complicated issues arise in keeping the data involved both finite and manageably sized.
The recursive datatype fact [1] described in Chapter 2 is naturally infinite. FDR is quite happy to accept such definitions, and even channels that can carry any value of the type; but it does require that inputs be constrained to offer finite choices and equally that synchronization sets be finite. In practice, typically, both the time to explore the system and the fixed space needed to hold the representation of the transition system ...
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.
