[ Changed 4th March 1997 ]
A novel protocol has been formally analyzed using the prover Isabelle/HOL, following the inductive approach described in the speaker's earlier work. A single run of the protocol delivers session keys to any number of agents, allowing neighbours to perform mutual authentication. The basic security theorem states that session keys are correctly delivered to adjacent pairs of honest agents, even if other agents in the chain are compromised. The complexity of the protocol caused modest difficulties in the specification and proofs, but symmetries in the protocol reduced the number of separate theorems to prove.