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 | |
| 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 | India |
| City | Katra, Jammu |
| Period | 03-06-11 → 05-06-11 |
Fingerprint
All Science Journal Classification (ASJC) codes
- Computer Networks and Communications
- Communication
Cite this
}
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 proceeding › Conference 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 -