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 acrossauthentication methods. EAP supportsmultiple authentication methods. In this paper, we have modelled the ExtensibleAuthenticationProtocolasa finite state machine. The various entities in our model are Authenticator, EAP Server, User and UserDatabase.The messages exchanged between various entities are modelled as transitions. The model isrepresented in PROMELA.The model is checked for conformance with its specifications todetectpossible flawsusingSPINmodel checker