Next: Rectification of formulas Up: The logic Previous: Axiomatisation

## Comparison with BAN logic

In order to understand the relation between our logic and BAN logic, we show that every theorem of BAN logic is a theorem of our logic -- in other words, that our logic is stronger. Because our logic stripped off the operator from most of the axioms, the following lemma will be useful in the proof.

From Believing Modus Ponens and the Rationality Rule we now obtain:

If part of a message is fresh, the whole of the message must be fresh as well:

Note that the reverse does not hold, since a message can contain old news'' next to new data; the combination is fresh, but every element is not.

Proof

It suffices to prove that all axioms of the BAN logic are theorems of our logic.

is our axiom Seeing parts of a joint message, and therefore a theorem.

both follow from Lemma 4 using the identification of the joining operator on formulas with the logical-and operator.

follows from the symmetry of the operator.

follows from our axiom Saying parts of a joint message and Lemma 3.

follows from our axioms Possessing believed keys and Decryption.

follows from our axiom Awareness and Lemmas 3 and 4.

follows from the definition of ,the idempotence of ,and Lemmas 3 and 4.

follows from Lemmas 3 and 5.

follows from the definitions of and and Lemmas 3 and 4.

Next: Rectification of formulas Up: The logic Previous: Axiomatisation