Modeling and verification of Extensible Authentication Protocol for Transport layer Security in Wireless LAN environment

Humayra Ali, M karim, M Ashraf, David Powers

    Research output: Contribution to conferencePaperpeer-review

    6 Citations (Scopus)

    Abstract

    Today complex edge services are positioned on the Wireless LAN, different cryptographic protocols with complex as well as reactive communication models and event dependencies are increasingly being specified and adopted. To ensure that such protocols (and compositions there of with existing protocols) do not result in unacceptable behaviors (e.g., deadlocks or live locks); a methodology is desirable for the automated checking of the "correctness" of these protocols. In this paper, we present ingredients of such a methodology. Specifically, we show how SPIN, a tool used for the formal systems verification purposes, can be used to verify as well as quickly identify problematic behaviors (if any) in core component of emergent Wireless LAN with non trivial communication authentication constructs - such as Extensible Authentication Protocol (EAP) for Transport layer Security (TLS). In our analysis, we identify essential elements, model and verify the EAP - TLS protocol using SPIN. It will evidently provide an insight into the scope and utility of formal methods based on state space exploration in testing larger and complex systems, for example, the complete Wireless LAN authentication suit.

    Original languageEnglish
    PagesV241-V245
    DOIs
    Publication statusPublished - 16 Dec 2010
    EventInternational Conference on Software Technology and Engineering -
    Duration: 3 Oct 2010 → …

    Conference

    ConferenceInternational Conference on Software Technology and Engineering
    Period3/10/10 → …

    Keywords

    • Authentication
    • Communication protocols modeling & Verification
    • EAP-TLS
    • Protocol engineering
    • Wireless LAN security

    Fingerprint

    Dive into the research topics of 'Modeling and verification of Extensible Authentication Protocol for Transport layer Security in Wireless LAN environment'. Together they form a unique fingerprint.

    Cite this