A Formal Analysis of Some Properties of Kerberos 5 Using MSR

We formalize aspects of the Kerberos 5 authentication protocol in the Multi-Set Rewriting formalism (MSR) on two levels of detail. The more detailed formalization reflects the intricate structure of the Kerberos 5 specification, taking into account several protocol features which have not viously considered. In the abstract formalization, we prove an authentication property about Kerberos 5. We discovered three anomalies, one of which occurs on both levels of detail, while the other two rely on the richer structure of the detailed formalization. We also discuss how the addition of checksums (some of which are in the protocol specification and some of which are not) may eliminate the anomalies that we found.

• Type: Conference
• Year: 2002
• Where: CSFW
• Authors: Frederick Butler, Iliano Cervesato, Aaron D. Jaggard, Andre Scedrov
• Keywords: Authentication Protocol, CSFW 2002, Detailed Formalization, Multi-Set Rewriting Formalism, Security Privacy