Journal of Information Security

Volume 1, Issue 2 (October 2010)

ISSN Print: 2153-1234   ISSN Online: 2153-1242

Google-based Impact Factor: 1.90  Citations  h5-index & Ranking

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    4,997 Downloads   8,530 Views   Citations
Author(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.

Cite this paper

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.

Cited by

[1] Nonce-based Kerberos is a Secure Delegated AKE Protocol
IACR Cryptology ePrint Archive, 2016
[2] Secure time information in the internet key exchange protocol
Annales UMCS, Informatica, 2011

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.