The inductive method rests on the notion of *event*.
Each time an agent *A* sends
an agent *B* a message *X*, the event
*Says* *A B X*

occurs in our model. This event suffices to describe all traffic over the network and is the only one envisaged so far.

Cryptographic protocols are formalised as the set of all possible traces, which are lists of events. Our specification defines this set inductively, i.e. it describes how to extend a trace of the set with a new event, according to the protocol operation.

Proving properties on the set formalising a protocol follows the classical
induction principle. Once shown that the property holds on the empty set,
we simply have to show that, if the property holds on a trace *evs*
of the set, it still holds on the traces that extend *evs* by means
of the rules for defining the set.
Proofs would be too long to carry out on paper. This is where the theorem
prover Isabelle comes into help.

The framework for shared-key protocols
existing before the analysis of Kerberos relied on a
*trusted party*, a special agent which has knowledge of all agents'
secret keys. An
eavesdropper, which attempts to get network resources by faking messages
and exploiting accidental key losses,
was impersonated by the agent *Spy*. Nonces were explicitly formalised
as legitimate parts of messages. Tackling Kerberos has brought up the need
for a few extensions (see Section 4).

Mon Aug 4 18:43:12 BST 1997