A formal analysis method for composition protocol based on model checking

被引：3
|
作者：
Xiao, Meihua [1 ]
Zhao, Hanyu [1 ]
Yang, Ke [1 ]
Ri Ouyang [1 ]
Song, Weiwei [1 ]
机构：
[1] East China Jiaotong Univ, Sch Software, Nanchang 330013, Jiangxi, Peoples R China
来源：
SCIENTIFIC REPORTS | 2022年 / 12卷 / 01期
基金：
中国国家自然科学基金;
关键词：
AUTHENTICATION; VERIFICATION; SECURITY;
D O I：
10.1038/s41598-022-12448-2
中图分类号：
O [数理科学和化学]; P [天文学、地球科学]; Q [生物科学]; N [自然科学总论];
学科分类号：
07 ; 0710 ; 09 ;
摘要：
Protocol security in a composition protocol environment has always been an open problem in the field of formal analysis and verification of security protocols. As a well-known tool to analyze and verify the logical consistency of concurrent systems, SPIN (Simple Promela Interpreter) has been widely used in the analysis and verification of the security of a single protocol. There is no special research on the verification of protocol security in a composition protocol environment. To solve this problem, firstly, a formal analysis method for composition protocol based on SPIN is proposed, and a formal description of protocol operation semantics is given. Then the attacker model is formalized, and a message specification method based on field detection and component recognition is presented to alleviate the state explosion problem. Finally, the NSB protocol and the NSL protocol are used as examples for compositional analysis. It is demonstrated that the proposed method can effectively verify the security of the protocol in a composition protocol environment and enhance the efficiency of composition protocol verification.
引用
收藏
页数：18
相关论文
共 50 条
  • [41] Formal analysis of production line systems by probabilistic model checking tools
    Ballarini, Paolo
    Horvath, Andras
    [J]. 2021 26TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2021,
  • [42] Formal analysis of DeGroot Influence Problems using probabilistic model checking
    Gyftopoulos, Sotirios
    Efraimidis, Pavlos S.
    Katsaros, Panagiotis
    [J]. SIMULATION MODELLING PRACTICE AND THEORY, 2018, 89 : 144 - 159
  • [43] Formal security analysis of near field communication using model checking
    Alexiou, Nikolaos
    Basagiannis, Stylianos
    Petridou, Sophia
    [J]. COMPUTERS & SECURITY, 2016, 60 : 1 - 14
  • [44] A Formal Algorithm for Verifying the Validity of Clustering Results Based on Model Checking
    Huang, Shaobin
    Cheng, Yuan
    Lang, Dapeng
    Chi, Ronghua
    Liu, Guofeng
    [J]. PLOS ONE, 2014, 9 (03):
  • [45] A Formal Model and Analysis of the MQ Telemetry Transport Protocol
    Aziz, Benjamin
    [J]. 2014 NINTH INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY AND SECURITY (ARES), 2015, : 59 - 68
  • [46] Analysis on EURORADIO Safety Critical Protocol by Probabilistic Model Checking
    Quan Hongyu
    Zhao Huibing
    Zhou Guo
    [J]. 2013 IEEE INTERNATIONAL CONFERENCE ON INTELLIGENT RAIL TRANSPORTATION (ICIRT), 2013, : 75 - 78
  • [47] Dynamic protocol implementation model based on protocol composition
    College of Computer, Nanjing University of Posts and Telecommunications, Nanjing 210003, China
    不详
    [J]. Nanjing Youdian Daxue Xuebao (Ziran Kexue Ban), 2007, 3 (12-17):
  • [48] Symbolic Model Checking and Analysis for E-Commerce Protocol
    文静华
    张梅
    李祥
    [J]. Journal of Electronic Science and Technology, 2005, (03) : 213 - 217
  • [49] Formal Verification for Interaction Protocol in Agent-Based E-Learning System Using Model Checking Toolkit - MCMAS
    Latif, Norizal Abd
    Hassan, Mohd Fadzil
    Hasan, Mohd Hilmi
    [J]. SOFTWARE ENGINEERING AND COMPUTER SYSTEMS, PT 2, 2011, 180 : 412 - 426
  • [50] Efficient Model Checking of Network Authentication Protocol Based on SPIN
    Tan, Zhi-hua
    Zhang, Da-fang
    Miao, Li
    Zhao, Dan
    [J]. INTERNATIONAL CONFERENCE ON GRAPHIC AND IMAGE PROCESSING (ICGIP 2012), 2013, 8768
12345