next up previous
Next: Correctness of protocols Up: A semantics for BAN Previous: Soundness


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.

A {\em protocol} is a finite sequence of {\em actions}, where...
 ...ants} of a protocol are
the principals mentioned in its actions.\end{definition}
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:

We define the transition function 
$\baretransf$, mapping a s...
 ...{{\cal P}_2}{\transf{{\cal P}_1}{s}}\end{array}\end{displaymath}\end{definition}

Using Lemma 10 it follows immediately from the definition of $\baretransf$ that the transition function is augmenting for a fixed protocol:

\(s \subseteq \transf{{\cal P}}{s} \)\end{lemma}

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\end{displaymath}

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

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

The specifications may be composed:
If $\models \spec{{\cal A}}{{\...
then $\models \spec{{\cal A}}{{\cal P}_1;{\cal P}_2}{{\cal C}}$ \end{lemma}

\xpr{\models \spec{{\cal A}}{{\cal P}_1}{{\cal B}} \n...
 ...r{\models \spec{{\cal A}}{{\cal P}_1;{\cal P}_2}{{\cal C}}}\end{calc}\end{proof}

Similarly, one can prove:

If $\models \spec{{\cal A}}{{\cal P}}{{\cal B}}$ 
and $\models \sp...
 ...s \spec{{\cal A}\union{\cal A}'}{{\cal P}}{{\cal B}\union{\cal B}'}$ \end{lemma}

next up previous
Next: Correctness of protocols Up: A semantics for BAN Previous: Soundness