TY - JOUR
T1 - Formal Analysis of the PKMv3 Protocol
AU - Zhu, Xiaoran
AU - Xu, Yuanmin
AU - Li, Xin
AU - Guo, Jian
AU - Zhu, Huibiao
AU - Cong Vinh, Phan
N1 - Publisher Copyright:
© 2017, Springer Science+Business Media, LLC.
PY - 2018/2/1
Y1 - 2018/2/1
N2 - WiMax (Worldwide Interoperability for Microwave Access, IEEE 802.16) is a standard-based wireless technology, which uses Privacy Key Management (PKM) protocol to provide authentication and key management. Three versions of PKM protocol have been released and the third one (PKMv3) strengthens the security by enhancing the message management. In this paper, a formal analysis of PKMv3 protocol is presented. Both the Subscriber Station (SS) and the Base Station (BS) are modeled as processes in our framework. Besides, we introduce an intruder model where the intruder has capabilities of overhearing, intercepting and faking messages. Discrete time describes the lifetime of the Authorization Key (AK) and the Transmission Encryption Key (TEK). Moreover, the PKMv3 model is constructed through the discrete-time PROMELA (DT-PROMELA) language and the tool DT-Spin implements the PKMv3 model with lifetime. Finally, we simulate communications between SS and BS and verify some properties, such as liveness, succession and message consistency, which are extracted from the PKMv3 protocol and specified using Linear Temporal Logic (LTL) formulae and assertions. The simulation and verification results demonstrate that the attacks may exist in our model of the PKMv3 protocol.
AB - WiMax (Worldwide Interoperability for Microwave Access, IEEE 802.16) is a standard-based wireless technology, which uses Privacy Key Management (PKM) protocol to provide authentication and key management. Three versions of PKM protocol have been released and the third one (PKMv3) strengthens the security by enhancing the message management. In this paper, a formal analysis of PKMv3 protocol is presented. Both the Subscriber Station (SS) and the Base Station (BS) are modeled as processes in our framework. Besides, we introduce an intruder model where the intruder has capabilities of overhearing, intercepting and faking messages. Discrete time describes the lifetime of the Authorization Key (AK) and the Transmission Encryption Key (TEK). Moreover, the PKMv3 model is constructed through the discrete-time PROMELA (DT-PROMELA) language and the tool DT-Spin implements the PKMv3 model with lifetime. Finally, we simulate communications between SS and BS and verify some properties, such as liveness, succession and message consistency, which are extracted from the PKMv3 protocol and specified using Linear Temporal Logic (LTL) formulae and assertions. The simulation and verification results demonstrate that the attacks may exist in our model of the PKMv3 protocol.
KW - DT-PROMELA
KW - DT-Spin
KW - Linear temporal logic
KW - PKMv3
UR - https://www.scopus.com/pages/publications/85029696610
U2 - 10.1007/s11036-017-0903-0
DO - 10.1007/s11036-017-0903-0
M3 - 文章
AN - SCOPUS:85029696610
SN - 1383-469X
VL - 23
SP - 44
EP - 56
JO - Mobile Networks and Applications
JF - Mobile Networks and Applications
IS - 1
ER -