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

fYear

2011

fDate

3-5 June 2011

Firstpage

651

Lastpage

654

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/CSNT.2011.140

Filename

5966530