TY - GEN
T1 - Modeling and analyzing the μTESLA protocol using CSP
AU - Wang, Mengying
AU - Zhu, Huibiao
AU - Zhao, Yongxin
AU - Liu, Si
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/80055102177
U2 - 10.1109/TASE.2011.10
DO - 10.1109/TASE.2011.10
M3 - 会议稿件
AN - SCOPUS:80055102177
SN - 9780769545066
T3 - Proceedings - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
SP - 247
EP - 250
BT - Proceedings - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
T2 - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
Y2 - 29 August 2011 through 31 August 2011
ER -