Formal verification of a radio network random access protocol

被引：4
作者：
Roumane, Ahmed [1 ]
Kechar, Bouabdellah [1 ]
Kouninef, Belkacem [2 ]
机构：
[1] Univ Oran1 Ahmed Ben Bella, Fac Sci Exactes & Appl, Dept Informat, Lab Informat Ind & Reseaux RIIR, BP1524, El Mnaouer Oran, Algeria
[2] Natl Inst Telecommun & ICT INTTIC, LARATIC, BP 1518, El Mnaouer Oran, Algeria
来源：
INTERNATIONAL JOURNAL OF COMMUNICATION SYSTEMS | 2017年 / 30卷 / 18期
关键词：
formal verification; model checking; random access procedure; spin; UMTS; UPPAAL; SECURITY PROTOCOL;
D O I：
10.1002/dac.3447
中图分类号：
TM [电工技术]; TN [电子技术、通信技术];
学科分类号：
0808 ; 0809 ;
摘要：
In this paper, the random access procedure of Universal Mobile Telecommunications System network is investigated. We have proposed a model based on communicating timed automata that represents the main functions related to the random access procedure including the user equipment, the base station (node B or BTS), and the channel. Then, we have used computational tree logic formula to specify the proprieties to be verified. The model and the formulas serve as inputs to the model checker, which is used as a verification engine, ie, UPPAAL and SPIN. The formal verification approach shows that the protocol has several drawbacks that may not be detected by simulation.
引用
收藏
页数：18
相关论文
共 26 条
[1]  
*3GPP TS, 25214 3GPP TS
[2]  
[Anonymous], 2014, 25321 3GPP TS
[3]  
[Anonymous], 2014, 25214 3GPP TS
[4]   Formal verification of security protocol implementations: a survey [J].
Avalle, Matteo ;
Pironti, Alfredo ;
Sisto, Riccardo .
FORMAL ASPECTS OF COMPUTING, 2014, 26 (01) :99-123
[5]   Designing and verifying a P2P service security protocol in M2M environment [J].
Bae, Woo-Sik .
PEER-TO-PEER NETWORKING AND APPLICATIONS, 2016, 9 (03) :539-545
[6]  
Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
[7]  
Behrmann G., 2006, TUTORIAL UPPAAL 4 0
[8]  
Bharti MV., 2012, INT J SCI RES PUBLIC, V2, P228
[9]  
Bosnacki D, 1998, FORTE PSTV 18 C KLUW
[10]  
Chen H., 2016, P 37 ACM SIGPLAN C P
123