Various logics have been used successfully for analysis of cryptographic protocols. The first of these was the logic of Burrows, Abadi and Needham, the BAN logic [10]. An analysis of a protocol using the BAN logic results in a set of beliefs of each protocol principal and goals may be expressed as the desired final beliefs. In principle it is not necessary to know the protocol goals in order to perform such an analysis; indeed one of the strengths of a logical analysis is the ability to discover subtly differing final beliefs of the principals. However, the authors of the BAN logic do suggest what may be typical protocol goals. The first is as follows, where A and B are principals who wish to use a new key K . (The goal may be expressed in the formalism of the logic but that need not concern us here.)
This is an extensional goal which is essentially identical to Gollman's Gol1. (Although being a `good' key is an atomic construct, its semantics are that the key will never be discovered by others. Furthermore only keys that are fresh are ever promoted to being believed good.) Normally B would also be expected to establish a symmetrical belief. Principals in a BAN logic analysis can possess beliefs about beliefs and the other typical goal put forward is such a second order belief.
Again this is an extensional goal concerned solely with key establishment. No general goals about entity authentication are discussed, but in the course of analysis of several protocols the BAN authors obtain certain properties that might have been termed protocol goals. For example they show that some protocols reveal that a certain principal is `alive' because that principal has sent a message recently. We will expand on this idea later.
Numerous enhancements and alternatives to the BAN logic have been published. The logic of Syverson and van Oorschot, SVO logic [28,29], aims to unify a number of previous logics including BAN. The authors identify what they term six `Generic Formal Goals'. These are expressed in English below; for formal statements readers should refer to the papers.
There are clearly dependencies between various of these goals. Furthermore, it is not clear why these particular goals are important; for example it might be questioned whether Secure Key Establishment is useful without Key Freshness. To be fair to the authors they state that it is not intended as a ``definitive list of the goals that a key agreement or key distribution protocol should meet''.
Secure Key Establishment, SVO3, is an extensional goal essentially the same as BAN1 and Gol1. SVO4 and SVO6 are also extensional. SVO1 and SVO2, however, are intensional goals because they are concerned with particular message flows. Below the goal SVO1 (`liveness') will be presented as an extensional goal in the absence of the particular requirement that a message has recently been uttered by B .