next up previous
Next: References Up: Using Isabelle to Prove Previous: Guarantees about Kerberos


  A framework for the analysis of cryptographic protocols based on the inductive method has been developed within Isabelle and applied to some case studies [8].

This paper has discussed the analysis of Kerberos by means of that framework. Kerberos was chosen because it is a popular authentication system which was still lacking a mechanised analysis. Hence, while Kerberos has met its first mechanisation, the Isabelle framework has been, in turn, extended to deal with two trusted parties and with timestamps.

This analysis has shown that the method scales up to real-world protocols, and has founded a new class of guarantees, the temporal properties, only partially investigated so far, which will be the field for the future research.

Acknowledgement    Giampaolo Bella wishes to thank the Fondazione Bonino-Pulejo (Messina-ITALY) and The British Council (Rome-ITALY) for funding his Ph.D. at the University of Cambridge (UK).

Giampaolo Bella
Mon Aug 4 18:43:12 BST 1997