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: