Model Checking Wireless Sensor Network Security Protocols: TinySec

Abstract. In this paper, a formal analysis of security protocols in the field of wireless sensor networks is presented. Two complementary pro-tocols, TinySec and LEAP, are modelled using the high-level formal lan-guage HLPSL, and verified using the model checking tool Avispa, where two main security properties are checked: authenticity and confidential-ity of messages. As a result of this analysis, two attacks have been found: a man-in-the-middle- attack and a type flaw attack. In both cases confi-dentiality is compromised and an intruder may obtain confidential data from a node in the network. Two solutions to these attacks are proposed in the paper. Keywords:Wireless sensor, model checking, security protocols, avispa toolbox