Model checking wireless sensor network security protocols: TinySec + LEAP

Abstract

In this paper, a formal analysis of security protocols in the field of wireless sensor networks is presented. Two complementary protocols, TinySec and LEAP, are modelled 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 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 confidentiality 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. © 2007 International Federation for Information Processing.