7.2. Secrecy of the shared key: a rank function
As our example, we will consider the description of the Yahalom protocol discussed in Section 3.1, with the Claim_Secret signal inserted. We wish to prove that
This means that for any two users a and b, Secretab(tr) must hold. Hence we can consider for arbitrary A and B the requirement
where Secrecy and SecretAB are defined as in Section 3.2. In other words, if A claims that s is a secret shared with B, and B is honest, then leak.s should not appear in the trace tr.
Thus we aim to show for some ...
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.
