TY - GEN
T1 - Algebraic formalization and verification of PKMv3 protocol using maude
AU - She, Jia
AU - Zhu, Xiaoran
AU - Zhang, Min
PY - 2017
Y1 - 2017
N2 - PKMv3 is the third version of Privacy and Key Management protocol, which plays an important role by providing key distribution and security access control in IEEE802.16m, the standard of Worldwide Interoperability for Microwave Access. The protocol should be guaranteed safe in terms of confidentiality, authentication and integrity. In this paper, we develop an executable formal specification of PKMv3 in an algebraic language called Maude and verify safety properties of the protocol using state exploration and LTL model checking in Maude. Unlike existing approaches, we consider the behaviors of intruders and time feature in our verification and verify both safety properties and time-related properties of the protocol.
AB - PKMv3 is the third version of Privacy and Key Management protocol, which plays an important role by providing key distribution and security access control in IEEE802.16m, the standard of Worldwide Interoperability for Microwave Access. The protocol should be guaranteed safe in terms of confidentiality, authentication and integrity. In this paper, we develop an executable formal specification of PKMv3 in an algebraic language called Maude and verify safety properties of the protocol using state exploration and LTL model checking in Maude. Unlike existing approaches, we consider the behaviors of intruders and time feature in our verification and verify both safety properties and time-related properties of the protocol.
UR - https://www.scopus.com/pages/publications/85029527213
U2 - 10.18293/SEKE2017-061
DO - 10.18293/SEKE2017-061
M3 - 会议稿件
AN - SCOPUS:85029527213
T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
SP - 167
EP - 172
BT - Proceedings - SEKE 2017
PB - Knowledge Systems Institute Graduate School
T2 - 29th International Conference on Software Engineering and Knowledge Engineering, SEKE 2017
Y2 - 5 July 2017 through 7 July 2017
ER -