next up previous
Next: Comparison with BAN logic Up: The logic Previous: The language


  For the axiomatisation we need to define the contents of a message as the collection of submessages when encryption is transparent:

The function $\Contents{\placeh}$\space takes a message and
 ...s{X} & := \{X\} \nomath{(otherwise)}\end{array}\end{displaymath}\end{definition}

The axiomatisation includes the standard axioms for equational logic with Modus Ponens -- which subsumes propositional logic -- and the standard rules for universal quantification, where a formula $\phi\bareiff\psi$ is treated as shorthand for $(\phiimplpsi)\land(\psi\bareimpl\phi)$.

Beneath, we introduce a collection of axioms for the specific operators of our logic, and mention the related axiom in the original BAN logic -- if such an axiom exists. (Because of the presence of the Modus Ponens rule, we can replace inference rules (20,12)[l]\( \begin{array}
\\  \hline
\psi\end{array} \)by axioms $\derives \phiimplpsi$.)

For message joining there are all axioms of the forms $\derives (X,(Y,Z)) = ((X,Y),Z)$,$\derives (X,Y) = (Y,X)$ and $\derives (X,X) = X$, and for the $\barekey$ operator $\derives \key{P}{Q}{K} = \key{Q}{P}{K}$.Equational logic allows us to apply theorems of the form $\derives \phi[x] \land x=y \:\implies\: \phi[y]$.

Furthermore, we have:

The rationality rule introduces a collection of axioms, one for every theorem of the logic: \begin{displaymath}
\derives \phi
\\  \hline
\derives P \believes \phi\end{array} \end{displaymath}

This axiom, together with the next one, lifts the level of reasoning from beliefs of principals to general statements.

Believing Modus Ponens
Modus Ponens under the $\believes$ operator: \begin{displaymath}
\derives P \believes (\phiimplpsi) \implies 
 (P \believes \phi \implies P \believes \psi) \end{displaymath}

Saying parts of a joint message
Uttering a joint message implies uttering each of the parts:

\derives P \oncesaid (X,Y) \implies P \oncesaid X \end{displaymath}

The related BAN logic axiom is: \begin{displaymath}
\banderives P \believes Q \oncesaid (X,Y) 
 \implies P \believes Q \oncesaid X \end{displaymath}

Saying contents of an encrypted message
Uttering an encrypted message, signed by yourself, while you believe that the key is good, implies uttering of the encrypted message:

\derives P \oncesaid \encrypt{X}{K}{P} \:\land\: P \believes \key{P}{Q}{K} 
 \implies P \oncesaid X \end{displaymath}

There is no similar axiom in BAN logic.

Seeing parts of a joint message
Seeing a joint message means seeing each part separately as well:

\derives P \sees (X,Y) \implies P \sees X \end{displaymath}

The BAN logic has this axiom (exactly so) as well.

Awareness of what one sees:

\derives P \sees X \implies P \believes P \sees X \end{displaymath}

There is no similar axiom in BAN logic.

Possessing keys of a seen key statement
If one sees a key statement, one possesses the key that it mentioned: \begin{displaymath}
\derives P \sees \key{Q}{R}{K} \implies P \possesses K \end{displaymath}

In BAN logic, the notion of possession does not exist.

Possessing believed keys
One can only believe that a certain key is good if possessing the key: \begin{displaymath}
\derives P \believes \key{Q}{R}{K} \implies P \possesses K \end{displaymath}

Seeing an encrypted message while having the key in possession, means seeing the message itself: \begin{displaymath}
\derives P \possesses K \land P \sees \encrypt{X}{K}{Q} 
 \implies P \sees X \end{displaymath}

The related BAN logic axiom is decryption:

\banderives P \believes \key{P}{Q}{K} \:\land\: P \sees \encrypt{X}{K}{Q}
 \implies P \sees X\end{displaymath}In BAN logic one can only decrypt with keys that are believed to be one's own key. With any other key in possession, decryption cannot be derived, since BAN logic does not have a notion of possession.

Good key ensures the utterer
A collection of axioms, stating that if a key is good, the only ones that use it for encryption are the owners, so if somewhere, someone sees a message that contains a part encrypted with that key, that part must have been said by the key owner who encrypted it:
For all P,Q,R,X,Y,K such that $\encrypt{X}{K}{Q} \in \Contents{Y}$:

\derives \key{P}{Q}{K} \land R \sees Y \implies Q \oncesaid X\end{displaymath}

The related BAN logic axiom is the message meaning rule: \begin{displaymath}
\banderives P \believes \key{P}{Q}{K} \:\land\: P \sees \encrypt{X}{K}{Q}
 \implies P \believes Q \oncesaid X \end{displaymath}

The BAN axioms that were not mentioned above are:

\banderives P \believes \phi \:\land\: P \believes \psi 
 \implies P \believes (\phi,\psi) \end{displaymath}

\banderives P \believes (\phi,\psi) 
 \implies P \believes \phi \end{displaymath}

\banderives P \believes \key{Q}{R}{K} 
 \implies P \believes \key{R}{Q}{K} \end{displaymath}

\banderives P \believes \fresh \phi \:\land\ P \believes Q \oncesaid \phi
 \implies P \believes Q \believes \phi \end{displaymath}

\banderives P \believes\fresh X \implies P \believes\fresh(X,Y)\end{displaymath}

\banderives P \believes Q \controls \phi 
 \:\land\: P \believes Q \believes \phi
 \implies P \believes \phi \end{displaymath}

next up previous
Next: Comparison with BAN logic Up: The logic Previous: The language