Name
Abstract | ||
|---|---|---|
IEEE 802.16m, aiming at providing secure communication pathways between the base station (BS) and the mobile station (MS), is a broadband wireless MAN (Metropolitan Area Network) standard. Its security sublayer contains a Privacy Key Management (PKM) protocol, which achieves authentication and key management in the communication process. In this paper, we apply Communicating Sequential Processes (CSP) to formally analyze the latest version of the PKM (PKMv3) protocol. Both communication entities, i.e., the mobile station and the base station, are modelled as processes in our modelling framework. Besides, we introduce intruders in our formalization who have capabilities of intercepting, faking and overhearing. Furthermore, we employ the Process Analysis Toolkit (PAT), a model checker for CSP, to implement the entire model and then verify some non-trivial properties, such as secrecy violation and timeout freedom. With respect to the verification results, we discuss some cases where intruders may take place. Consequently, through our framework, a better understanding of the PKMv3 protocol can be achieved. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/COMPSAC.2017.133 | 2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC) |
Keywords | Field | DocType |
PKMv3 protocol,Formalization,Verification,CSP,PAT | Key management,Base station,Authentication,Computer science,Mobile station,Communicating sequential processes,Computer network,Metropolitan area network,Secure communication,Mobile telephony,Distributed computing | Conference |
Volume | ISSN | ISBN |
1 | 0730-3157 | 978-1-5386-0368-0 |
Citations | PageRank | References |
1 | 0.35 | 4 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yuanmin Xu | 1 | 4 | 1.76 |
| Huibiao Zhu | 2 | 583 | 86.68 |
| Xiaoran Zhu | 3 | 17 | 3.22 |
| Xi Wu | 4 | 37 | 9.97 |
| Jian Guo | 5 | 2 | 2.06 |
| Gang Lu | 6 | 2 | 1.39 |