Formalization And Verification Of TESAC Using CSP

Cloud computing(Cloud Computing)is an emerging computing paradigm in the IT industry.It aims to achieve "network as a high-performance computer" and connects the network to manage and schedule huge computing resources in a unified manner.Many problems have been exposed in the widespread application of cloud computing,which has caused people to worry about data security management in the cloud.It prompts re-searchers in cloud computing to propose corresponding solutions.Access control and data security are two essential issues in cloud computing.In order to ensure the security of data access and transmission,a variety of cloud computing access control models have been proposed.Time Efficient Secure Access Control(TESAC)model is a new cloud com-puting access control scheme based on profile of users.It has better characteristics than other existing models in cloud computing,which makes TESAC attract more and more attentions from industries.Therefore,it is significant to study the reliability of TESAC.The TESAC model contains three entities,including user,data owner,and cloud server.Users need to obtain data from the cloud server according to the algorithm pro-cess.In order to ensure the security of messages,TESAC uses asymmetric encryption to encrypt the message packet.This thesis applies Communicating Sequential Process(CSP)to TESAC.We focus on its access control system,and do the formal modeling and verifi-cation of the access control process.The user,data owner,and cloud server are abstracted into three process entities.We define the messages passed between the processes and the channels used to transmit the messages,which completes the CSP modeling of the entire system.At the same time,this thesis uses the model checker PAT to implement and verify the established model.We verify the deadlock-free,security and sequentiality of the TESAC model.For security,three types of intrusion are introduced.By analyzing the verification results,we find out that TESAC does not satisfy the security and sequentiality when the intruder exists.We give a typical case of an intruder's successful invasion,and provide a detailed description of the case.In order to enhance the reliability of TESAC,we use the digital signature method to improve and optimize the system.The verification results of the improved model show that our scheme can improve the safety of TESAC effectively.