We obtain an extremely specialised theorem that applies to
authentication properties on this specific description NET of the
network. This theorem is at the heart of the proof strategy presented
in this paper. It provides a sufficient list of conditions whose
achievement guarantees that NET
.
Theorem 1
The rank function is intended to have positive value on all
messages which can be generated by some agent (including the enemy)
during a run of the protocol, when all messages in the set R are
prevented from occurring. The intention is to show that this
restriction on R means that no event from T can occur, and hence
by Lemma 1 that
. Conditions C1 and
C2 together mean that if the enemy only ever sees messages of
positive rank, then he can only ever generate messages of positive
rank.
Condition C4 states that the same is true for the users of the
network (when restricted on R ): they never output a message of
non-positive rank unless they previously received such a message. The
specification is defined as:
If every message received on rec has positive rank, then so does every message sent out on trans .
The predicate ``'' can therefore be seen as describing an
invariant: at every stage of the protocol's execution when R is
suppressed, it must hold of the next message. Since C3 states that
it does not hold for any message in T , this means that no message in
T can ever be generated.
The problem for any particular protocol, and a particular
authentication property expressed in terms of R and T , is to find
an appropriate rank function which makes C1 to C4 all true,
and to verify this fact.