Proof of the Secrecy Property of Secure WLAN Authentication Scheme (SWAS) using Extended Protocol Composition Logic
Rajeev Singh, Teek Parval Sharma · Journal of Textile Science & Engineering · 2013
An effective and secure key exchange is one of the essential feature of a secure communication. Secure WLAN Authentication Scheme (SWAS) is one such mechanism that involves cryptographic operations for providing a secure key exchange. The scheme not only provide entity authentication but also provide authentication to the individual frames involved. It evolves fresh keys for securing data sessions. It enhances the network performance by reducing the number of messages required for authentication and key exchange. The protocol enhances reliability of the WLAN communication system and hence its properties need to be validated. Extended Protocol Composition Logic (PCL) is a formal method used extensively for validating the security properties of a protocol. In this paper, we utilize it for proving the secrecy property of SWAS. Thus, main contribution of the paper is presentation of formal proof for the secrecy property of the SWAS scheme.