Title :
Modeling and Analyzing the (mu)TESLA Protocol Using CSP
Author :
Wang, Mengying ; Zhu, Huibiao ; Zhao, Yongxin ; Liu, Si
Author_Institution :
Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai, China
Abstract :
In this paper, we investigate the μTESLA protocol and analyze its broadcast authentication property using process algebra CSP. All the communication entities of the protocol involving the base station, the sensors and the intruder are modeled as CSP processes respectively. Besides, we also produce a CSP description of the protocol specification in our framework. Our verification result demonstrates the correctness of the protocol and the satisfaction toward the broadcast authentication property.
Keywords :
formal specification; process algebra; protocols; telecommunication computing; telecommunication security; wireless sensor networks; μTESLA protocol; CSP process algebra; broadcast authentication property; communicating sequential process; protocol specification; wireless sensor network; Authentication; Base stations; Broadcasting; Protocols; Receivers; Sensors;
Conference_Titel :
Theoretical Aspects of Software Engineering (TASE), 2011 Fifth International Symposium on
Conference_Location :
Xi´an, Shaanxi
Print_ISBN :
978-1-4577-1487-0
DOI :
10.1109/TASE.2011.10
