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

Yongjian Li, Jun Pang

.

DOI: 10.4236/jis.2010.12007                

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.

Keywords

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

Conflicts of Interest

The authors declare no conflicts of interest.

References

[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.