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

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.


\begin{definition}
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:


\begin{definition}
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:


\begin{lemma}
\(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:

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

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


 \begin{lemma}
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}


\begin{proof}
\begin{calc}
\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:


 \begin{lemma}
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