Modeling and Verifying AUPS Using CSP

Hongqin Zhang; Huibiao Zhu; Jiaqi Yin; Ningning Chen

doi:10.18293/SEKE2022-088

Modeling and Verifying AUPS Using CSP

Hongqin Zhang
, Huibiao Zhu^*
, Jiaqi Yin
, Ningning Chen

^*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 Internet of Things (IoT) is an important technology in IT industries. The wide adoption of IoT raises concerns about security and privacy. The Authenticated Publish/Subscribe (AUPS) model is an IoT system which aims to address the security and privacy issues in the IoT environment. AUPS is attracting more and more attention from industries. Hence, the reliability of AUPS is worth investigating. In this paper, we model AUPS using Communicating Sequential Processes (CSP). Five properties (Deadlock Freedom, Data Availability, Data Leakage, Device Faking and User Privacy Leakage) of the model are verified by utilizing the model checker Process Analysis Toolkit (PAT). The verification results demonstrate that AUPS cannot ensure the security of critical data. To solve the problem, we improve the model by using a digital certificate. The verification results of the improved model indicate that our study can enhance the security and reliability of the AUPS model.

Original language	English
Title of host publication	SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering
Publisher	Knowledge Systems Institute Graduate School
Pages	568-573
Number of pages	6
ISBN (Electronic)	1891706543, 9781891706547
DOIs	https://doi.org/10.18293/SEKE2022-088
State	Published - 2022
Event	34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022 - Pittsburgh, United States Duration: 1 Jul 2022 → 10 Jul 2022

Publication series

Name	Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
ISSN (Print)	2325-9000
ISSN (Electronic)	2325-9086

Conference

Conference	34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022
Country/Territory	United States
City	Pittsburgh
Period	1/07/22 → 10/07/22

Keywords

AUPS
CSP
Modeling
PAT
Verifying

Access to Document

10.18293/SEKE2022-088

Cite this

Zhang, H., Zhu, H., Yin, J., & Chen, N. (2022). Modeling and Verifying AUPS Using CSP. In SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering (pp. 568-573). (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE). Knowledge Systems Institute Graduate School. https://doi.org/10.18293/SEKE2022-088

@inproceedings{7e17b180d4b547ba996b3c5beacde4a7,

title = "Modeling and Verifying AUPS Using CSP",

abstract = "The Internet of Things (IoT) is an important technology in IT industries. The wide adoption of IoT raises concerns about security and privacy. The Authenticated Publish/Subscribe (AUPS) model is an IoT system which aims to address the security and privacy issues in the IoT environment. AUPS is attracting more and more attention from industries. Hence, the reliability of AUPS is worth investigating. In this paper, we model AUPS using Communicating Sequential Processes (CSP). Five properties (Deadlock Freedom, Data Availability, Data Leakage, Device Faking and User Privacy Leakage) of the model are verified by utilizing the model checker Process Analysis Toolkit (PAT). The verification results demonstrate that AUPS cannot ensure the security of critical data. To solve the problem, we improve the model by using a digital certificate. The verification results of the improved model indicate that our study can enhance the security and reliability of the AUPS model.",

keywords = "AUPS, CSP, Modeling, PAT, Verifying",

author = "Hongqin Zhang and Huibiao Zhu and Jiaqi Yin and Ningning Chen",

note = "Publisher Copyright: {\textcopyright} 2022 Knowledge Systems Institute Graduate School. All rights reserved.; 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022 ; Conference date: 01-07-2022 Through 10-07-2022",

year = "2022",

doi = "10.18293/SEKE2022-088",

language = "英语",

series = "Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE",

publisher = "Knowledge Systems Institute Graduate School",

pages = "568--573",

booktitle = "SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering",

address = "美国",

}

Zhang, H, Zhu, H, Yin, J & Chen, N 2022, Modeling and Verifying AUPS Using CSP. in SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering. Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE, Knowledge Systems Institute Graduate School, pp. 568-573, 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022, Pittsburgh, United States, 1/07/22. https://doi.org/10.18293/SEKE2022-088

Modeling and Verifying AUPS Using CSP. / Zhang, Hongqin; Zhu, Huibiao; Yin, Jiaqi et al.
SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering. Knowledge Systems Institute Graduate School, 2022. p. 568-573 (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE).

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

TY - GEN

T1 - Modeling and Verifying AUPS Using CSP

AU - Zhang, Hongqin

AU - Zhu, Huibiao

AU - Yin, Jiaqi

AU - Chen, Ningning

PY - 2022

Y1 - 2022

N2 - The Internet of Things (IoT) is an important technology in IT industries. The wide adoption of IoT raises concerns about security and privacy. The Authenticated Publish/Subscribe (AUPS) model is an IoT system which aims to address the security and privacy issues in the IoT environment. AUPS is attracting more and more attention from industries. Hence, the reliability of AUPS is worth investigating. In this paper, we model AUPS using Communicating Sequential Processes (CSP). Five properties (Deadlock Freedom, Data Availability, Data Leakage, Device Faking and User Privacy Leakage) of the model are verified by utilizing the model checker Process Analysis Toolkit (PAT). The verification results demonstrate that AUPS cannot ensure the security of critical data. To solve the problem, we improve the model by using a digital certificate. The verification results of the improved model indicate that our study can enhance the security and reliability of the AUPS model.

AB - The Internet of Things (IoT) is an important technology in IT industries. The wide adoption of IoT raises concerns about security and privacy. The Authenticated Publish/Subscribe (AUPS) model is an IoT system which aims to address the security and privacy issues in the IoT environment. AUPS is attracting more and more attention from industries. Hence, the reliability of AUPS is worth investigating. In this paper, we model AUPS using Communicating Sequential Processes (CSP). Five properties (Deadlock Freedom, Data Availability, Data Leakage, Device Faking and User Privacy Leakage) of the model are verified by utilizing the model checker Process Analysis Toolkit (PAT). The verification results demonstrate that AUPS cannot ensure the security of critical data. To solve the problem, we improve the model by using a digital certificate. The verification results of the improved model indicate that our study can enhance the security and reliability of the AUPS model.

KW - AUPS

KW - CSP

KW - Modeling

KW - PAT

KW - Verifying

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

U2 - 10.18293/SEKE2022-088

DO - 10.18293/SEKE2022-088

M3 - 会议稿件

AN - SCOPUS:85137153115

T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE

SP - 568

EP - 573

BT - SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering

PB - Knowledge Systems Institute Graduate School

T2 - 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022

Y2 - 1 July 2022 through 10 July 2022

ER -

Zhang H, Zhu H, Yin J, Chen N. Modeling and Verifying AUPS Using CSP. In SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering. Knowledge Systems Institute Graduate School. 2022. p. 568-573. (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE). doi: 10.18293/SEKE2022-088

Modeling and Verifying AUPS Using CSP

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this