Formal verification of the extensible authentication protocol using SPIN

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

doi:10.1145/2393216.2393278

Formal verification of the extensible authentication protocol using SPIN

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

^*Corresponding author for this work

Manipal Institute of Technology, Manipal

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

2 Citations (Scopus)

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 language	English
Title of host publication	Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012
Pages	365-371
Number of pages	7
DOIs	https://doi.org/10.1145/2393216.2393278
Publication status	Published - 12-12-2012
Event	2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012 - Coimbatore, India Duration: 26-10-2012 → 28-10-2012

Publication series

Name	ACM International Conference Proceeding Series

Conference

Conference	2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012
Country/Territory	India
City	Coimbatore
Period	26-10-12 → 28-10-12

All Science Journal Classification (ASJC) codes

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

Access to Document

10.1145/2393216.2393278

Cite this

@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 = dec,

day = "12",

doi = "10.1145/2393216.2393278",

language = "English",

isbn = "9781450313100",

series = "ACM International Conference Proceeding Series",

pages = "365--371",

booktitle = "Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012",

note = "2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012 ; Conference date: 26-10-2012 Through 28-10-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. ACM International Conference Proceeding Series, 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 (ACM International Conference Proceeding Series).

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 - https://www.scopus.com/pages/publications/84870707082

UR - https://www.scopus.com/pages/publications/84870707082#tab=citedBy

U2 - 10.1145/2393216.2393278

DO - 10.1145/2393216.2393278

M3 - Conference contribution

AN - SCOPUS:84870707082

SN - 9781450313100

T3 - ACM International Conference Proceeding Series

SP - 365

EP - 371

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

T2 - 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012

Y2 - 26 October 2012 through 28 October 2012

ER -

Formal verification of the extensible authentication protocol using SPIN

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this