Title
Formal Verification and Improvement of the PKMv3 Protocol Using CSP.
Abstract
WiMAX (Worldwide Interoperability for Microwave Access) is the standard of broadband wireless MAN (Metropolitan Area Network) which aims at providing secure communication pathways between the base station (BS) and the subscriber station (SS). The security sublayer within IEEE 802.16m MAC layer contains a Privacy Key Management (PKM) protocol, which provides authentication and key management. There are attacks in the latest version of the PKM (PKMv3) protocol. In order to defend Man-in-the-Middle attacks, two methods are proposed and formally verified using Communicating Sequential Processes (CSP) in this paper. Both BS and SS are modeled as processes in our framework. Not only the time characteristic is introduced but also the intruder who can falsify the message is depicted. In addition, the Process Analysis Toolkit (PAT) is used to verify some important properties such as confidentiality, integrity and availability, and detect potential attacks from intruders. In order to increase the functionality of existing models, two improved approaches against attacks are given, the one by encrypting the digital signature, the other by improving the checksum algorithm. The verification results show that a more secure PKMv3 protocol can be achieved through our modeling.
Year
Venue
Field
2018
COMPSAC
Key management,Checksum,Authentication,Computer science,Cryptography,Communicating sequential processes,Computer network,Encryption,Digital signature,Real-time computing,Secure communication
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
0
4
Name
Order
Citations
PageRank
Jinpeng Jiang100.34
Hongyan Mao201.35
Rumeng Shao300.34
Yuanmin Xu441.76