Security Property Validation of the Sensor Network Encryption Protocol (SNEP)

Computers

Salekul Islam¹ 

[1] Department of Computer Science and Engineering, United International University, Dhaka 1209, Bangladesh; E-Mail

关键词: wireless sensor networks (WSN);    Secure Network Encryption Protocol (SNEP);    key distribution;    strong freshness;    validating security protocols;    AVISPA;    DoS attack;   

DOI  :  10.3390/computers4030215

来源: mdpi

【 摘 要 】

Since wireless sensor networks (WSNs) have been designed to be deployed in an unsecured, public environment, secured communication is really vital for their wide-spread use. Among all of the communication protocols developed for WSN, the Security Protocols for Sensor Networks (SPINS) is exceptional, as it has been designed with security as a goal. SPINS is composed of two building blocks: Secure Network Encryption Protocol (SNEP) and the “micro” version of the Timed Efficient Streaming Loss-tolerant Authentication (TESLA), named μTESLA. From the inception of SPINS, a number of efforts have been made to validate its security properties. In this paper, we have validated the security properties of SNEP by using an automated security protocol validation tool, named AVISPA. Using the protocol specification language, HLPSL, we model two combined scenarios—node to node key agreement and counter exchange protocols—followed by data transmission. Next, we validate the security properties of these combined protocols, using different AVISPA back-ends. AVISPA reports the models we have developed free from attacks. However, by analyzing the key distribution sub-protocol, we find one threat of a potential DoS attack that we have demonstrated by modeling in AVISPA. Finally, we propose a modification, and AVISPA reports this modified version free from the potential DoS attack.

【 授权许可】

CC BY   
© 2015 by the authors; licensee MDPI, Basel, Switzerland.