Title: Formal security analysis and verification of a password-based user authentication scheme for hierarchical wireless sensor networks
Authors: Ashok Kumar Das; Santanu Chatterjee; Jamuna Kanta Sing
Addresses: Center for Security, Theory and Algorithmic Research, International Institute of Information Technology, Hyderabad 500 032, India ' Research Center Imarat, Defence Research and Development Organization, Hyderabad 500 069, India ' Department of Computer Science and Engineering, Jadavpur University, Kolkata 700 032, India
Abstract: In 2012, Das et al. proposed a new password-based remote user authentication scheme in hierarchical wireless sensor networks (HWSNs). The proposed scheme achieves better security and efficiency as compared to those for other existing password-based schemes proposed in HWSNs. In this paper, we first analyse Das et al.'s scheme for formal security under the random oracle models to show their scheme is secure. Furthermore, we simulate this proposed scheme for formal security verification using the widely-accepted automated validation of internet security protocols and applications (AVISPA) tool. Using the AVISPA model checkers, we show that Das et al.'s scheme is also secure against possible passive and active attacks, including the replay and man-in-the-middle attacks. In addition, we also simulate the existing password-based schemes for formal security verification using AVISPA tool and provide a comparison among Das et al.'s scheme and other schemes. It is shown that Das et al.'s scheme outperforms other existing approaches.
Keywords: wireless sensor networks; hierarchical WSNs; user authentication; smart cards; AVISPA; formal security; random oracle model; password based authentication; simulation; replay attacks; man-in-the-middle attacks; security verification; network security.
International Journal of Trust Management in Computing and Communications, 2014 Vol.2 No.1, pp.78 - 102
Received: 25 Oct 2013
Accepted: 10 Nov 2013
Published online: 09 Jul 2014 *