Since Needham and Schroeder pioneered in [6] that protocol errors are unlikely to be detected in normal operations and that the need for techniques to verify the correctness of such protocols is great, a number of methods have been developed to analyse cryptographic protocols. However, none of these methods can claim that a protocol is mathematically secure.
A combination of different methods might yield the best results. For instance, the use of a belief logic [3] during the design phase might help ensure freshness properties, and the use of a state enumeration method [4] might pinpoint simple flaws quickly. Deeper structural properties might be proved by way of the inductive method.
Using such a method, some famous cryptographic protocols of the literature have been analysed with the support of the generic theorem prover Isabelle. Several guarantees (nearly two hundred theorems in all) have been established about the following protocols: Needham-Schroeder (both shared-key and public-key), Otway-Rees, Yahalom [8, 9, 10]. A new attack has been discovered in a variant of the Otway-Rees protocol.
The inductive approach has also been tailored to analyse real-world protocols. The first one tackled in this field is Kerberos [5, 1], whose analysis has required some effort for the mechanism of broadcast of a session key to the intended recipients which relies on the presence of two different trusted third parties. Kerberos is the first protocol relying on the use of timestamps (instead of nonces) to prevent the replay of messages. This has caused the introduction in the framework of a function yielding the current time and has brought the case for the definition of a new class of theorems stating temporal properties.
Assuming that the reader is familiar with Kerberos, Section 2 sketches the basic operation of the protocol. It also gives the motivations for the choice of Kerberos by going through the little related work. Section 3 then gives a feel about the inductive method, and Section 4 presents the actual analysis of the protocol. Finally, Section 5 sums up the paper. The complete Isabelle specification of Kerberos is given in Appendix.