next up previous
Next: Introduction

Using Isabelle to Prove Properties of the
Kerberos Authentication System

Giampaolo Bellagif    Lawrence C Paulsongif

Computer Laboratory - University of Cambridge
New Museums Site, Pembroke Street
Cambridge CB2 3QG (UK)


The Inductive method, previously used to analyse classical, nonce-based 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.

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