Verifying Confidentiality and Authentication in Kerberos 5

We present results from a recent project analyzing Kerberos 5. The main expected properties of this protocol, namely confidentiality and authentication, hold throughout the protocol. Our analysis also highlights a number of behaviors that do not follow the script of the protocol, although they do not appear harmful for the principals involved. We obtained these results by formalizing Kerberos 5 at two levels of detail in the multiset rewriting formalism MSR and by adapting an inductive proof methodology pioneered by Schneider. Our more detailed specification takes into account encryption types, flags and options, error messages, and a few timestamps.