Expressing Security Protocol Goals

This chapter is from the book 

3.3 Authentication

Entity authentication is concerned with verification of an entity’s claimed identity. An authentication protocol provides an agent b with a mechanism to achieve this: an exchange of messages that establishes that the other party a has also been involved in the protocol run. This provides authentication of a to b: an assurance is provided to b that some communication has occurred with a.

Signal Commit.b.a events will be introduced into the description of b’s run of the protocol to mark the point at which authentication of a to b is taken to have been achieved. Occurrence of Commit.b.a in b’s protocol run means simply that

Agent b has completed a protocol run apparently with a.

Events of the form Running.a.b in a’s run of the protocol are introduced to mark the point that should have been reached by the time b performs the Commit.b.a event. Occurrence of Running.a.b in a’s protocol run means simply that

Agent a is following a protocol run apparently with b.

If a Running.a.b event must always have occurred by the time the Commit.b.a event is performed, then authentication is achieved. Further information ds associated with the protocol run, such as the values of nonces or keys, is also included as components of the Commit and Running events. For example, in the Yahalom protocol, there are two nonces and a key associated with any particular run. An event Commit.b.a.n_a.n_b.k_ab in b’s run would be appropriate to mean that

Agent b has completed a protocol run apparently with a, and with nonces n_b, n_a, and with key k_ab.

A corresponding event Running.a.b.n_a.n_b.k_ab would be used to denote that

Agent a is following a protocol run with b, with nonces n_a, n_b, and with key k_ab.

The details to include will depend on the protocol (in terms of what data will be associated with particular protocol runs) and also on the point at which the events are introduced (since only some of the information might be available at particular points during the protocol).

This pattern is a scheme for authentication properties, but it allows the different flavours of authentication to be expressed by introducing different requirements on the correspondence between the Commit and Running events within this scheme:

1. One agent b might require simply that the other agent a is alive and has not failed. This is ensured if Commit.b.a.ds provides evidence simply that a has participated in some recent communication: an occurrence of Running.a.c.ds′ with any c and any data ds′ will suffice.

2. Agent b might require authentication that a participated in a run in which a took b to be the other participant. In this case, occurrence of the event Commit.b.a.ds will guarantee that Running.a.b.ds′ occurred previously, though the information ds and ds′ need not be the same.

3. Agents a and b might further be required to agree on the additional information ds specific to the particular run. This will authenticate to b that a was involved in that particular run.

Some protocols aim to provide authentication for each of the parties: that each party receives an assurance about the identity of the other. The Yahalom protocol is one such example: it aims to provide to each of the parties involved some assurance about the identity of the other. In this case, two properties will need to be specified: authentication of the initiator to the responder, and authentication of the responder to the initiator. Thus each party will introduce a Commit event to indicate when it has reached the point where authentication is claimed, and a Running signal to correspond to the other party’s Commit signal. The Commit signal will usually be inserted at the end of the protocol run, since authentication is generally considered to have been achieved when the run is completed. The corresponding Running signal will usually be inserted either right at the beginning of the corresponding protocol to verify that the other party began a corresponding run; or just before the last message sent out by the agent that precedes the Commit, which is the latest possible point that can potentially be guaranteed by the protocol. Within the context of the protocol, this provides the strongest possible information about the progress that has been made.

Figure 3.4 illustrates the general situation where B commits to the run with A after receipt of message m which should be sent by A. In this case the Running signal should be inserted into the description of A’s run at some point before m is transmitted, and it can be at the point immediately before. If the occurrence of Commit really does guarantee that the corresponding Running signal must previously have occurred, then B’s receipt of message m must guarantee that A transmitted it. To see this, consider the contrapositive: if B can receive m without A having sent it (perhaps because an attack on the protocol is possible), then B can receive m without A having performed the Running signal (since the performance of that signal affects nothing that B can do), and so B can then perform Commit without A having performed the corresponding Running signal.

Figure 3.4. Placing signals into a protocol

In general, when there are more than two parties involved in the protocol, one of the parties other than A might have been involved in the transmission of m.In this case, the Running signal will need to be inserted at a point in A’s run at a point causally prior to the Commit signal. Figure 3.5 illustrates a situation in which B’s receipt of message m₂ is intended to provide an assurance that A transmitted m₁ earlier in the protocol.

Figure 3.5. Placing signals into a protocol

Authentication for the initiator of a protocol run will establish that the responder has reached a particular point in his run of the protocol. Conversely, authentication for the responder will establish that the initiator has reached a (different) particular point in his run. It is therefore appropriate to distinguish commitment of the initiator from commitment of the responder by introducing the events signal.Commit_Initiator.a.b and signal.Commit_Responder.b.a, and the Running events signal.Running_Responder.b.a and signal.Running Initiator.a.b which correspond. Authentication (of type (2) above) for the initiator will then be expressed by the requirement that whenever signal.Commit Initiator.a.b is performed for honest agent b, then b must previously have performed signal.Running_Responder.b.a, signalling that he is engaged in a run of the protocol with a, in the role of responder, and that he has reached the particular point specified.

Authentication for the responder is described in a similar way: that the signal signal.Commit_Responder.b.a must be preceded by signal.Running_Initiator.a.b.

Trace specification

The requirement that one kind of event e should precede another d is easy to express as a trace specification: that whenever d appears in the trace then e must appear beforehand:

This states that if tr′^<d>is a prefix of the trace tr, then e should appear in tr′ – the part of the trace before d. To make its relationship to authentication explicit, we will abbreviate this specification as

to state that the occurrence of d in tr guarantees that e has previously appeared in tr.

In fact this specification is equivalent on processes to the specification

because the set of traces corresponding to any system must be prefix closed: if a sequence of events is a trace, then so too are all of its prefixes. This means that the prefix ending in d must be a trace, and hence must also contain e; and so e must appear before d in the trace.

In the context of authentication, we require that if Commit appears in the trace, then a corresponding Running event must also be present: authentication has the general form Running precedes Commit.

Yahalom: authentication of initiator by responder

A run of the Yahalom protocol between a and b involves two nonces n_a and n_b, and a key k_ab that is obtained by each party. We will first consider the protocol from the point of view of the responder. If agreement is required on some or all of this information, (as in authentication of type (3) above) then the signal event at the end of the responder’s run should be signal.Commit_Responder.b.a.n_a.n_b.k_ab and it should follow an event signal.Running_Initiator.a.b.n_a.n_b.k_ab in the initiator’s run.

The authentication property of initiator by responder will require that

Since the intruder does not provide signals (even when following the protocol), we can only guarantee that the corresponding Running signal has occurred provided we assume that the initiator is honest: that a ∊ Honest.

We must decide where to place these authenticating signals in the CSP descriptions of the protocol. Figure 3.6 contains a message sequence chart of the protocol. It shows that the responder is not even in possession of all the information (and in particular k_ab) until receipt of the last message, so the only possible place for the commit message is right at the end of the protocol. Similarly, the initiator is not in possession of all the information until just before its final message, so the Running signal should either precede or follow that message. However, it must causally precede the responder’s Commit message, and so it must be inserted before transmission of the final message. Thus we obtain the following enhanced descriptions of the protocol:

Figure 3.6. Authentication for the responder in the Yahalom protocol

Yahalom: authentication of responder by initiator

Since the Yahalom protocol aims to establish authentication in both directions, we must also introduce signals to describe the initiator authenticating the responder. The first attempt at this will insert the event signal.Commit_Initiator.a.b.n_a.n_b.k_ab at the end of the initiator’s run. Then authentication will require that the occurrence of such an event confirms earlier performance of the corresponding responder Running event with the same information. However, there is a local difficulty with this. Examination of the protocol in Figure 3.7 reveals that the last message sent by b is the second message of the protocol, so the Running signal must be inserted before that. By this stage, the two nonces have been provided to b, but the key to be issued in message 3 cannot be known at that time to agent b. Thus the signal to introduce can be at most Running_Responder.b.a.n_a.n_b, with no mention of the key.

Figure 3.7. Authentication of the responder by the initiator in the Yahalom protocol

On reflection this situation is expected. The protocol does not provide any guarantees to a that b ever obtains the key. The last message between a and b could be intercepted after a has finished the protocol run, and no earlier messages to b contain the key. The protocol does ensure that if b accepts a key, then it must be the same key that a has accepted (since the key in b’s Commit matches the key in a’s Running); but a has a weaker authentication than b, since a can never confirm that b did indeed accept the key.

The strongest authentication property for authenticating the responder to the initiator is the following:

Provided the other agent b is honest, any commitment should establish that a corresponding Running event has previously occurred. This assurance is independent of the key that the initiator has committed to, but it does require agreement on the nonces.

This requirement can be expressed and the points at which the Commit event is inserted into the protocol specifies the stage at which a is provided with a guarantee about the fact that b has reached the corresponding stage.

The CSP description of the protocol is decorated as follows:

Weaker authentication

In fact weaker authentication requirements can be expressed by relaxing the correspondence between Commit and Running signals, so that they do not need to agree on all of their information. For example, if b only requires evidence that a has been running the protocol with him and that they agree on the key k_ab, then signal.Commit_Responder.b.a.n_a.n_b.k_ab simply needs to authenticate that there are some nonces n and n′ such that signal.Running_Initiator.a.b.n.n′.k_ab must previously have occurred. Alternatively, this expresses that some element of

must have occurred.

This leads to a generalization of the authentication trace property: that if some element of a set D of events has appeared in a trace tr, then this provides a guarantee that some element of some other set E has previously appeared in tr. In this case we say that E precedes D, defined as follows:

This states that if some prefix of tr finishes with some event from D, then there must be some event from E already in that prefix (i.e. the projection of tr′ on to E is not empty). When D and E are singleton sets then the set brackets may be elided to obtain the notation introduced earlier for authentication between events.

If b requires authentication with regard to the key but not the nonces, then the requirement is captured as the trace specification

The requirement authenticating the responder to the initiator, where the value of the key k_ab is ignored, can also be expressed as follows:

Process-oriented specification

Signal events can also be used to specify authentication requirements in a process-oriented way.

We can capture the requirement that d authenticates e by providing a specification process in which d can occur only if the e has previously occurred:

More generally, if the set D authenticates the set E, then we require that some element from E must occur before any element of D. This generalizes the process Precedes as follows:

Then the various flavours of authentication can be given as particular instances of these processes:

• If a as initiator is to authenticate b as responder, where a has particular data ds_a in its Commit signal, and b has corresponding data ds_b in its running signal, then we can define

  

  
  

  We will write ds_a ↔ ds_b to state that the information in the signals ds_a and ds_b correspond.

• Similarly, a definition can be given for b as responder authenticating a as initiator:

  

  
  

If we want to specify that all initiators are correctly authenticating honest responders, we can combine several copies of the above specification together:

And similarly for the responders:

And we can test whether the appropriate restriction of the system refines this specification:

where

We focus attention only on authentication of honest users to and by each other, in the same way as the conditions that a ∊ Honest and b ∊ Honest restricted the specification only to honest users. The intruder does not perform signal events (and could not be relied upon to, even if they were available to him) and so it is inappropriate to try to authenticate that these have occurred.

Duplicate runs

The above specifications allow b to complete several runs of the protocol for only a single run of a. In some instances (for example, financial transactions) a stronger requirement might be appropriate, that different occurrences of Commit events correspond to different occurrences of Running events. One can specify a one-one correspondence between the runs with the additional requirement that

This states that the number of responder Commit signals with respect to the information in any run must be no greater than the number of initiator Running signals – in other words, that there cannot be more protocol runs completing than starting. This additional requirement is called injective authentication, in contrast to non-injective authentication which requires only that completion of a run indicates that there is some corresponding start to the run.

Injective authentication can also be captured as a process-oriented specification as follows:

However, the above process is infinite state, so would be impractical for model-checking purposes. In this case, if there is some bound n on the number of runs a can perform, then one can use a specification like the following:

The data ds_a or ds_b often contains nonces, and so typically the bound n will be 1, since different runs of the protocol should make use of different nonces.