On the Formal Verification of the SNEP Key Agreement Protocol for Wireless Sensor Networks

Wireless Sensor Networks (WSNs) are expected to play an essential role in the age of pervasive computing. Wide deployments of mission-critical WSNs create concerns about security issues. Security of large scale densely deployed and infrastructure-less wireless networks of resource limited sensor nodes requires efficient key distribution protocols. Perring et al. developed SNEP capable of providing several security services, such as data confidentiality, data authentication, and data freshness. In order to provide assurance that these protocols are verifiable secure and trustworthy it is necessary to perform a formal verification on their design specification. The formal logic of Coffey-Saidha-Newe (CSN) combines the logic of belief and knowledge to evaluate trust and security of communication protocols. In this paper the SNEP key agreement protocol is discussed. A formal verification of SNEP key agreement using the CSN modal logic is presented. Some additional axioms relating to MAC authentication are also presented and used to simplify the verification of protocols that involve MAC authentication.