This section provides the wps for the five general operations of an authentication protocol:
{B receives X}
{A sends X}
K {A creates a key from public agreement keys}
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 
if A only passed along a full uncomprehended message that
contained . 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 
. 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.