Giampaolo Bella Lawrence
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.