3.2. Secrecy
In order to formalize secrecy properties, it is natural to use an event
at the point in a’s run of the protocol with b where we believe the protocol guarantees that Yves cannot obtain the secret value s. It expresses that expectation that the intruder cannot be in possession of s. It may be understood to mean: ‘The value s used in the run apparently between a and b initiated by a should be secret for the entire protocol run’. For example, the Yahalom protocol aims to ensure that the key kab received by a in the third message is secret. This expectation is expressed by introducing the signal message into the description of the general ...
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.
