Formal Analysis of PANA Authentication and Authorisation Protocol

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.