Protocols

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 $\send{P}{Q}{X}$ 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 $s \subseteq s'$, $X \in \Once'_P$ and $X \in \Sees'_Q$.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 $\baretransf$ that the transition function is augmenting for a fixed protocol:

A specification of a protocol is given by two sets of formulas, ${\cal A}$ (the assumptions) and ${\cal C}$ (the conclusions). Protocol ${\cal P}$ satisfies such a specification (notation: $\spec{{\cal A}}{{\cal P}}{{\cal C}}$)when ``${\cal A}$ holds initially'' guarantees that ``${\cal C}$ holds finally'', i.e., after running ${\cal P}$.We extend the relation $\models$between states and formulas to a relation between states and sets of formulas, as follows:

$$s \models {\cal F}~~:=~\nomath{for all} \phi \in {\cal F}:~ s \models \phi$$

Using this, the semantics of the specification triple $\spec{{\cal A}}{{\cal P}}{{\cal C}}$ is now defined as follows:

$$\begin{array} {lll} \models \spec{{\cal A}}{{\cal P}}{{\cal ... ... \ $implies$\ \transf{{\cal P}}{s} \models {\cal C}.\end{array}$$

 

Similarly, one can prove: