file.pdf (292.55 kB)
Verifying Confidentiality and Authentication in Kerberos 5
journal contribution
posted on 1972-01-01, 00:00 authored by Frederick Butler, Iliano Cervesato, Aaron D. Jaggard, Andre ScedrovWe 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.