posted on 1972-01-01, 00:00authored byFrederick Butler, Iliano Cervesato, Aaron D. Jaggard, Andre Scedrov
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.