Modeling Source Authentication Protocols in Wireless Sensor Networks Using HLPSL

Wireless sensor networks (WSNs) are being widely deployed in military, healthcare, and commercial environments. Because sensor networks pose unique challenges, traditional security methods, commonly used in enterprise networks, cannot be directly applied. In particular, broadcast source authentication is a critical security requirement in wireless sensor networks. Therefore, formal validation of source authentication protocols in wireless sensor networks has become an important research topic. The Multi-Level-μTESLA, Staggered Multi-Level-μTESLA, and Bloom Filter based source authentication protocols are potential candidates for source authentication in WSNs but so far, there has been no formal validation of those protocols. In this paper, we aim to formally verify and model those three authentication protocols using the AVISPA model-checking tool and HLPSL language. We show that those protocols can safely be used for source authentication. We also show that those three protocols exhibit also some DoS attack problems which are hard to eliminate.