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