next up previous
Next: Proofs and Beliefs Up: Weakest Preconditions Previous: Weakest Preconditions

General Operations

This section provides the wps for the five general operations of an authentication protocol:

The first three operations listed are explicitly denoted in the presentation of any authentication protocol. They involve the sending and receiving of messages as well as a sequential ordering of operations. It is interesting to note that most protocol specifications combine the act of sending and receiving messages as a single operation. This is acceptable if we can be assured that both parties are following the correct operations of the protocol, and are who they claim to be. As such, we prefer to distinguish between the acts of sending and receiving messages, to enable us to evaluate the actions and beliefs of the participants independently.

Table 1: Weakest preconditions for composition of two operations.

In Table 1 we present the wp for operation composition. This enables us to treat each operation separately by treating the wp of operation T as the postcondition to operation S.

Table 2: Weakest preconditions for sending a message.

Table 3: Weakest preconditions for receiving a message.

To enable communication between participants we have the operations of sending and receiving messages. In Table 2 we present the wps for message sending. The semantics here state that prior to sending a message a participant must have seen the message. In addition, if we want to state that a participant sent a component of a message, then it is necessary that they see the component. In other words, we can not claim that A sent tex2html_wrap_inline1107 if A only passed along a full uncomprehended message that contained tex2html_wrap_inline1107 . It is also worth noting that if we limit the evaluation of the protocol to only what can be inferred directly by the recipient (as discussed by Syverson and van Oorschot in [Syv96, SvO96]), we never need worry about messages sent by another participant. We leave this wp in place however, since there may be analysis methods that require that a participant be aware of messages previously sent by itself (see [AF97]).

In Table 3 we present the wps for message receipt. The conditions in this case are rather straight forward. Upon receipt of a message X, B will have received it and seen it. B will also have received and seen all components of the message. If we follow the message comprehension method of Syverson and van Oorschot [SvO96], B receives and sees the uncomprehended messages tex2html_wrap_inline1111 . Additional preconditions must be put in place to specify what B comprehends; work on this is left for a future paper. The message will be considered fresh if there is a component of X that is fresh.

Table 4: Weakest preconditions for applying a function.

Function application is one of the most basic operations of an authentication protocol, and is usually not explicitly stated in the presentation of a protocol but rather only in the textual description of the protocol. This includes, but is not limited to encryption, decryption, key creation and modification of a message. The basic conditions we are concerned about in Table 4 are that A sees all parameters prior to function application and that for the result to be fresh, one of the components must be fresh. A special example of function application is the creation of a key, as depicted in Table 5. The creation of public agreement keys requires special axioms (see [SvO94, SvO96]), and thus is treated separately here.

Table 5: Weakest preconditions for creating a key from public-agreement keys.

next up previous
Next: Proofs and Beliefs Up: Weakest Preconditions Previous: Weakest Preconditions

Jim Alves-Foss
Fri Aug 1 16:00:31 PDT 1997