Using Isabelle to Prove Properties of the Kerberos Authentication System
Giampaolo Bella · 1997
The Inductive method, previously used to analyse classical, noncebased cryptographic protocols, is here tailored to formalise Kerberos, a real-world, timestamp-based protocol. A complete formalisation of the whole protocol is achieved, and several guarantees about its entangled operation are proved using the theorem prover Isabelle. 1 Introduction 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 dierent 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 aws quickly. Deeper structural properties might...