This chapter is from the book
This chapter is from the book
This chapter is from the book
3.6 Summary
This chapter has considered how authentication and secrecy properties can be captured by enhancing CSP descriptions of protocols with the introduction of ‘specification events’ into the descriptions of honest agents. These events do not affect the interactions between the components of the protocol, and so they do not change the attacks that are possible on a protocol. They allow the intentions of the protocol designer or specifier to be expressed explicitly in terms of what should have been achieved when a protocol participant reaches a particular state. Requirements on protocols are captured by the introduction of appropriate specification events at particular points of the CSP protocol description, and then by describing the requirements on these events.
If Claim_Secret signals are introduced into the CSP description only for runs with honest protocols, then secrecy requirements on protocols tend to take the form
)
so that when an honest agent a claims that s is a secret value, then the intruder should not be in possession of it – leak.s can occur only when the intruder has s.
Alternatively, the assumption that the agents are honest might be captured more explicitly within the property, as the fact that a ∊ Honest b ∊ Honest.
)
In this case, the signal event is always possible at the end of the protocol run, and the requirement is that only in the appropriate cases should this be taken to indicate secrecy of s.
These secrecy properties can also both be expressed as process-oriented specifications, enabling model-checking.
Authentication properties are expressed in terms of the relationship between a Commit signal and a Running signal: that the performance of a Commit signal by one agent must guarantee that the other agent has already performed a corresponding Running signal, such as in the following property:
)
The Commit signal is introduced into the protocol description at the point where the protocol designer expects the protocol to have achieved authentication for that agent of the other party. It is required to correspond to the other party having reached a particular stage in their part of the protocol. Although the other party need not have committed, they should at least have done something, and so the Running signal is introduced to mark the point they must have reached. Early approaches to authentication and secrecy [84, 61, 86, 57] expressed properties on the bare protocols without the introduction of signal events. The approach favoured in this book prefers signal events to enable clearer expression of the properties required.
We have also considered non-repudiation properties [44], where evidence is introduced; and anonymity, where we require that permutations of the agents requiring anonymity does not affect the visible parts of the system. These approaches were first presented in [88] and [85]. The full Zhou-Gollmann non-repudiation protocol is described in [102]. The dining cryptographers example was first described in [21].