Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra

Ailun Liu; Huibiao Zhu; Yuan Fei; Shuangqing Xiang; Gang Lu; Wanling Xie

doi:10.1109/COMPSAC.2017.170

Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra

Ailun Liu
, Huibiao Zhu^*
, Yuan Fei
, Shuangqing Xiang
, Gang Lu
, Wanling Xie

^*此作品的通讯作者

软件工程学院

East China Normal University

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

摘要

The security protocol is proposed as a security solution for end-to-end communication between smart grid applications in the EU FP7 project C-DAX. Since the importance and widespread use of the security protocol, it is of great significance to formally analyze and verify relevant security properties of this security protocol. In this paper, we apply Communicating Sequential Processes (CSP) to model the security protocol. Further, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for the specification and relevant secure properties, e.g. reachability of the fake goal. Our modeling and verification show that a risk may exist in the security protocol.

源语言	英语
主期刊名	Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017
编辑	Sorel Reisman, Sheikh Iqbal Ahamed, Claudio Demartini, Thomas Conte, Ling Liu, William Claycomb, Motonori Nakamura, Edmundo Tovar, Stelvio Cimato, Chung-Horng Lung, Hiroki Takakura, Ji-Jiang Yang, Toyokazu Akiyama, Zhiyong Zhang, Kamrul Hasan
出版商	IEEE Computer Society
页	39-44
页数	6
ISBN（电子版）	9781538603673
DOI	https://doi.org/10.1109/COMPSAC.2017.170
出版状态	已出版 - 7 9月 2017
活动	41st Annual IEEE Computer Software and Applications Conference, COMPSAC 2017 - Torino, 意大利期限: 4 7月 2017 → 8 7月 2017

丛书

姓名	Proceedings - International Computer Software and Applications Conference
卷	1
ISSN（印刷版）	0730-3157

会议

会议	41st Annual IEEE Computer Software and Applications Conference, COMPSAC 2017
国家/地区	意大利
市	Torino
时期	4/07/17 → 8/07/17

联合国可持续发展目标

此成果有助于实现下列可持续发展目标：

可持续发展目标 7 经济适用的清洁能源

访问文件

10.1109/COMPSAC.2017.170

其它文件与链接

链接到 Scopus 的出版物

引用此

Liu, A., Zhu, H., Fei, Y., Xiang, S., Lu, G., & Xie, W. (2017). Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra. 在 S. Reisman, S. I. Ahamed, C. Demartini, T. Conte, L. Liu, W. Claycomb, M. Nakamura, E. Tovar, S. Cimato, C.-H. Lung, H. Takakura, J.-J. Yang, T. Akiyama, Z. Zhang, & K. Hasan (版本), Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017 (页码 39-44). 期刊论文 8029588 (Proceedings - International Computer Software and Applications Conference; 卷 1). IEEE Computer Society. https://doi.org/10.1109/COMPSAC.2017.170

Liu, Ailun ; Zhu, Huibiao ; Fei, Yuan 等. / Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra. Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017. 编辑 / Sorel Reisman ; Sheikh Iqbal Ahamed ; Claudio Demartini ; Thomas Conte ; Ling Liu ; William Claycomb ; Motonori Nakamura ; Edmundo Tovar ; Stelvio Cimato ; Chung-Horng Lung ; Hiroki Takakura ; Ji-Jiang Yang ; Toyokazu Akiyama ; Zhiyong Zhang ; Kamrul Hasan. IEEE Computer Society, 2017. 页码 39-44 (Proceedings - International Computer Software and Applications Conference).

@inproceedings{ea65294a9cbf45bcadc379245894cde6,

title = "Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra",

abstract = "The security protocol is proposed as a security solution for end-to-end communication between smart grid applications in the EU FP7 project C-DAX. Since the importance and widespread use of the security protocol, it is of great significance to formally analyze and verify relevant security properties of this security protocol. In this paper, we apply Communicating Sequential Processes (CSP) to model the security protocol. Further, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for the specification and relevant secure properties, e.g. reachability of the fake goal. Our modeling and verification show that a risk may exist in the security protocol.",

keywords = "C-DAX, Formalization, The Security Protocol, Verification",

author = "Ailun Liu and Huibiao Zhu and Yuan Fei and Shuangqing Xiang and Gang Lu and Wanling Xie",

note = "Publisher Copyright: {\textcopyright} 2017 IEEE.; 41st Annual IEEE Computer Software and Applications Conference, COMPSAC 2017 ; Conference date: 04-07-2017 Through 08-07-2017",

year = "2017",

month = sep,

day = "7",

doi = "10.1109/COMPSAC.2017.170",

language = "英语",

series = "Proceedings - International Computer Software and Applications Conference",

publisher = "IEEE Computer Society",

pages = "39--44",

editor = "Sorel Reisman and Ahamed, \{Sheikh Iqbal\} and Claudio Demartini and Thomas Conte and Ling Liu and William Claycomb and Motonori Nakamura and Edmundo Tovar and Stelvio Cimato and Chung-Horng Lung and Hiroki Takakura and Ji-Jiang Yang and Toyokazu Akiyama and Zhiyong Zhang and Kamrul Hasan",

booktitle = "Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017",

address = "美国",

}

Liu, A, Zhu, H, Fei, Y, Xiang, S, Lu, G & Xie, W 2017, Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra. 在 S Reisman, SI Ahamed, C Demartini, T Conte, L Liu, W Claycomb, M Nakamura, E Tovar, S Cimato, C-H Lung, H Takakura, J-J Yang, T Akiyama, Z Zhang & K Hasan (版本), Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017., 8029588, Proceedings - International Computer Software and Applications Conference, 卷 1, IEEE Computer Society, 页码 39-44, 41st Annual IEEE Computer Software and Applications Conference, COMPSAC 2017, Torino, 意大利, 4/07/17. https://doi.org/10.1109/COMPSAC.2017.170

Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra. / Liu, Ailun; Zhu, Huibiao; Fei, Yuan 等.
Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017. 编辑 / Sorel Reisman; Sheikh Iqbal Ahamed; Claudio Demartini; Thomas Conte; Ling Liu; William Claycomb; Motonori Nakamura; Edmundo Tovar; Stelvio Cimato; Chung-Horng Lung; Hiroki Takakura; Ji-Jiang Yang; Toyokazu Akiyama; Zhiyong Zhang; Kamrul Hasan. IEEE Computer Society, 2017. 页码 39-44 8029588 (Proceedings - International Computer Software and Applications Conference; 卷 1).

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

TY - GEN

T1 - Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra

AU - Liu, Ailun

AU - Zhu, Huibiao

AU - Fei, Yuan

AU - Xiang, Shuangqing

AU - Lu, Gang

AU - Xie, Wanling

PY - 2017/9/7

Y1 - 2017/9/7

N2 - The security protocol is proposed as a security solution for end-to-end communication between smart grid applications in the EU FP7 project C-DAX. Since the importance and widespread use of the security protocol, it is of great significance to formally analyze and verify relevant security properties of this security protocol. In this paper, we apply Communicating Sequential Processes (CSP) to model the security protocol. Further, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for the specification and relevant secure properties, e.g. reachability of the fake goal. Our modeling and verification show that a risk may exist in the security protocol.

AB - The security protocol is proposed as a security solution for end-to-end communication between smart grid applications in the EU FP7 project C-DAX. Since the importance and widespread use of the security protocol, it is of great significance to formally analyze and verify relevant security properties of this security protocol. In this paper, we apply Communicating Sequential Processes (CSP) to model the security protocol. Further, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for the specification and relevant secure properties, e.g. reachability of the fake goal. Our modeling and verification show that a risk may exist in the security protocol.

KW - C-DAX

KW - Formalization

KW - The Security Protocol

KW - Verification

UR - https://www.scopus.com/pages/publications/85031942966

U2 - 10.1109/COMPSAC.2017.170

DO - 10.1109/COMPSAC.2017.170

M3 - 会议稿件

AN - SCOPUS:85031942966

T3 - Proceedings - International Computer Software and Applications Conference

SP - 39

EP - 44

BT - Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017

A2 - Reisman, Sorel

A2 - Ahamed, Sheikh Iqbal

A2 - Demartini, Claudio

A2 - Conte, Thomas

A2 - Liu, Ling

A2 - Claycomb, William

A2 - Nakamura, Motonori

A2 - Tovar, Edmundo

A2 - Cimato, Stelvio

A2 - Lung, Chung-Horng

A2 - Takakura, Hiroki

A2 - Yang, Ji-Jiang

A2 - Akiyama, Toyokazu

A2 - Zhang, Zhiyong

A2 - Hasan, Kamrul

PB - IEEE Computer Society

T2 - 41st Annual IEEE Computer Software and Applications Conference, COMPSAC 2017

Y2 - 4 July 2017 through 8 July 2017

ER -

Liu A, Zhu H, Fei Y, Xiang S, Lu G, Xie W. Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra. 在 Reisman S, Ahamed SI, Demartini C, Conte T, Liu L, Claycomb W, Nakamura M, Tovar E, Cimato S, Lung CH, Takakura H, Yang JJ, Akiyama T, Zhang Z, Hasan K, 编辑, Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017. IEEE Computer Society. 2017. 页码 39-44. 8029588. (Proceedings - International Computer Software and Applications Conference). doi: 10.1109/COMPSAC.2017.170

Modeling and Analysis of the Security Protocol in C-DAX Based on Process Algebra

摘要

丛书

会议

联合国可持续发展目标

访问文件

其它文件与链接

学术指纹

引用此