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 | |
| 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 |
Conference
| Conference | 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012 |
|---|---|
| Country | India |
| City | Coimbatore |
| Period | 26-10-12 → 28-10-12 |
Fingerprint
All Science Journal Classification (ASJC) codes
- Software
- Human-Computer Interaction
- Computer Vision and Pattern Recognition
- Computer Networks and Communications
Cite this
}
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 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 - 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
AN - SCOPUS:84870707082
SN - 9781450313100
SP - 365
EP - 371
BT - Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012
ER -