Modelling and Verification of Extensible Authentication Protocol Using SPIN Model Checker
The Extensible Authentication Protocol (EAP) is a framework for transporting authentication credentials. EAP offers simpler interoperability and compatibility across authentication methods. EAP supports multiple authentication methods. In this paper, the authors have modeled the Extensible Authentication Protocol as a finite state machine. The various entities in their 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. The model is checked for conformance with its specifications to detect possible flaws using SPIN model checker.