Formalization and Verification of TESAC Using CSP

Dongzhen Sun, Huibiao Zhu, Yuan Fei, Lili Xiao, Gang Lu, Jiaqi Yin

Research output: Contribution to journalArticlepeer-review

1 Scopus citations

Abstract

Cloud computing is an emerging computing paradigm in IT industries. The wide adoption of cloud computing is raising concerns about management of data in the cloud. Access control and data security are two critical issues of cloud computing. Time-efficient secure access control (TESAC) model is a new data access control scheme which can minimize many significant problems. This scheme has better performance than other existing models in a cloud computing environment. TESAC is attracting more and more attentions from industries. Hence, the reliability of TESAC becomes extremely important. In this paper, we apply Communication Sequential Processes (CSP) to model TESAC, as well as their security properties. We mainly focus on its data access mechanism part and formalize it in detail. Moreover, using the model checker Process Analysis Toolkit (PAT), we have verified that the TESAC model cannot assure the security of data with malicious users. For the purpose of solving this problem, we introduce a new method similar to digital signature. Our study can improve the security and robustness of the TESAC model.

Original languageEnglish
Pages (from-to)1741-1760
Number of pages20
JournalInternational Journal of Software Engineering and Knowledge Engineering
Volume29
Issue number11-12
DOIs
StatePublished - 1 Nov 2019
Externally publishedYes

Keywords

  • access control
  • cloud computing
  • CSP
  • modeling
  • TESAC
  • verification

Fingerprint

Dive into the research topics of 'Formalization and Verification of TESAC Using CSP'. Together they form a unique fingerprint.

Cite this