Axiomatisation

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

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]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:

Rationality

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

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: $$\derives P \believes (\phiimplpsi) \implies (P \believes \phi \implies P \believes \psi)$$

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$$

The related BAN logic axiom is: $$\banderives P \believes Q \oncesaid (X,Y) \implies P \believes Q \oncesaid X$$

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$$

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$$

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

Awareness

Awareness of what one sees:

$$\derives P \sees X \implies P \believes P \sees X$$

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: $$\derives P \sees \key{Q}{R}{K} \implies P \possesses K$$

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: $$\derives P \believes \key{Q}{R}{K} \implies P \possesses K$$

Decryption

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

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$$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$$

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

The BAN axioms that were not mentioned above are:

$$\banderives P \believes \phi \:\land\: P \believes \psi \implies P \believes (\phi,\psi)$$

$$\banderives P \believes (\phi,\psi) \implies P \believes \phi$$

$$\banderives P \believes \key{Q}{R}{K} \implies P \believes \key{R}{Q}{K}$$

$$\banderives P \believes \fresh \phi \:\land\ P \believes Q \oncesaid \phi \implies P \believes Q \believes \phi$$

$$\banderives P \believes\fresh X \implies P \believes\fresh(X,Y)$$

$$\banderives P \believes Q \controls \phi \:\land\: P \believes Q \believes \phi \implies P \believes \phi$$