Kerberos Authentication Protocol Modeling Using NUSMV Model
Brajesh Patel, Priyanka Dubey · 2012
Authentication is one of the biggest problem related to computer information security in the area of distributed environments. Various protocols are used for the authentication purpose such as Needham-Schroeder protocol Kerberos protocol etc. The aim of this paper is to verify and formalize the Kerberos protocol using NuSMV model checker. The protocol v e r s i o n used in this paper is Kerberos Authentication Protocol. The paper suggests CTL specifications for authentication, secrecy and i n t e g r i t y. We have also proposed an approach to identify presence of intruder in the system.