full
search.png

Search

close.png

Cancel

arrow
Volume 2, Issue 3
Analyzing Authentication in Kerberos-5 Using Distributed Temporal Protocol Logic

J. Info. Comput. Sci. , 2 (2007), pp. 163-171.

Purchase PDF 61 875

Cited by

google scholar semantic scholar
Export citation
  • Abstract
Recently a Distributed Temporal Protocol Logic has been devised to capture reasoning in the distributed environment of security protocols. Elsewhere we have constructed a proof-based verification framework using distributed temporal protocol logic to verify the authentication property of security protocols. In this paper, we apply our verification framework to a well-known protocol. In particular, we analyze the authentication property of the public-key extension of Kerberos-5 protocol. We demonstrate how we are able to identify a subtle design flaw in the protocol. This results into showing the applicability of our framework as well as demonstrating the ease with which distributed temporal protocol logic can be used to analyze authentication protocols.
  • Keywords

Kerberos, distributed temporal protocol logic, formal verification, authentication.

  • AMS Subject Headings

  • Copyright

COPYRIGHT: © Global Science Press

  • Email address
  • BibTex
  • RIS
  • TXT
@Article{JICS-2-163, author = {}, title = {Analyzing Authentication in Kerberos-5 Using Distributed Temporal Protocol Logic}, journal = {Journal of Information and Computing Science}, year = {2024}, volume = {2}, number = {3}, pages = {163--171}, abstract = { Recently a Distributed Temporal Protocol Logic has been devised to capture reasoning in the distributed environment of security protocols. Elsewhere we have constructed a proof-based verification framework using distributed temporal protocol logic to verify the authentication property of security protocols. In this paper, we apply our verification framework to a well-known protocol. In particular, we analyze the authentication property of the public-key extension of Kerberos-5 protocol. We demonstrate how we are able to identify a subtle design flaw in the protocol. This results into showing the applicability of our framework as well as demonstrating the ease with which distributed temporal protocol logic can be used to analyze authentication protocols. }, issn = {1746-7659}, doi = {https://doi.org/}, url = {http://global-sci.org/intro/article_detail/jics/22794.html} }
TY - JOUR T1 - Analyzing Authentication in Kerberos-5 Using Distributed Temporal Protocol Logic AU - JO - Journal of Information and Computing Science VL - 3 SP - 163 EP - 171 PY - 2024 DA - 2024/01 SN - 2 DO - http://doi.org/ UR - https://global-sci.org/intro/article_detail/jics/22794.html KW - Kerberos, distributed temporal protocol logic, formal verification, authentication. AB - Recently a Distributed Temporal Protocol Logic has been devised to capture reasoning in the distributed environment of security protocols. Elsewhere we have constructed a proof-based verification framework using distributed temporal protocol logic to verify the authentication property of security protocols. In this paper, we apply our verification framework to a well-known protocol. In particular, we analyze the authentication property of the public-key extension of Kerberos-5 protocol. We demonstrate how we are able to identify a subtle design flaw in the protocol. This results into showing the applicability of our framework as well as demonstrating the ease with which distributed temporal protocol logic can be used to analyze authentication protocols.
. (2024). Analyzing Authentication in Kerberos-5 Using Distributed Temporal Protocol Logic. Journal of Information and Computing Science. 2 (3). 163-171. doi:
Copy to clipboard
BibteX RIS TXT
The citation has been copied to your clipboard