S. P. Miller, J. I. Neuman, J. I. Schiller and J. H. Saltzer, “Kerberos Authentication and Authorisation System,” Technical Report, Technical Plan Section E.2.1, MIT, Athena, 1989.

has been cited by the following article:

• TITLE: Extending the Strand Space Method with Timestamps: Part II Application to Kerberos V

  AUTHORS: Yongjian Li, Jun Pang

  KEYWORDS: Strand Space, Kerberos V, Theorem Proving, Verification, Isabelle/HOL

  JOURNAL NAME: Journal of Information Security, Vol.1 No.2, October 29, 2010

  ABSTRACT: In this paper, we show how to use the novel extended strand space method to verify Kerberos V. First, we formally model novel semantical features in Kerberos V such as timestamps and protocol mixture in this new framework. Second, we apply unsolicited authentication test to prove its secrecy and authentication goals of Kerberos V. Our formalization and proof in this case study have been mechanized using Isabelle/HOL.