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 proceedingConference 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 languageEnglish
Title of host publicationProceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011
Pages651-654
Number of pages4
DOIs
Publication statusPublished - 2011
Event2011 International Conference on Communication Systems and Network Technologies, CSNT 2011 - Katra, Jammu, India
Duration: 03-06-201105-06-2011

Conference

Conference2011 International Conference on Communication Systems and Network Technologies, CSNT 2011
CountryIndia
CityKatra, Jammu
Period03-06-1105-06-11

Fingerprint

secrecy
integrity
Authentication
Network protocols
Security of data
Specifications

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Communication

Cite this

Mundra, P., Shukla, S., Sharma, M., Pai, R. M., & 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 (pp. 651-654). [5966530] https://doi.org/10.1109/CSNT.2011.140
Mundra, Punit ; Shukla, Shobhit ; Sharma, Madhavi ; Pai, Radhika M. ; Singh, Sanjay. / Modeling and verification of kerberos protocol using symbolic model verifier. Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011. 2011. pp. 651-654
@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",

}

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

Modeling and verification of kerberos protocol using symbolic model verifier. / Mundra, Punit; Shukla, Shobhit; Sharma, Madhavi; Pai, Radhika M.; Singh, Sanjay.

Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011. 2011. p. 651-654 5966530.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

SN - 9780769544373

SP - 651

EP - 654

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

ER -

Mundra P, Shukla S, Sharma M, Pai RM, Singh S. Modeling and verification of kerberos protocol using symbolic model verifier. In Proceedings - 2011 International Conference on Communication Systems and Network Technologies, CSNT 2011. 2011. p. 651-654. 5966530 https://doi.org/10.1109/CSNT.2011.140