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).