## 1 Introduction  
Wireless sensor networks (WSNs) with proliferation in micro-electromechanical systems (MEMS) technology and low-cost smart sensors have emerged as a widely-deployed technology for gathering data from the environment. In recent years, many limitations of WSNs, including cost, limited processing and computing resources, and shorter battery life have been improved significantly [1]. As a result, a wide range of tiny sensors--mechanical, thermal, biological, chemical, optical and magnetic sensors--is being designed to perform various tasks [2]. Due to the versatile uses of sensor nodes, the applications of WSNs are found in military surveillance, home medical care and environmental science [3]. Typically, a node is comprised of one or more sensors that can read data from its surroundings. The read data are then transmitted to a base station, which has more computing and storage resources than a node. In general, node to base station and node to node connections are wireless connections and, thus, are publicly accessible. Since any wireless link is susceptible to attack, a WSN is inherently vulnerable to attacks from outsiders. Sensor networks face a number of security challenges, including secure routing, key establishment, secrecy, authentication, privacy, robustness and denial-of-service (DoS) attacks [4; 5]. Conventional end to end security mechanisms, such as SSH or SSL, are not possible to deploy in WSNs, due to in-network aggregation of data that requires intermediate routers to have access to the message content [6]. Moreover, sensor nodes with their low computing and storage resources are not capable of processing asymmetric cryptographic algorithms (e.g., typical RSA keys are 1024 to 2048 bits long [7]). Most of the sensor networks' routing protocols are vulnerable to some kind of attack, as these protocols have not been designed with security as a goal [6]. One exception is Security Protocols for Sensor Networks (SPINS) [8], which has been designed to meet a set of security requirements. SPINS has been designed to provide secured communication in WSNs, which is feasible for limited resources, as well. SPINS, a set of security protocols, has two building blocks: the Secure Network Encryption Protocol (SNEP) and a \"micro\" version of the Timed Efficient Streaming Loss-tolerant Authentication (TESLA) [9], named \(\upmu\)TESLA. The security requirements of SPINS protocols are summarized as follows:  
* Data confidentiality confirms that a sensor network's information, especially the readings of the sensors, is kept secret from other networks. Encryption is the most commonly-used technique for providing data confidentiality. * Data authentication confirms that data were really sent by the claimed sender. A symmetric key (shared by the sender and the receiver)-based message authentication code (MAC) ensures data authenticity. * Data integrity verifies that data have not been altered _en route_ by any adversary. MAC-based data authentication includes data integrity. * Data freshness ensures that data are recent and not replayed by an adversary. Nonces and counters are two ways to provide freshness. * Replay protection prevents an adversary from reusing an old message. * Low communication overhead is a basic security property that should be ensured by any WSN security protocols. * Semantic security confirms that no two messages are identical. This could be confirmed by sending a counter or timestamp that is modified in every message. In this paper, we have validated the security properties of SNEP by modeling the protocol using Automated Validation of Internet Security Protocols and Applications (AVISPA) [10]. AVISPA is a push-button tool with industrial-strength technology for the analysis of different Internet security protocols and applications. It is being used by the developers of different security protocols and by academic researchers, as well [11].