6.6. Specifying desired properties
The claims from the ‘specification’ part of the Casper description of the protocol give rise to assertions in the CSP script. These are in terms of processes over the signal and leak channels and a view of the system in which all other events have been renamed (to yield the appropriate signals) or hidden. The channel signal is defined to carry the types of information needed by the specification processes:
datatype Signal = Claim_Secret.ALL_PRINCIPALS.ALL_SECRETS.Set(ALL_PRINCIPALS) | Running1.ROLE.ALL_PRINCIPALS.ALL_PRINCIPALS.Nonce.Nonce | Commit1.ROLE.ALL_PRINCIPALS.ALL_PRINCIPALS.Nonce.Nonce | Running2.ROLE.ALL_PRINCIPALS.ALL_PRINCIPALS.SessionKey | Commit2.ROLE.ALL_PRINCIPALS.ALL_PRINCIPALS.SessionKey ...
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.
