Specifying Kerberos 5 Cross-Realm Authentication

Cross-realm authentication is a useful and interesting component of Kerberos aimed at enabling secure access to services astride organizational boundaries. We present a formalization of Kerberos 5 cross-realm authentication in MSR, a specification language based on multiset rewriting. We also adapt the Dolev-Yao intruder model to the cross-realm setting and prove an important property for a critical field in a cross-realm ticket. Finally, we document several failures of authentication and confidentiality in the presence of compromised intermediate realms. Although the current Kerberos specifications disclaim responsibility for these vulnerabilities, the associated security implications must be highlighted for system administrators to decide whether to adopt this technology and to aid designers with future development.