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