TY - GEN
T1 - Formal Verification of PKMv3 Protocol Using DT-Spin
AU - Zhu, Xiaoran
AU - Xu, Yuanmin
AU - Guo, Jian
AU - Wu, Xi
AU - Zhu, Huibiao
AU - Miao, Weikai
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2015/10/26
Y1 - 2015/10/26
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 version (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. Discrete time describes the lifetime of the Authorization Key (AK) and the Transmission Encryption Key (TEK), which are produced by BS. 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 some properties are verified, i.e. liveness, succession and message consistency, which are extracted from PKMv3 and specified using Linear Temporal Logic (LTL) formulae and assertions. Our model provides a basis for further verification of PKMv3 protocol with time characteristic.
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 version (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. Discrete time describes the lifetime of the Authorization Key (AK) and the Transmission Encryption Key (TEK), which are produced by BS. 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 some properties are verified, i.e. liveness, succession and message consistency, which are extracted from PKMv3 and specified using Linear Temporal Logic (LTL) formulae and assertions. Our model provides a basis for further verification of PKMv3 protocol with time characteristic.
KW - DT-Spin
KW - Discrete-time PROMELA
KW - PKMv3 protocol
KW - modeling
KW - verification
UR - https://www.scopus.com/pages/publications/84958149879
U2 - 10.1109/TASE.2015.20
DO - 10.1109/TASE.2015.20
M3 - 会议稿件
AN - SCOPUS:84958149879
T3 - Proceedings - 2015 International Symposium on Theoretical Aspects of Software Engineering, TASE 2015
SP - 71
EP - 78
BT - Proceedings - 2015 International Symposium on Theoretical Aspects of Software Engineering, TASE 2015
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - International Symposium on Theoretical Aspects of Software Engineering, TASE 2015
Y2 - 12 September 2015 through 14 September 2015
ER -