Formal Analysis of Sensor Network Encryption Protocol (SNEP)

In this paper, a formal analysis of a security protocol in the field of wireless sensor networks is presented. Sensor network encryption protocol (SNEP) describes basic primitives for providing confidentiality, authentication between two nodes, data integrity and weak message freshness in a wireless sensor network. It was designed as base component of security protocols for sensor networks (SPINS). SNEP is modelled in two scenarios using the high-level formal language HLPSL, and verified using the model checking tool Avispa, where two main security properties are checked: authenticity and confidentiality of relevant messages components. The first case is the communication between the base station and networks nodes in order to retrieve node confidential information. The second case is a key distribution protocol in a sensor network using SNEP for securing messages. As a result of this analysis, one attack have been found: a false request message from an intruder. In that case, the intruder impersonates the base station and creates false requests. This way, the intruder may obtain confidential data from a node in the network. A solution to this attack is proposed in the paper.