Home > Articles > Security > Network Security

  • Print
  • + Share This
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.na.nb.kab in b’s run would be appropriate to mean that

Agent b has completed a protocol run apparently with a, and with nonces nb, na, and with key kab.

A corresponding event Running.a.b.na.nb.kab would be used to denote that

Agent a is following a protocol run with b, with nonces na, nb, and with key kab.

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.

03fig20.gifFigure 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 m2 is intended to provide an assurance that A transmitted m1 earlier in the protocol.

03fig21.gifFigure 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 na and nb, and a key kab 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.na.nb.kab and it should follow an event signal.Running_Initiator.a.b.na.nb.kab 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 aHonest.

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 kab) 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:


03fig27.gifFigure 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.na.nb.kab 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.na.nb, with no mention of the key.

03fig28.gifFigure 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 kab, then signal.Commit_Responder.b.a.na.nb.kab simply needs to authenticate that there are some nonces n and n′ such that signal.Running_Initiator.a.b.n.n′.kab 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 kab 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 dsa in its Commit signal, and b has corresponding data dsb in its running signal, then we can define


    We will write dsadsb to state that the information in the signals dsa and dsb 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:




We focus attention only on authentication of honest users to and by each other, in the same way as the conditions that aHonest and bHonest 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 dsa or dsb often contains nonces, and so typically the bound n will be 1, since different runs of the protocol should make use of different nonces.

  • + Share This
  • 🔖 Save To Your Account

InformIT Promotional Mailings & Special Offers

I would like to receive exclusive offers and hear about products from InformIT and its family of brands. I can unsubscribe at any time.


Pearson Education, Inc., 221 River Street, Hoboken, New Jersey 07030, (Pearson) presents this site to provide information about products and services that can be purchased through this site.

This privacy notice provides an overview of our commitment to privacy and describes how we collect, protect, use and share personal information collected through this site. Please note that other Pearson websites and online products and services have their own separate privacy policies.

Collection and Use of Information

To conduct business and deliver products and services, Pearson collects and uses personal information in several ways in connection with this site, including:

Questions and Inquiries

For inquiries and questions, we collect the inquiry or question, together with name, contact details (email address, phone number and mailing address) and any other additional information voluntarily submitted to us through a Contact Us form or an email. We use this information to address the inquiry and respond to the question.

Online Store

For orders and purchases placed through our online store on this site, we collect order details, name, institution name and address (if applicable), email address, phone number, shipping and billing addresses, credit/debit card information, shipping options and any instructions. We use this information to complete transactions, fulfill orders, communicate with individuals placing orders or visiting the online store, and for related purposes.


Pearson may offer opportunities to provide feedback or participate in surveys, including surveys evaluating Pearson products, services or sites. Participation is voluntary. Pearson collects information requested in the survey questions and uses the information to evaluate, support, maintain and improve products, services or sites, develop new products and services, conduct educational research and for other purposes specified in the survey.

Contests and Drawings

Occasionally, we may sponsor a contest or drawing. Participation is optional. Pearson collects name, contact information and other information specified on the entry form for the contest or drawing to conduct the contest or drawing. Pearson may collect additional personal information from the winners of a contest or drawing in order to award the prize and for tax reporting purposes, as required by law.


If you have elected to receive email newsletters or promotional mailings and special offers but want to unsubscribe, simply email information@informit.com.

Service Announcements

On rare occasions it is necessary to send out a strictly service related announcement. For instance, if our service is temporarily suspended for maintenance we might send users an email. Generally, users may not opt-out of these communications, though they can deactivate their account information. However, these communications are not promotional in nature.

Customer Service

We communicate with users on a regular basis to provide requested services and in regard to issues relating to their account we reply via email or phone in accordance with the users' wishes when a user submits their information through our Contact Us form.

Other Collection and Use of Information

Application and System Logs

Pearson automatically collects log data to help ensure the delivery, availability and security of this site. Log data may include technical information about how a user or visitor connected to this site, such as browser type, type of computer/device, operating system, internet service provider and IP address. We use this information for support purposes and to monitor the health of the site, identify problems, improve service, detect unauthorized access and fraudulent activity, prevent and respond to security incidents and appropriately scale computing resources.

Web Analytics

Pearson may use third party web trend analytical services, including Google Analytics, to collect visitor information, such as IP addresses, browser types, referring pages, pages visited and time spent on a particular site. While these analytical services collect and report information on an anonymous basis, they may use cookies to gather web trend information. The information gathered may enable Pearson (but not the third party web trend services) to link information with application and system log data. Pearson uses this information for system administration and to identify problems, improve service, detect unauthorized access and fraudulent activity, prevent and respond to security incidents, appropriately scale computing resources and otherwise support and deliver this site and its services.

Cookies and Related Technologies

This site uses cookies and similar technologies to personalize content, measure traffic patterns, control security, track use and access of information on this site, and provide interest-based messages and advertising. Users can manage and block the use of cookies through their browser. Disabling or blocking certain cookies may limit the functionality of this site.

Do Not Track

This site currently does not respond to Do Not Track signals.


Pearson uses appropriate physical, administrative and technical security measures to protect personal information from unauthorized access, use and disclosure.


This site is not directed to children under the age of 13.


Pearson may send or direct marketing communications to users, provided that

  • Pearson will not use personal information collected or processed as a K-12 school service provider for the purpose of directed or targeted advertising.
  • Such marketing is consistent with applicable law and Pearson's legal obligations.
  • Pearson will not knowingly direct or send marketing communications to an individual who has expressed a preference not to receive marketing.
  • Where required by applicable law, express or implied consent to marketing exists and has not been withdrawn.

Pearson may provide personal information to a third party service provider on a restricted basis to provide marketing solely on behalf of Pearson or an affiliate or customer for whom Pearson is a service provider. Marketing preferences may be changed at any time.

Correcting/Updating Personal Information

If a user's personally identifiable information changes (such as your postal address or email address), we provide a way to correct or update that user's personal data provided to us. This can be done on the Account page. If a user no longer desires our service and desires to delete his or her account, please contact us at customer-service@informit.com and we will process the deletion of a user's account.


Users can always make an informed choice as to whether they should proceed with certain services offered by InformIT. If you choose to remove yourself from our mailing list(s) simply visit the following page and uncheck any communication you no longer want to receive: www.informit.com/u.aspx.

Sale of Personal Information

Pearson does not rent or sell personal information in exchange for any payment of money.

While Pearson does not sell personal information, as defined in Nevada law, Nevada residents may email a request for no sale of their personal information to NevadaDesignatedRequest@pearson.com.

Supplemental Privacy Statement for California Residents

California residents should read our Supplemental privacy statement for California residents in conjunction with this Privacy Notice. The Supplemental privacy statement for California residents explains Pearson's commitment to comply with California law and applies to personal information of California residents collected in connection with this site and the Services.

Sharing and Disclosure

Pearson may disclose personal information, as follows:

  • As required by law.
  • With the consent of the individual (or their parent, if the individual is a minor)
  • In response to a subpoena, court order or legal process, to the extent permitted or required by law
  • To protect the security and safety of individuals, data, assets and systems, consistent with applicable law
  • In connection the sale, joint venture or other transfer of some or all of its company or assets, subject to the provisions of this Privacy Notice
  • To investigate or address actual or suspected fraud or other illegal activities
  • To exercise its legal rights, including enforcement of the Terms of Use for this site or another contract
  • To affiliated Pearson companies and other companies and organizations who perform work for Pearson and are obligated to protect the privacy of personal information consistent with this Privacy Notice
  • To a school, organization, company or government agency, where Pearson collects or processes the personal information in a school setting or on behalf of such organization, company or government agency.


This web site contains links to other sites. Please be aware that we are not responsible for the privacy practices of such other sites. We encourage our users to be aware when they leave our site and to read the privacy statements of each and every web site that collects Personal Information. This privacy statement applies solely to information collected by this web site.

Requests and Contact

Please contact us about this Privacy Notice or if you have any requests or questions relating to the privacy of your personal information.

Changes to this Privacy Notice

We may revise this Privacy Notice through an updated posting. We will identify the effective date of the revision in the posting. Often, updates are made to provide greater clarity or to comply with changes in regulatory requirements. If the updates involve material changes to the collection, protection, use or disclosure of Personal Information, Pearson will provide notice of the change through a conspicuous notice on this site or other appropriate way. Continued use of the site after the effective date of a posted revision evidences acceptance. Please contact us if you have questions or concerns about the Privacy Notice or any objection to any revisions.

Last Update: November 17, 2020