TY - GEN
T1 - Formalization and Verification of the PKMv3 Protocol Using CSP
AU - Xu, Yuanmin
AU - Zhu, Huibiao
AU - Zhu, Xiaoran
AU - Wu, Xi
AU - Guo, Jian
AU - Lu, Gang
N1 - Publisher Copyright:
© 2017 IEEE.
PY - 2017/9/7
Y1 - 2017/9/7
N2 - IEEE 802.16m, aiming at providing secure communication pathways between the base station (BS) and the mobile station (MS), is a broadband wireless MAN (Metropolitan Area Network) standard. Its security sublayer contains a Privacy Key Management (PKM) protocol, which achieves authentication and key management in the communication process. In this paper, we apply Communicating Sequential Processes (CSP) to formally analyze the latest version of the PKM (PKMv3) protocol. Both communication entities, i.e., the mobile station and the base station, are modelled as processes in our modelling framework. Besides, we introduce intruders in our formalization who have capabilities of intercepting, faking and overhearing. Furthermore, we employ the Process Analysis Toolkit (PAT), a model checker for CSP, to implement the entire model and then verify some non-trivial properties, such as secrecy violation and timeout freedom. With respect to the verification results, we discuss some cases where intruders may take place. Consequently, through our framework, a better understanding of the PKMv3 protocol can be achieved.
AB - IEEE 802.16m, aiming at providing secure communication pathways between the base station (BS) and the mobile station (MS), is a broadband wireless MAN (Metropolitan Area Network) standard. Its security sublayer contains a Privacy Key Management (PKM) protocol, which achieves authentication and key management in the communication process. In this paper, we apply Communicating Sequential Processes (CSP) to formally analyze the latest version of the PKM (PKMv3) protocol. Both communication entities, i.e., the mobile station and the base station, are modelled as processes in our modelling framework. Besides, we introduce intruders in our formalization who have capabilities of intercepting, faking and overhearing. Furthermore, we employ the Process Analysis Toolkit (PAT), a model checker for CSP, to implement the entire model and then verify some non-trivial properties, such as secrecy violation and timeout freedom. With respect to the verification results, we discuss some cases where intruders may take place. Consequently, through our framework, a better understanding of the PKMv3 protocol can be achieved.
KW - CSP
KW - Formalization
KW - PAT
KW - PKMv3 protocol
KW - Verification
UR - https://www.scopus.com/pages/publications/85031900856
U2 - 10.1109/COMPSAC.2017.133
DO - 10.1109/COMPSAC.2017.133
M3 - 会议稿件
AN - SCOPUS:85031900856
T3 - Proceedings - International Computer Software and Applications Conference
SP - 499
EP - 504
BT - Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017
A2 - Demartini, Claudio
A2 - Conte, Thomas
A2 - Nakamura, Motonori
A2 - Lung, Chung-Horng
A2 - Zhang, Zhiyong
A2 - Hasan, Kamrul
A2 - Reisman, Sorel
A2 - Liu, Ling
A2 - Claycomb, William
A2 - Takakura, Hiroki
A2 - Yang, Ji-Jiang
A2 - Tovar, Edmundo
A2 - Cimato, Stelvio
A2 - Ahamed, Sheikh Iqbal
A2 - Akiyama, Toyokazu
PB - IEEE Computer Society
T2 - 41st IEEE Annual Computer Software and Applications Conference, COMPSAC 2017
Y2 - 4 July 2017 through 8 July 2017
ER -