Goals in Algebraic Analysis

The most widely used alternative to using logic for analysis of cryptographic protocols is to specify them in an `algebraic' specification language and perform analysis of the states reached, particularly by an attacker. Several research efforts have been made in this direction [15,24,27].

The NRL Protocol Analyzer [19] is a software tool implementing one such approach. Syverson and Meadows [31] have considered methods to specify formal requirements for the protocols which are analysed using the NRL Protocol Analyzer, rather than simply looking for specific flaws such as compromised keys. They specify slightly different goals for different protocol architectures, in particular differentiating between server based key distribution and key agreement protocols. The three requirements for the two party/one server key distribution protocols, in their informal versions, are as follows.

SM1

If a key is accepted, it should not be learned by the intruder, except through a compromise event.

SM2

If a key is accepted for communication between two parties, it should not have been accepted in the past, except by the other party.

SM3

If a key is accepted for communication between two entities, then it must have been requested by the initiating entity and sent by the server for a communication between those two entitites.

SM1 and SM2 are extensional and correspond closely to SVO3 and SVO5. SM3, however, is intensional and places restrictions on the protocol format; for example it precludes the possibility that one of the two users generates the session key, or that the responder alone contacts the server.

Syverson and Meadows also provide requirements for the case of key agreement between two users without the help of a server. These requirements are also partly extensional and partly intensional. In an extension of their work they also consider requirements for re-authentication of a key [31]; as might be expected, these involve different properties from those relevant for new session keys.

Another method for algebraic analysis uses CSP specifications together with a tool called FDR [24]. Lowe has used this technique to derive a variety of new protocol attacks and recently has considered what are the possible goals for authentication protocols [18]. These all concern properties provided to an initiator A communicating with a responder B .

Low1: Aliveness

Whenever A completes a run of the protocol, apparently with B , then B has previously been running the protocol.

Low2: Weak Agreement

Whenever A completes a run of the protocol, apparently with responder B , then B has previously been running the protocol, apparently with A .

Low3: Non-injective Agreement

on a set of data items ds . Whenever A completes a run of the protocol, apparently with B , then B has previously been running the protocol, apparently with A , and B was acting as responder in his run, and the two agents agree on the data values corresponding to all the variables in ds .

Low4: Agreement

on a set of data items ds . Whenever A completes a run of the protocol, apparently with responder B , then B has previously been running the protocol, apparently with A , and B was acting as responder in his run, and the two agents agreed on the data values corresponding to all the variables in ds and each such run of A corresponds to a unique run of B .

It can be seen that each property is stricter than the previous one. Lowe also provides formal versions in CSP for which he shows that the hierarchy holds formally. All the properties are intensional. Take for example Low1; this is different from SVO1 because it demands that the responder is engaged in the same protocol as the initiator, rather than that a value is returned as in SVO1. Low1 does not provide assurance that B has responded recently, so it provides liveness at some time, rather than the liveness `now' of SVO1. However Lowe does discuss how to extend the properties to include recentness.

Another approach using CSP has been made by Schneider [27]. He enumerated nine different `flavours' of authentication in his analysis of the well-known Needham-Schroeder public key protocol [21]. These fascinatingly subtle variations reveal the microscopic detail with which protocol goals may be differentiated. Each property relates matters such as who initiated the run, whether a nonce is associated with a specific party, or whether a nonce was received by a specific party. All the properties are intensional.

There have been a number of other algebraic analysis techniques proposed. It has recently been recognised that, in order to ensure that the same protocol specified by a designer is presented to different analysis tools in a uniform way, there should be some standard method for presenting protocol specifications that includes all the information required by each tool. To this end Millen has initiated a Common Authentication Protocols Specification Language (CAPSL) [20] which does just this. A CAPSL specification consists of a number of sections concerning different protocol elements. One of these is a section on protocol assumptions and goals.

A CAPSL protocol specifier is free to choose the protocol goals within what may be expressed in the language. This requires use of a set of keywords, principally BELIEVES, HOLDS, KNOWS and SECRET. For examples, a goal might be that the session key K is secret to certain principals, or that a principal believes that another principal holds K . These are extensional goals. At present CAPSL only appears to have the ability to specify goals concerning key establishment and not entity authentication.