Algebraic Formalization and Verification of PKMv3 Protocol using Maude
Jia She, Xiaoran Zhu, Min Zhang · Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge Engineering · 2017
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.