Research ArticleOpen AccessGoogle Scholar indexed
Extending the Strand Space Method with Timestamps: Part II Application to Kerberos V
- 1
- 2
Journal of Information Security·Volume 01 (2010)·Pages 56–67·Published 29 October 2010·DOI10.4236/jis.2010.12007
Copy link · social · email
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.
KeywordsStrand SpaceKerberos VTheorem ProvingVerificationIsabelle/HOL
- Y. L. and J. Pang, “Extending the Strand Space Method with Timestamps: Part I the Theory,” Journal of Information Security, Vol. 1, No. 2, 2010, pp. 45-55.
- G. Bella, “Inductive Verification of Cryptographic Protocols,” PhD Thesis, Cambridge University Computer Laboratory, 2000.
- L. Bozga, C. Ene and Y. Lakhnech, “A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps,” Journal of Logic and Algebraic Programming, Vol. 65, No. 1, 2005, pp. 1-35.
- F. Butler, I. Cervesato, A. Jaggard and A. Scedrov, “A formal Analysis of Some Properties of Kerberos 5 Using MSR,” Proceedings of 15th IEEE Computer Security Foundations Workshop, 2002, pp. 175-190.
- K. R. C. Neuman and S. Hartman, “The Kerberos Network Authentication Service (v5),” Technical report, Internet RFC 4120, July 2005.
- F. Javier Thayer, J. C. Herzog and J. D. Guttman, “Strand Spaces: Proving Security Protocols Correct,” Journal of Computer Security, Vol. 7, No. 1, 1999, pp. 191-230.
- Y. Li, “Strand Space and Security Protocols,” http://lcs. ios.ac.cn/?lyj238/strand.html.
- 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.
- J. C. Mitchell, M. Mitchell and U. Stern, “Automated Analysis of Cryptographic Protocols Using Murphi,” Proceedings of 18th Symposium on Security and Privacy, 1997, pp. 141-153.