Title :
Modeling and Verification of Kerberos Protocol Using Symbolic Model Verifier
Author :
Mundra, Punit ; Shukla, Shobhit ; Sharma, Madhavi ; Pai, Radhika M. ; Singh, Sanjay
Author_Institution :
Dept. of Inf. & Commun. Technol., Manipal Univ., Manipal, India
Abstract :
Authentication is one of the biggest issues concerning information security in the context of distributed environments. Various protocols are used for the authentication purpose such as Needham-Schroeder, 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 version 4. The paper suggests CTL specifications for authentication, secrecy and integrity. We have also proposed an approach to identify presence of intruder in the system.
Keywords :
authorisation; computer network security; data privacy; formal specification; formal verification; protocols; CTL specification; Kerberos protocol modeling; Kerberos protocol verification; NuSMV model checker; authorization; client-server model; computer network authentication protocol; distributed environment; information security; integrity; mutual authentication; secrecy; symbolic model verifier; system intruder presence identification; Authentication; Computational modeling; Cryptography; Protocols; Radiation detectors; Servers; CTL; Kerberos Protocol; NuSMV Model Checker;
Conference_Titel :
Communication Systems and Network Technologies (CSNT), 2011 International Conference on
Conference_Location :
Katra, Jammu
Print_ISBN :
978-1-4577-0543-4
Electronic_ISBN :
978-0-7695-4437-3
DOI :
10.1109/CSNT.2011.140
