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.