Portal de Periódicos da CAPES

Modelling and Verification of Extensible Authentication Protocol Using Spin Model Checker

2012; Volume: 4; Issue: 6 Linguagem: Inglês

10.5121/ijnsa.2012.4606

0975-2307

Manu S. Hegde,

Security and Verification in Computing

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, we have modelled the Extensible Authentication Protocol as a finite state machine. The various entities in our model are Authenticator, EAP Server, User and User Database. The messages exchanged between various entities are modelled 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.