Formal verification of the extensible authentication protocol using SPIN

H. K. Jnanamurthy, Manu S.hegde, Sanjay Singh

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

Abstract

The Extensible Authentication Protocol (EAP) is a framework for transporting authentication credentials. EAP offers simpler interoperability and compatibility across authentication methods. In this paper, we have modeled the Extensible Authentication Protocol is modeled as a finite state machine. Then the model is checked for conformance with its specifications to detect possible flaws. The various entities in our model are Authenticator, EAP Server, User and User Database. The messages exchanged between various entities are modeled as transitions. The model is represented in PROMELA. Then the model is verified using SPIN model checker. This enables us to check working of protocol before implementation.

Original languageEnglish
Title of host publicationProceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012
Pages365-371
Number of pages7
DOIs
Publication statusPublished - 12-12-2012
Event2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012 - Coimbatore, India
Duration: 26-10-201228-10-2012

Conference

Conference2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012
CountryIndia
CityCoimbatore
Period26-10-1228-10-12

Fingerprint

Authentication
Network protocols
Finite automata
Interoperability
Formal verification
Servers
Specifications
Defects

All Science Journal Classification (ASJC) codes

  • Software
  • Human-Computer Interaction
  • Computer Vision and Pattern Recognition
  • Computer Networks and Communications

Cite this

Jnanamurthy, H. K., S.hegde, M., & Singh, S. (2012). Formal verification of the extensible authentication protocol using SPIN. In Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012 (pp. 365-371) https://doi.org/10.1145/2393216.2393278
Jnanamurthy, H. K. ; S.hegde, Manu ; Singh, Sanjay. / Formal verification of the extensible authentication protocol using SPIN. Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012. 2012. pp. 365-371
@inproceedings{790ad5168a1a4ec08d9afb58dd38a506,
title = "Formal verification of the extensible authentication protocol using SPIN",
abstract = "The Extensible Authentication Protocol (EAP) is a framework for transporting authentication credentials. EAP offers simpler interoperability and compatibility across authentication methods. In this paper, we have modeled the Extensible Authentication Protocol is modeled as a finite state machine. Then the model is checked for conformance with its specifications to detect possible flaws. The various entities in our model are Authenticator, EAP Server, User and User Database. The messages exchanged between various entities are modeled as transitions. The model is represented in PROMELA. Then the model is verified using SPIN model checker. This enables us to check working of protocol before implementation.",
author = "Jnanamurthy, {H. K.} and Manu S.hegde and Sanjay Singh",
year = "2012",
month = "12",
day = "12",
doi = "10.1145/2393216.2393278",
language = "English",
isbn = "9781450313100",
pages = "365--371",
booktitle = "Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012",

}

Jnanamurthy, HK, S.hegde, M & Singh, S 2012, Formal verification of the extensible authentication protocol using SPIN. in Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012. pp. 365-371, 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012, Coimbatore, India, 26-10-12. https://doi.org/10.1145/2393216.2393278

Formal verification of the extensible authentication protocol using SPIN. / Jnanamurthy, H. K.; S.hegde, Manu; Singh, Sanjay.

Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012. 2012. p. 365-371.

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

TY - GEN

T1 - Formal verification of the extensible authentication protocol using SPIN

AU - Jnanamurthy, H. K.

AU - S.hegde, Manu

AU - Singh, Sanjay

PY - 2012/12/12

Y1 - 2012/12/12

N2 - The Extensible Authentication Protocol (EAP) is a framework for transporting authentication credentials. EAP offers simpler interoperability and compatibility across authentication methods. In this paper, we have modeled the Extensible Authentication Protocol is modeled as a finite state machine. Then the model is checked for conformance with its specifications to detect possible flaws. The various entities in our model are Authenticator, EAP Server, User and User Database. The messages exchanged between various entities are modeled as transitions. The model is represented in PROMELA. Then the model is verified using SPIN model checker. This enables us to check working of protocol before implementation.

AB - The Extensible Authentication Protocol (EAP) is a framework for transporting authentication credentials. EAP offers simpler interoperability and compatibility across authentication methods. In this paper, we have modeled the Extensible Authentication Protocol is modeled as a finite state machine. Then the model is checked for conformance with its specifications to detect possible flaws. The various entities in our model are Authenticator, EAP Server, User and User Database. The messages exchanged between various entities are modeled as transitions. The model is represented in PROMELA. Then the model is verified using SPIN model checker. This enables us to check working of protocol before implementation.

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

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

U2 - 10.1145/2393216.2393278

DO - 10.1145/2393216.2393278

M3 - Conference contribution

SN - 9781450313100

SP - 365

EP - 371

BT - Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012

ER -

Jnanamurthy HK, S.hegde M, Singh S. Formal verification of the extensible authentication protocol using SPIN. In Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012. 2012. p. 365-371 https://doi.org/10.1145/2393216.2393278