Modeling and Verifying AUPS Using CSP

  • Hongqin Zhang
  • , Huibiao Zhu
  • , Jiaqi Yin
  • , Ningning Chen

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-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 languageEnglish
Title of host publicationSEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering
PublisherKnowledge Systems Institute Graduate School
Pages568-573
Number of pages6
ISBN (Electronic)1891706543, 9781891706547
DOIs
StatePublished - 2022
Externally publishedYes
Event34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022 - Pittsburgh, United States
Duration: 1 Jul 202210 Jul 2022

Publication series

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

Conference

Conference34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022
Country/TerritoryUnited States
CityPittsburgh
Period1/07/2210/07/22

Keywords

  • AUPS
  • CSP
  • Modeling
  • PAT
  • Verifying

Fingerprint

Dive into the research topics of 'Modeling and Verifying AUPS Using CSP'. Together they form a unique fingerprint.

Cite this