Up: A semantics for BAN Previous: References

# Appendix

Proof of Lemma 24

Considering the semantics of specification triples, it is sufficient to prove for every positive formula with that for arbitrary s , follows from positive, and .We will prove this by induction on the structure of (positive) . We write and .

First, assume that for some R : . Then:

Now assume that for no R : ; in particular, . We want to prove that also in that case . So assume , i.e., , and therefore . The only participant R' that can have is B . From and we see that , and so . Note further that . We now prove by induction on the structure of messages that for all M :

If , , and ,
then

Since , and are also increase, the proofs for , , and are analogous.

Proof of Lemma 28

The proof is analogous to the proof of Lemma 24. According to the semantics of specification triples, it is sufficient to prove for every formula in that for arbitrary s , follows from safe, and .For positive Lemma 24 ensures that . For (where is positive) we must prove that either is positive, or under the assumptions mentioned. We prove this by induction on the structure of (positive) .Before embarging on the induction, note that formulas of each of the forms , , and are invariant under the mapping , so that we can skip them in the case analysis.

Finally, the postponed Case  Observe that . The first conjunct of this expression is positive, which is enough to prove our claim. The second conjunct is not positive, hence we need to prove separately.

According to the definition of , we can assume:

For all :

We have to prove:

For all :

Let P and be given. We now distinguish three cases to prove the above implication: , and finally . Note that it is sufficient to prove .

For , we first observe that P=A (only the sender's set has changed). We now prove the following statement by induction on M :

If , , ,
and , then .

This proves by induction the claim

If , , ,
and , then .
which concludes Case of the induction of Lemma 28.

Up: A semantics for BAN Previous: References