5.4. Protocol specifications
Casper supports a number of different forms of specification for protocols, some of which we have seen before. The complete list is as follows:
Secret(A, s, [B1, ... ,Bn]) specifies that in any completed run A can expect the value of the variable s to be a secret; B1,... ,Bn are the variables representing the roles with whom the secret is shared. This specification fails if A can complete a run, where none of the roles B1,... ,Bn is legitimately taken by the intruder, but the intruder learns the value A gives to s.
StrongSecret(A, s, [B1,... ,Bn]) is similar to Secret(A, s, [B1,... ,Bn]), except it also includes incomplete runs. Thus, this specification fails if A can take part in a run – complete or not – where none ...
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.
