Kerberos Authentication Protocol Modeling Using NUSMV Model

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 version used in this paper is Kerberos Authentication Protocol. The paper suggests CTL specifications for authentication, secrecy and integrity. We have also proposed an approach to identify presence of intruder in the system.