A Formal Description and Verification of Authentication Protocol

被引:0
作者
Yuan, Zhanting [1 ]
Kang, Xu [1 ]
Zhang, Qiuyu [1 ]
Liang, Shuang [1 ]
机构
[1] Lanzhou Univ Technol, Coll Comp & Commun, Lanzhou 730050, Gansu, Peoples R China
来源
DCABES 2008 PROCEEDINGS, VOLS I AND II | 2008年
关键词
Identity Authentication Protocol; Petri Net; Reachable Tree; Reachable Analysis; Security;
D O I
暂无
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Identity authentication, as the first step to realize the network security, is the key technology for secure exchange of the online commercial information. Moreover, if there is any leak in the authentication protocol, secret information will leak out consequentially. It is necessary to adopt some formalized method to describe and prove the authentication protocol. In this paper the colored Petri. Net is employed to describe the authentication protocol, and simultaneously the combined strategy of 1-reachable analysis and conversing analysis has been put forward to verify the security of this authentication protocol.
引用
收藏
页码:735 / 740
页数:6
相关论文
共 50 条
[21]   Formal Verification and Improvement of the PKMv3 Protocol Using CSP [J].
Jiang, Jinpeng ;
Mao, Hongyan ;
Shaol, Rumeng ;
Xu, Yuanmin .
2018 IEEE 42ND ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC 2018), VOL 2, 2018, :682-687
[22]   Formal Verification of 5G EAP-AKA protocol [J].
Ajit, Megha ;
Sankaran, Sriram ;
Jain, Kurunandan .
2021 31ST INTERNATIONAL TELECOMMUNICATION NETWORKS AND APPLICATIONS CONFERENCE (ITNAC), 2021, :140-146
[23]   Formal Modeling and Verification of a Blockchain-Based Crowdsourcing Consensus Protocol [J].
Afzaal, Hamra ;
Imran, Muhammad ;
Janjua, Muhammad Umar ;
Gochhayat, Sarada Prasad .
IEEE ACCESS, 2022, 10 :8163-8183
[24]   Formal analysis of RFC 8120 authentication protocol for HTTP under different assum ptions ? [J].
Okumura, Naomi ;
Ogata, Kazuhiro ;
Shinoda, Yoichi .
JOURNAL OF INFORMATION SECURITY AND APPLICATIONS, 2020, 53
[25]   Formal Verification and Performance Analysis of a New Data Exchange Protocol for Connected Vehicles [J].
Chouali, Samir ;
Boukerche, Azzedine ;
Mostefaoui, Ahmed ;
Merzoug, Mohammed Amine .
IEEE TRANSACTIONS ON VEHICULAR TECHNOLOGY, 2020, 69 (12) :15385-15397
[26]   SSMBP: A Secure SMS-based Mobile Banking Protocol with Formal Verification [J].
Bojjagani, Sriramulu ;
Sastry, V. N. .
2015 IEEE 11TH INTERNATIONAL CONFERENCE ON WIRELESS AND MOBILE COMPUTING, NETWORKING AND COMMUNICATIONS (WIMOB), 2015, :252-259
[27]   Formal Verification of the mERA-Based eServices with Trusted Third Party Protocol [J].
Christofi, Maria ;
Gouget, Aline .
INFORMATION SECURITY AND PRIVACY RESEARCH, 2012, 376 :299-312
[28]   Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method [J].
Ouranos, Iakovos ;
Stefaneas, Petros ;
Ogata, Kazuhiro .
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT I, 2010, 6415 :75-+
[29]   Formal Analysis of 5G EAP-TLS Authentication Protocol Using Proverif [J].
Zhang, Jingjing ;
Yang, Lin ;
Cao, Weipeng ;
Wang, Qiang .
IEEE ACCESS, 2020, 8 :23674-23688
[30]   AUTHENTICATION BY BIOMETRIC VERIFICATION INTRODUCTION [J].
Vetter, Ron .
COMPUTER, 2010, 43 (02) :28-29