7.3. Secrecy on nB
We can also consider whether the nonce nB is kept secret if the intruder does not know it. The specification in this case introduces an arbitrary fixed nonce NB into the claimed secret. Agents will claim that both the distributed key and the nonce issued by the responder are secrets. The following is the property to check, for honest agents A and B:
If a claims that NB is a secret, this is in response to receiving it as part of his own run. If b claims it, this is because b issued it.
We separate the protocol runs of the user in order to analyze them separately. We will again use the rules of Figure 7.6 to combine the results ...
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.
