7.1. Rank functions
We will provide a number of results based on CSP traces that can be used in protocol verification of secrecy and authentication properties. These properties are concerned with conditions under which particular facts become available to the intruder. In the case of secrecy, we require that a particular fact is never obtained by the intruder. In the case of authentication, we are concerned that a fact (the authenticating event) should only be possible after some other fact (the authenticated event) has already been provided.
In both cases we are therefore concerned to establish that (in particular circumstances) a fact is not available to the intruder. In order to establish this, we will aim to show that all the facts that ...
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.
