We present initial results of an ongoing analysis (joint work with F. Butler, I. Cervesato, and A. Scedrov) of Kerberos 5 using the MultiSet Rewriting (MSR) framework. . Kerberos 5 is intended to allow the repeated authentication of a client to multiple servers using a single login. We give MSR formalizations of this protocol at two levels of detail. This indicates the utility of the MSR framework in analyzing real world protocols and allows us to prove, in our abstract formalization, some authentication properties of this protocol. In the process, we find some anomalous behavior in the protocol. Our proofs of authentication properties use notions of rank and corank inspired by Schneider, and may suggest reasoning methods which are well suited to MSR.