Analyzing Authentication in Kerberos-5 Using Distributed Temporal Protocol Logic
Year: 2007
Journal of Information and Computing Science, Vol. 2 (2007), Iss. 3 : pp. 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.
Journal Article Details
Publisher Name: Global Science Press
Language: English
DOI: https://doi.org/2024-JICS-22794
Journal of Information and Computing Science, Vol. 2 (2007), Iss. 3 : pp. 163–171
Published online: 2007-01
AMS Subject Headings:
Copyright: COPYRIGHT: © Global Science Press
Pages: 9