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

School of Software

East China Normal University

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

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.

Original language	English
Title of host publication	Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings
Editors	Hiroyuki Takizawa, Hong Shen, Toshihiro Hanawa, Jong Hyuk Park, Hui Tian, Ryusuke Egawa
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	158-171
Number of pages	14
ISBN (Print)	9783031299261
DOIs	https://doi.org/10.1007/978-3-031-29927-8_13
State	Published - 2023
Event	23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022 - Sendai, Japan Duration: 7 Dec 2022 → 9 Dec 2022

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13798 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022
Country/Territory	Japan
City	Sendai
Period	7/12/22 → 9/12/22

Keywords

CSP
Modeling
Session Initiation Protocol (SIP)
Software Defined Networking (SDN)
Verification

Access to Document

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

Cite this

Hou, Z., Yin, J., Zhu, H., & Chen, N. (2023). Formalization and Verification of SIP Using CSP. In H. Takizawa, H. Shen, T. Hanawa, J. Hyuk Park, H. Tian, & R. Egawa (Eds.), Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings (pp. 158-171). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 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 et al. / Formalization and Verification of SIP Using CSP. Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. editor / Hiroyuki Takizawa ; Hong Shen ; Toshihiro Hanawa ; Jong Hyuk Park ; Hui Tian ; Ryusuke Egawa. Springer Science and Business Media Deutschland GmbH, 2023. pp. 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. in H Takizawa, H Shen, T Hanawa, J Hyuk Park, H Tian & R Egawa (eds), 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), vol. 13798 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 158-171, 23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022, Sendai, Japan, 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 et al.
Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. ed. / Hiroyuki Takizawa; Hong Shen; Toshihiro Hanawa; Jong Hyuk Park; Hui Tian; Ryusuke Egawa. Springer Science and Business Media Deutschland GmbH, 2023. p. 158-171 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13798 LNCS).

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

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. In Takizawa H, Shen H, Hanawa T, Hyuk Park J, Tian H, Egawa R, editors, Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. Springer Science and Business Media Deutschland GmbH. 2023. p. 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