Formalization and Verification of SIP Using CSP

Zhiru Hou; Jiaqi Yin; Huibiao Zhu; Ningning Chen

doi:10.1007/978-3-031-29927-8_13

Formalization and Verification of SIP Using CSP

Zhiru Hou, Jiaqi Yin, Huibiao Zhu, Ningning Chen

软件学院

East China Normal University

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

摘要

As one of the most popular multimedia communication protocol, Session Initiation Protocol (SIP) has lots of interesting features, such as extensible and open communication. However, with its rapid development, load balance problem and security risks are exposed. Finding the suitable method to solve the two problems has become an important issue. In this paper, we first apply Communicating Sequential Processes (CSP) to model SIP, then adopt the model checking tool Process Analysis Tookit (PAT) to verify the internal properties and the safety properties of our model. The verification results show that the SIP model has load balance problem and it cannot assure the security of data with malicious users. So we enhance it by adding Software Defined Networking (SDN) architecture and identity authentication mechanism in the process. In the light of new verification results, it can be found that the improved model can satisfy the internal properties and we succeed in improving the security of the SIP model.

源语言	英语
主期刊名	Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings
编辑	Hiroyuki Takizawa, Hong Shen, Toshihiro Hanawa, Jong Hyuk Park, Hui Tian, Ryusuke Egawa
出版商	Springer Science and Business Media Deutschland GmbH
页	158-171
页数	14
ISBN（印刷版）	9783031299261
DOI	https://doi.org/10.1007/978-3-031-29927-8_13
出版状态	已出版 - 2023
活动	23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022 - Sendai, 日本期限: 7 12月 2022 → 9 12月 2022

出版系列

姓名	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
卷	13798 LNCS
ISSN（印刷版）	0302-9743
ISSN（电子版）	1611-3349

会议

会议	23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022
国家/地区	日本
市	Sendai
时期	7/12/22 → 9/12/22

访问文件

10.1007/978-3-031-29927-8_13

其它文件与链接

链接到 Scopus 的出版物

引用此

Hou, Z., Yin, J., Zhu, H., & Chen, N. (2023). Formalization and Verification of SIP Using CSP. 在 H. Takizawa, H. Shen, T. Hanawa, J. Hyuk Park, H. Tian, & R. Egawa (编辑), Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings (页码 158-171). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 卷 13798 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-29927-8_13

Hou, Zhiru ; Yin, Jiaqi ; Zhu, Huibiao 等. / Formalization and Verification of SIP Using CSP. Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. 编辑 / Hiroyuki Takizawa ; Hong Shen ; Toshihiro Hanawa ; Jong Hyuk Park ; Hui Tian ; Ryusuke Egawa. Springer Science and Business Media Deutschland GmbH, 2023. 页码 158-171 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{8a35164aee724da296c20d0e484b44ab,

title = "Formalization and Verification of SIP Using CSP",

abstract = "As one of the most popular multimedia communication protocol, Session Initiation Protocol (SIP) has lots of interesting features, such as extensible and open communication. However, with its rapid development, load balance problem and security risks are exposed. Finding the suitable method to solve the two problems has become an important issue. In this paper, we first apply Communicating Sequential Processes (CSP) to model SIP, then adopt the model checking tool Process Analysis Tookit (PAT) to verify the internal properties and the safety properties of our model. The verification results show that the SIP model has load balance problem and it cannot assure the security of data with malicious users. So we enhance it by adding Software Defined Networking (SDN) architecture and identity authentication mechanism in the process. In the light of new verification results, it can be found that the improved model can satisfy the internal properties and we succeed in improving the security of the SIP model.",

keywords = "CSP, Modeling, Session Initiation Protocol (SIP), Software Defined Networking (SDN), Verification",

author = "Zhiru Hou and Jiaqi Yin and Huibiao Zhu and Ningning Chen",

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022 ; Conference date: 07-12-2022 Through 09-12-2022",

year = "2023",

doi = "10.1007/978-3-031-29927-8_13",

language = "英语",

isbn = "9783031299261",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "158--171",

editor = "Hiroyuki Takizawa and Hong Shen and Toshihiro Hanawa and {Hyuk Park}, Jong and Hui Tian and Ryusuke Egawa",

booktitle = "Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings",

}

Hou, Z, Yin, J, Zhu, H & Chen, N 2023, Formalization and Verification of SIP Using CSP. 在 H Takizawa, H Shen, T Hanawa, J Hyuk Park, H Tian & R Egawa (编辑), Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 卷 13798 LNCS, Springer Science and Business Media Deutschland GmbH, 页码 158-171, 23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022, Sendai, 日本, 7/12/22. https://doi.org/10.1007/978-3-031-29927-8_13

Formalization and Verification of SIP Using CSP. / Hou, Zhiru; Yin, Jiaqi; Zhu, Huibiao 等.
Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. 编辑 / Hiroyuki Takizawa; Hong Shen; Toshihiro Hanawa; Jong Hyuk Park; Hui Tian; Ryusuke Egawa. Springer Science and Business Media Deutschland GmbH, 2023. 页码 158-171 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 卷 13798 LNCS).

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

TY - GEN

T1 - Formalization and Verification of SIP Using CSP

AU - Hou, Zhiru

AU - Yin, Jiaqi

AU - Zhu, Huibiao

AU - Chen, Ningning

PY - 2023

Y1 - 2023

N2 - As one of the most popular multimedia communication protocol, Session Initiation Protocol (SIP) has lots of interesting features, such as extensible and open communication. However, with its rapid development, load balance problem and security risks are exposed. Finding the suitable method to solve the two problems has become an important issue. In this paper, we first apply Communicating Sequential Processes (CSP) to model SIP, then adopt the model checking tool Process Analysis Tookit (PAT) to verify the internal properties and the safety properties of our model. The verification results show that the SIP model has load balance problem and it cannot assure the security of data with malicious users. So we enhance it by adding Software Defined Networking (SDN) architecture and identity authentication mechanism in the process. In the light of new verification results, it can be found that the improved model can satisfy the internal properties and we succeed in improving the security of the SIP model.

AB - As one of the most popular multimedia communication protocol, Session Initiation Protocol (SIP) has lots of interesting features, such as extensible and open communication. However, with its rapid development, load balance problem and security risks are exposed. Finding the suitable method to solve the two problems has become an important issue. In this paper, we first apply Communicating Sequential Processes (CSP) to model SIP, then adopt the model checking tool Process Analysis Tookit (PAT) to verify the internal properties and the safety properties of our model. The verification results show that the SIP model has load balance problem and it cannot assure the security of data with malicious users. So we enhance it by adding Software Defined Networking (SDN) architecture and identity authentication mechanism in the process. In the light of new verification results, it can be found that the improved model can satisfy the internal properties and we succeed in improving the security of the SIP model.

KW - CSP

KW - Modeling

KW - Session Initiation Protocol (SIP)

KW - Software Defined Networking (SDN)

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=85159487326&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-29927-8_13

DO - 10.1007/978-3-031-29927-8_13

M3 - 会议稿件

AN - SCOPUS:85159487326

SN - 9783031299261

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 158

EP - 171

BT - Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings

A2 - Takizawa, Hiroyuki

A2 - Shen, Hong

A2 - Hanawa, Toshihiro

A2 - Hyuk Park, Jong

A2 - Tian, Hui

A2 - Egawa, Ryusuke

PB - Springer Science and Business Media Deutschland GmbH

T2 - 23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022

Y2 - 7 December 2022 through 9 December 2022

ER -

Hou Z, Yin J, Zhu H, Chen N. Formalization and Verification of SIP Using CSP. 在 Takizawa H, Shen H, Hanawa T, Hyuk Park J, Tian H, Egawa R, 编辑, Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. Springer Science and Business Media Deutschland GmbH. 2023. 页码 158-171. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-29927-8_13

Formalization and Verification of SIP Using CSP

摘要

出版系列

会议

访问文件

其它文件与链接

指纹

引用此