The Extensible Authentication Protocol (EAP), which is typically used over wireless LANs and point-to-point links, allows a server to request authentication information from a client. The Protocol for Carrying Authentication for Network Access (PANA) is designed to transport EAP messages over IP networks. This paper presents a formal Coloured Petri net model and analysis of PANA, focusing on the initial Authentication and Authorisation phase. State space analysis of selected configurations reveals a deadlock may occur at the client when the server aborts a PANA authentication session. The analysis also derives a formal definition of the service between PANA and EAP, which is important for verifying that PANA correctly interfaces with EAP, and can later be used for automated testing.
Funding
Other
History
Parent Title
Proceedings: Ninth International Conference on Parallel and Distributed Computing, Applications and Technologies