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 条

[41] Comprehensive Formal Verification of an OS Microkernel [J].

Klein, Gerwin ;

Andronick, June ;

Elphinstone, Kevin ;

Murray, Toby ;

Sewell, Thomas ;

Kolanski, Rafal ;

Heiser, Gernot .

ACM TRANSACTIONS ON COMPUTER SYSTEMS, 2014, 32 (01)

[42] Formal Verification of BNB Smart Contract [J].

Li, Xiaoyu ;

Su, Cheng ;

Xiong, Yan ;

Huang, Wenchao ;

Wang, Wansen .

5TH INTERNATIONAL CONFERENCE ON BIG DATA COMPUTING AND COMMUNICATIONS (BIGCOM 2019), 2019, :74-78

[43] Formal Verification and Security Analysis of AMQP [J].

Liu, Huiying ;

Dong, Wenting ;

Zhu, Huibiao ;

Su, Ziqing .

2024 IEEE 48TH ANNUAL COMPUTERS, SOFTWARE, AND APPLICATIONS CONFERENCE, COMPSAC 2024, 2024, :2177-2182

[44] A Framework for Formal Verification of DRAM Controllers [J].

Steiner, Lukas ;

Sudarshan, Chirag ;

Jung, Matthias ;

Stoffel, Dominik ;

Wehn, Norbert .

PROCEEDINGS OF THE INTERNATIONAL SYMPOSIUM ON MEMORY SYSTEMS, MEMSYS 2022, 2022,

[45] Equational approach to formal verification of SET [J].

Ogata, K ;

Futatsugi, K .

QSIC 2004: PROCEEDINGS OF THE FOURTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE, 2004, :50-59

[46] Towards Formal Verification of Program Obfuscation [J].

Lu, Weiyun ;

Sistany, Bahman ;

Felty, Amy ;

Scott, Philip .

2020 IEEE EUROPEAN SYMPOSIUM ON SECURITY AND PRIVACY WORKSHOPS (EUROS&PW 2020), 2020, :635-644

[47] A Formal Verification Method for the SOPC Software [J].

Zhou, Shan ;

Wang, Jinbo ;

Jia, Jiao ;

Zhang, Chi ;

Wang, Ruixue .

IEEE TRANSACTIONS ON RELIABILITY, 2022, 71 (02) :818-829

[48] Formal automatic verification of security protocols [J].

Xiao, Meihua ;

Xue, Jinyun .

2006 IEEE INTERNATIONAL CONFERENCE ON GRANULAR COMPUTING, 2006, :566-+

[49] A Secure Authentication System for ePassport Detection and Verification [J].

Hamad, Fadi ;

Zraqou, Jamal ;

Maiita, Adi ;

Abu Taleb, Anas .

2015 EUROPEAN INTELLIGENCE AND SECURITY INFORMATICS CONFERENCE (EISIC), 2015, :173-176

[50] Digital Signature Verification Scheme for Image Authentication [J].

Singh, Manpreet ;

Kaur, Harpreet ;

Kakkar, Ajay .

2015 2ND INTERNATIONAL CONFERENCE ON RECENT ADVANCES IN ENGINEERING & COMPUTATIONAL SCIENCES (RAECS), 2015,

← 1 2 3 4 5 →