Table 6: Weakest preconditions for proving a statement.
Table 7: Weakest preconditions for beliefs.
During the operation of a protocol, participants will often prove statements and develop a set of beliefs. Although these operations are typically not explicitly stated in the protocol denotation and are sometimes only implicit in the textual description of the protocol; they are essential to the operation of the protocol, and more importantly, to the validation of protocol correctness. Table 6 demonstrates the wps for proving; these are modus ponens and the axiom for control. Table 7 shows the wps for beliefs. The first is necessitation, which is only applied to theorems that can be proven from the base axioms and proof rule. The second is the application of belief to wps, where if B believes a condition after an operation, then B believes the wp of that condition prior to the operation (this permits reasoning about beliefs without duplicating each wp rule for beliefs).