Next: The model Up: A semantics for BAN Previous: Comparison with BAN logic

Rectification of formulas

The rectify operation maps formulas to formulas. In particular, it maps formulas of the form to .It is defined as follows:

Directly from the definition on sets it follows that:

Proof

We prove it with structural induction on the derivation.

Case trivial proof: A trivial proof is a derivation step of the form , where .

Case deduction: Deduction is the introduction of implication by derivation:

If , then .

Using deduction, we may instantiate:

If , then .

From here we can derive, under the assumption :

Cases axioms of predicate logic: As an example, we prove our claim for the introduction of .Other introductions and eliminations (, , , )have analogous proofs.

Case Rationality: Let . We prove .

Case axiom:

For every axiom , we will prove , by deriving .

case Believing Modus Ponens: We prove it for the equivalent form

case Saying contents of an encrypted message:

case Awareness:

case Possessing believed keys:

The remaining axioms do not contain a believe operator, so they do not change under the rectify function.

Next: The model Up: A semantics for BAN Previous: Comparison with BAN logic