A Semantic Analysis of Key Management Protocols for Wireless Sensor Networks

2011/09/23 by Francesco Ballardin, Damiano Macedonio, Ballardin, Francesco +5
Computer Science · #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Networking and Internet Architecture (cs.NI) #cs.CR #cs.NI

paper · pdf · doi:10.48550/arxiv.1109.5088

51 pages

arxiv created 2011/09/23 · arxiv updated 2015/03/19

Abstract

We propose a simple timed broadcasting process calculus for modelling wireless network protocols. The operational semantics of our calculus is given in terms of a labelled transition semantics which is used to derive a standard (weak) bi-simulation theory. Based on our simulation theory, we reformulate Gorrieri and Martinelli's timed Generalized Non-Deducibility on Compositions (tGNDC) scheme, a well-known general framework for the definition of timed properties of security protocols. We use tGNDC to perform a semantic analysis of three well-known key management protocols for wireless sensor networks: μTESLA, LEAP+ and LiSP. As a main result, we provide a number of attacks to these protocols which, to our knowledge, have not yet appeared in the literature.

Related

• Analysing ZigBee Key Establishment Protocols
• Protocol Analysis with Time
• Information-Theoretic Security in Wireless Networks
• Cryptography and Key Management Schemes for Wireless Sensor Networks
• How not to secure wireless sensor networks revisited: Even if you say it twice it's still not secure