Modeling and verification of kerberos protocol using symbolic model verifier

Punit Mundra; Shobhit Shukla; Madhavi Sharma; Radhika M. Pai; Sanjay Singh

doi:10.1109/CSNT.2011.140

Modeling and verification of kerberos protocol using symbolic model verifier

Punit Mundra, Shobhit Shukla, Madhavi Sharma, Radhika M. Pai, Sanjay Singh

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 Citations (Scopus)

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.

Original language	English
Title of host publication	Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011
Pages	651-654
Number of pages	4
DOIs	https://doi.org/10.1109/CSNT.2011.140
Publication status	Published - 2011
Event	2011 International Conference on Communication Systems and Network Technologies, CSNT 2011 - Katra, Jammu, India Duration: 03-06-2011 → 05-06-2011

Conference

Conference	2011 International Conference on Communication Systems and Network Technologies, CSNT 2011
Country/Territory	India
City	Katra, Jammu
Period	03-06-11 → 05-06-11

All Science Journal Classification (ASJC) codes

Computer Networks and Communications
Communication

Access to Document

10.1109/CSNT.2011.140

Cite this

@inproceedings{caef5766df1c423ea14a51ec1d93f9f2,

title = "Modeling and verification of kerberos protocol using symbolic model verifier",

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.",

author = "Punit Mundra and Shobhit Shukla and Madhavi Sharma and Pai, {Radhika M.} and Sanjay Singh",

year = "2011",

doi = "10.1109/CSNT.2011.140",

language = "English",

isbn = "9780769544373",

pages = "651--654",

booktitle = "Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011",

note = "2011 International Conference on Communication Systems and Network Technologies, CSNT 2011 ; Conference date: 03-06-2011 Through 05-06-2011",

}

Mundra, P, Shukla, S, Sharma, M, Pai, RM & Singh, S 2011, Modeling and verification of kerberos protocol using symbolic model verifier. in Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011., 5966530, pp. 651-654, 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011, Katra, Jammu, India, 03-06-11. https://doi.org/10.1109/CSNT.2011.140

TY - GEN

T1 - Modeling and verification of kerberos protocol using symbolic model verifier

AU - Mundra, Punit

AU - Shukla, Shobhit

AU - Sharma, Madhavi

AU - Pai, Radhika M.

AU - Singh, Sanjay

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=80052129540&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80052129540&partnerID=8YFLogxK

U2 - 10.1109/CSNT.2011.140

DO - 10.1109/CSNT.2011.140

M3 - Conference contribution

AN - SCOPUS:80052129540

SN - 9780769544373

SP - 651

EP - 654

BT - Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011

T2 - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011

Y2 - 3 June 2011 through 5 June 2011

ER -

Modeling and verification of kerberos protocol using symbolic model verifier

Abstract

Conference

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this