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.
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.