File(s) not publicly available

Formal analysis of PANA authentication and authorisation protocol

conference contribution
posted on 04.04.2019, 00:00 by Steven Gordon
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

Start Page

277

End Page

284

Start Date

01/12/2008

Finish Date

04/12/2008

ISSN

2379-5352

ISBN-13

9780769534435

Location

Dunedin, New Zealand

Publisher

IEEE Computer Society

Place of Publication

Los Aamitos, California

Peer Reviewed

Yes

Open Access

No

Name of Conference

Ninth International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT 2008)