An Extended UML Method for the Verification of Security Protocols

被引：5

作者：

Shen, Gang ^{[1
]}

Li, Xiaohong ^{[1
]}

Feng, Ruitao ^{[1
]}

Xu, Guangquan ^{[1
]}

Hu, Jing ^{[1
]}

Feng, Zhiyong ^{[1
]}

机构：

[1] Tianjin Univ, Sch Comp Sci & Technol, Tianjin Key Lab Cognit Comp & Applicat, Tianjin 300072, Peoples R China

来源：

2014 19TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2014) | 2014年

关键词：

extended UML; confidentiality; correspondence; Spi calculus; ProVerif;

D O I：

10.1109/ICECCS.2014.12

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper presents a formal modeling method of security protocols based on the extended UML framework. In order to simplify the process and reduce the difficulty of security protocol modelling, extending mechanisms for the class diagram and sequence diagram of UML are presented, which provide an engineering specification for the security protocol formalizing. Therefore, for verifying the confidentiality and correspondence of security protocols by ProVerif, a transformation from extended UML model to ProVerif Spi calculus model is realized with matching rules and knowledge reasoning, and then the verifying results are analyzed through a regular expression. Finally, the handshake, NS public key and buyer-seller watermarking protocols are verified, the attack traces of unsatisfied security properties are exported, that show the validity and applicability of the approach provided by this paper.

引用

页码：19 / 28

页数：10

共 50 条

[1] Verification method of security model based on UML and model checking
Cheng, Liang
Zhang, Yang
Jisuanji Xuebao/Chinese Journal of Computers, 2009, 32 (04): : 699 - 708
[2] Verification of Security Protocols
Cortier, Veronique
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2009, 5403 : 5 - 13
[3] Formal modeling and verification of security protocols on cloud computing systems based on UML 2.3
Fang, Kunding
Li, Xiaohong
Hao, Jianye
Feng, Zhiyong
2016 IEEE TRUSTCOM/BIGDATASE/ISPA, 2016, : 852 - 859
[4] An improved method for formal security verification of cryptographic protocols
Watanabe, H
Fujiwara, T
Kasami, T
IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1996, E79A (07) : 1089 - 1096
[5] UML based Security Function Policy Verification Method for Requirements Specification
Noro, Atsushi
Matsuura, Saeko
2013 IEEE 37TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 2013, : 832 - 833
[6] Security software formal modeling and verification method based on UML and Z
Cao, K. (kunyucao@tju.edu.cn), 1600, Springer Verlag (332):
[7] Security Software Formal Modeling and Verification Method Based on UML and Z
Cao, Kunyu
Li, Xiaohong
Xing, Jinliang
CONTEMPORARY RESEARCH ON E-BUSINESS TECHNOLOGY AND STRATEGY, 2012, 332 : 390 - 401
[8] Verification of security protocols using LOTOS-method and application
Leduc, G
Germeau, F
COMPUTER COMMUNICATIONS, 2000, 23 (12) : 1089 - 1103
[9] Verification of randomized security protocols
Chadha, Rohit
Sistla, A. Prasad
Viswanathan, Mahesh
2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2017,
[10] Generic verification of security protocols
Khan, AS
Mukund, M
Suresh, SP
MODEL CHECKING SOFTWARE, PROCEEDINGS, 2005, 3639 : 221 - 235

← 1 2 3 4 5 →