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

^*Corresponding author for this work

Software Engineering Institute

East China Normal University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017
Editors	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
Publisher	IEEE Computer Society
Pages	39-44
Number of pages	6
ISBN (Electronic)	9781538603673
DOIs	https://doi.org/10.1109/COMPSAC.2017.170
State	Published - 7 Sep 2017
Event	41st Annual IEEE Computer Software and Applications Conference, COMPSAC 2017 - Torino, Italy Duration: 4 Jul 2017 → 8 Jul 2017

Publication series

Name	Proceedings - International Computer Software and Applications Conference
Volume	1
ISSN (Print)	0730-3157

Conference

Conference	41st Annual IEEE Computer Software and Applications Conference, COMPSAC 2017
Country/Territory	Italy
City	Torino
Period	4/07/17 → 8/07/17

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 7 Affordable and Clean Energy

Keywords

C-DAX
Formalization
The Security Protocol
Verification

Access to Document

10.1109/COMPSAC.2017.170

Cite this

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. In 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 (Eds.), Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017 (pp. 39-44). Article 8029588 (Proceedings - International Computer Software and Applications Conference; Vol. 1). IEEE Computer Society. https://doi.org/10.1109/COMPSAC.2017.170

Liu, Ailun ; Zhu, Huibiao ; Fei, Yuan et al. / 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. editor / 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. pp. 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. in 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 (eds), Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017., 8029588, Proceedings - International Computer Software and Applications Conference, vol. 1, IEEE Computer Society, pp. 39-44, 41st Annual IEEE Computer Software and Applications Conference, COMPSAC 2017, Torino, Italy, 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 et al.
Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017. ed. / 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. p. 39-44 8029588 (Proceedings - International Computer Software and Applications Conference; Vol. 1).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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. In 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, editors, Proceedings - 2017 IEEE 41st Annual Computer Software and Applications Conference, COMPSAC 2017. IEEE Computer Society. 2017. p. 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

Abstract

Publication series

Conference

UN SDGs

Keywords

Access to Document

Other files and links

Fingerprint

Cite this