DocumentCode
1688531
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
fYear
2011
Firstpage
247
Lastpage
250
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/TASE.2011.10
Filename
6042088
Link To Document