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

DOI: 10.4236/jis.2010.12007   PDF   HTML     5,087 Downloads   8,664 Views   Citations


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.

Share and Cite:

Y. Li and J. Pang, "Extending the Strand Space Method with Timestamps: Part II Application to Kerberos V," Journal of Information Security, Vol. 1 No. 2, 2010, pp. 56-67. doi: 10.4236/jis.2010.12007.

Conflicts of Interest

The authors declare no conflicts of interest.


[1] 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.
[2] G. Bella, “Inductive Verification of Cryptographic Protocols,” PhD Thesis, Cambridge University Computer Laboratory, 2000.
[3] 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.
[4] 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.
[5] K. R. C. Neuman and S. Hartman, “The Kerberos Network Authentication Service (v5),” Technical report, Internet RFC 4120, July 2005.
[6] 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.
[7] Y. Li, “Strand Space and Security Protocols,” http://lcs. ios.ac.cn/?lyj238/strand.html.
[8] 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.
[9] 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.

comments powered by Disqus

Copyright © 2020 by authors and Scientific Research Publishing Inc.

Creative Commons License

This work and the related PDF file are licensed under a Creative Commons Attribution 4.0 International License.