In the previous section we have proven our logic sound, so every theorem of the logic is a tautology in the model. This, however, does not by itself establish in any way the suitability of the logic as a tool for proving protocols correct. In fact, protocols were not referred to at all.
We model actions as transitions from states to states. If in state s the action is performed, only the local states for P and Q will be changed. The new state s' is the least (closed global) state such that , and .From the closure properties we know that the local states for other principals stay unchanged. Formally:
Using Lemma 10 it follows immediately from the definition of that the transition function is augmenting for a fixed protocol:
A specification of a protocol is given by two sets of formulas, (the assumptions) and (the conclusions). Protocol satisfies such a specification (notation: )when `` holds initially'' guarantees that `` holds finally'', i.e., after running .We extend the relation between states and formulas to a relation between states and sets of formulas, as follows:
Using this, the semantics of the specification triple is now defined as follows:
Similarly, one can prove: