Next: Protocols Up: A semantics for BAN Previous: Semantics of formulas

Soundness

$\begin{theorem}[Soundness] The logic as described in this article is sound with respect to the newly defined semantics.\end{theorem}$

$\begin{corollary} BAN logic is sound.\end{corollary}$

Proof of Theorem 11

For each axiom $\derives \phiimplpsi$ ,as summed up in section 2.2, we prove $s \models \phi \Rightarrow s \models \psi$ .

Rationality

does not have the form $\derives \phiimplpsi$ ; instead, we have to show that for each theorem $\phi$ (and any P in the environment) the formula $P \believes \phi$ is a tautology.
$\begin{outcase} % latex2html id marker 436 \begin{calc} \xpr{\derives \phi} \z{\... ...emantics of $\believes$} \xpr{s \models P \believes \psi}\end{calc}\end{outcase}$

Saying parts of a joint message

$\begin{calc} % latex2html id marker 459 \xpr{s \models P \oncesaid (X,Y)} \z{\eq... ..._P} \z{\equiv}{semantics of $\oncesaid$} \xpr{s \models P \oncesaid X}\end{calc}$

Saying contents of an encrypted message

$\begin{calc} % latex2html id marker 471 \xpr{s \models P \oncesaid \encrypt{X}{K... ..._P} \z{\equiv}{semantics of $\oncesaid$} \xpr{s \models P \oncesaid X}\end{calc}$

Seeing parts of a joint message

$\begin{calc} % latex2html id marker 494 \xpr{s \models P \sees (X,Y)} \z{\equiv}... ...in \Sees_P} \z{\equiv}{semantics of $\sees$} \xpr{s \models P \sees X}\end{calc}$

Awareness

$\begin{calc} % latex2html id marker 506 \xpr{s \models P \sees X} \z{\equiv}{sem... ...\z{\equiv}{semantics of $\sees$} \xpr{s \models P \believes P \sees X}\end{calc}$

Possessing keys of a seen key statement

$\begin{calc} % latex2html id marker 518 \xpr{s \models P \sees \key{Q}{R}{K}} \z... ...} \z{\equiv}{semantics of $\possesses$} \xpr{s \models P \possesses K}\end{calc}$

Possessing believed keys

$\begin{calc} % latex2html id marker 534 \xpr{s \models P \believes \key{Q}{R}{K}... ...} \z{\equiv}{semantics of $\possesses$} \xpr{s \models P \possesses K}\end{calc}$

Decryption

$\begin{calc} % latex2html id marker 550 \xpr{s \models P \possesses K \land P \s... ...in \Sees_P} \z{\equiv}{semantics of $\sees$} \xpr{s \models P \sees X}\end{calc}$

Good key ensures the utterer

We prove the soundness of this equivalent variant of the axiom: $\derives \key{P}{Q}{K} \implies (R \sees Y \implies Q \oncesaid X)$ ,where we may use the assumption that $\encrypt{X}{K}{Q} \in \Contents{Y}$ :

$\begin{calc} \xpr{s \models \key{P}{Q}{K}} \z{\Rightarrow}{semantics of $\bareke... ...antics of $\implies$} \xpr{s \models R \sees Y \implies Q \oncesaid X}\end{calc}$

$\fbox {\vphantom{\tiny .}}$