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

HTML  Download Download as PDF (Size: 471KB)  PP. 56-67  
DOI: 10.4236/jis.2010.12007    5,385 Downloads   9,291 Views  Citations
Author(s)

Affiliation(s)

.

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.

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.

Copyright © 2024 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.