Analysis of Authentication Protocols

When using belief logics for protocol validation, the typical approach has been to establish a set of premises or preconditions; generate beliefs by using the steps of the protocol and the belief logic [BAN89, GNY90, SvO94, SvO96]. Although the exact format of the protocol and the rules of the logic may differ, the approach is basically the same. In Syverson and van Oorschot's most recent paper [SvO96] they present a set of common premises and postconditions that can be used in protocol analysis. In addition, the suggest adding premises for all messages such that upon receipt of a message with uncomprehended component, we can assign a meaning to some of those components -- this is in lieu of protocol idealization which was used in earlier papers, and sometimes resulted in unintentional modification of the semantics of the protocol. There are several issues in the standard approach which need to be considered.

• Premises. All proofs require a set of premises/preconditions that must hold prior to protocol execution. Generation of these premises, although often standard, requires some thought. It is possible to generate too many premises. Our approach automatically generates these premises.
• Message Transmission/Receipt. The standard approach to validation assumes that all messages have already been received. It is possible to utilize the premises and messages received to derive incorrect or faulty beliefs. This is due to the fact that message receipt is not ordered [Sne91, AF97]. Our approach insists that message reception be treated in order.
• Idealization/Comprehension Premises. In any protocol, there are certain assumptions that the recipients make with respect to message meaning. These can be expressed in idealized versions of the message protocols, or in premises; but they must be expressed for the analysis to complete. If these premises or idealizations are incorrect, the analysis will fail. In [AF97] we provide a set of guidelines for the development of these idealizations; which are used in the analysis in this paper.
• Verification. It is often the case that the beliefs and comprehended messages of both participants are analyzed concurrently. This may result in the use of incorrect premises during the analysis. It also results in a more complicated proof. The technique we present here completely separates the proofs of the participants. This is also useful, since it does not force us to assume specific actions of the other participants; only that a message of a particular form has been received.
• Postconditions. The ultimate goal of protocol verification is to guarantee that following completion of the protocol, certain beliefs hold. The common protocol goals of [SvO96] are a good starting point for generation of these goals. These goals should be consistent with the protocol designer's intentions.
• Protocol Denotation. Most verification methods utilize the standard notation for protocol denotation. This involves the sequential list of all protocol messages and direction sent. Any auxiliary operations such as function application, encryption, decryption, etc. are only described textually. Our approach forces the explicit denotation of all of these steps for a more precise understanding of the protocol.

In particular, we present an approach to protocol verification based on the concept of the weakest precondition. The idea is to generate a set of postconditions/goals that we want the protocol to satisfy. Then, based on these postconditions and the steps of the protocol, generate the least restrictive set of preconditions such that upon completion of the protocol the goals will hold. To simplify the analysis, we handle each step of the protocol one at a time, propagating the generated preconditions through each step. To simplify presentation of this approach we assume that all conditions (pre and post) are represented in a set of conditions. The tables presented in the next section do not specifically reference the set, but rather only particular elements of the set. In other words, if a condition is relevant to a particular protocol step, it will be removed from the set of conditions and replaced with the necessary preconditions, otherwise it will be automatically propagated through as a precondition.

The choices regarding what the postconditions of an operation should be and what preconditions are necessary for those postconditions were primarily determined by the SvO logic [SvO94, SvO96]. The operations currently supported are: sending and receiving messages, applying functions, creating keys from public agreement keys, decrypting messages, construction of shared secrets, and proving statements. This includes the use of private, public, and shared keys. The wps were tested on several existing protocols. A discussion of the proof for the station-to-station protocol [DvOW92] and the Needham-Schroeder key distribution protocol [NS78] are included in Section 4 of this document.

Section 3 presents the weakest precondition rules. They are divided into four subsections, one for the general operations, one for proofs and beliefs, one for decryption using the various key types, and one for construction shared secrets. Section 4 presents analysis of the two exemplary protocols. Section 5 discusses a few issues regarding the use of the wps.