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

- C1:
- C2:
- C3:
- C4:

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 *C*1 and
*C*2 together mean that if the enemy only ever sees messages of
positive rank, then he can only ever generate messages of positive
rank.

Condition *C*4 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 *C*3 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 *C*1 to *C*4 all true,
and to verify this fact.