Key exchange protocol for Wireless Sensor Network: Formal verification using CSN modal logic

Due to the growth of Wireless Sensor Networks (WSN), many advanced applications such as industry process monitoring, patient monitoring and public service communications have been deployed. Security of data will be an important factor for their full adoption. Efficient key exchange protocols are required for Security of large scale densely deployed wireless networks of resource limited sensor nodes. Huang et al. proposed a hybrid authenticated key exchange protocol for secure communication between a sensor and a security manager in WSN. In order to provide assurance that these protocols are verifiably secure and trustworthy it is necessary to perform a formal verification on their design specifications. In this paper Huang et al. ´s protocol is discussed and a formal verification is performed using the Coffey-Saidha-Newe (CSN) modal logic. As a result of this verification a modification is suggested to improve the protocol security.