TY - GEN
T1 - Formal verification of a key agreement protocol for wireless sensor networks
AU - Li, Yue
AU - Chen, Dehua
AU - Newe, Thomas
PY - 2012
Y1 - 2012
N2 - Wireless sensor networks (WSNs) have gained much attention in both industry and research communities where they are expected to bring the interaction between humans, environment, and machines to a new level. Due to the resource constraints of sensors nodes, it is infeasible to use traditional key establishment techniques that find use in fixed communication systems. In recent years a number of group key agreement protocols have been proposed for resourcelimited wireless sensor devices. However, these protocols do not satisfy some important security properties such as mutual authentication and forward secrecy. In this paper, we propose a hybrid authenticated group key agreement protocol for WSNs. This hybrid protocol reduces the high cost public-key operations at the sensor side and replaces them with efficient symmetric-key based operations. In order to provide assurance that the proposed protocol is verifiably secure and trustworthy, a formal verification is performed on the protocol's design specification.
AB - Wireless sensor networks (WSNs) have gained much attention in both industry and research communities where they are expected to bring the interaction between humans, environment, and machines to a new level. Due to the resource constraints of sensors nodes, it is infeasible to use traditional key establishment techniques that find use in fixed communication systems. In recent years a number of group key agreement protocols have been proposed for resourcelimited wireless sensor devices. However, these protocols do not satisfy some important security properties such as mutual authentication and forward secrecy. In this paper, we propose a hybrid authenticated group key agreement protocol for WSNs. This hybrid protocol reduces the high cost public-key operations at the sensor side and replaces them with efficient symmetric-key based operations. In order to provide assurance that the proposed protocol is verifiably secure and trustworthy, a formal verification is performed on the protocol's design specification.
KW - Formal Logic
KW - Key agreement protocol
KW - Security
KW - Wireless Sensor Networks
UR - http://www.scopus.com/inward/record.url?scp=84868142192&partnerID=8YFLogxK
U2 - 10.1109/TrustCom.2012.163
DO - 10.1109/TrustCom.2012.163
M3 - Conference contribution
AN - SCOPUS:84868142192
SN - 9780769547459
T3 - Proc. of the 11th IEEE Int. Conference on Trust, Security and Privacy in Computing and Communications, TrustCom-2012 - 11th IEEE Int. Conference on Ubiquitous Computing and Communications, IUCC-2012
SP - 1537
EP - 1542
BT - Proc. of the 11th IEEE Int. Conference on Trust, Security and Privacy in Computing and Communications, TrustCom-2012 - 11th IEEE Int. Conference on Ubiquitous Computing and Communications, IUCC-2012
T2 - 11th IEEE International Conference on Trust, Security and Privacy in Computing and Communications, TrustCom-2012
Y2 - 25 June 2012 through 27 June 2012
ER -