云计算(Cloud Computing)是IT行业中新兴的计算范例,它以实现将“网络作为高性能计算机”为目的,以网络相连接的方式,对庞大的计算资源进行统一管理和调度。诸多问题在云计算的广泛应用中被暴露,引发了人们对云中数据安全管理的担忧,从而促使云计算领域的研究人员提出相应的解决方案。访问控制和数据安全是云计算中的两个关键问题,为了保证数据存取和传输的安全性,多种云计算访问控制模型被提出。高时效安全访问控制(Time Efficient Secure Access Control,TESAC)模型是一种新的基于用户资料的云计算访问控制方案,它与云计算中其他现有的模型相比,具有更好的特性,这使得TESAC吸引了行业越来越多的关注。因此,对于TESAC可靠性的研究具有很重要的意义。TESAC模型包含用户、数据拥有者和云服务器三个实体,用户需要按照算法流程从云服务器获取数据。为了保证消息的安全性,TESAC采用非对称加密的方式对消息包进行加密处理。本文将通信顺序进程(Communicating Sequential Process,CSP)方法应用到TESAC中,主要关注其访问控制系统,并对访问控制过程进行详细的形式化建模与验证分析。本文将用户、数据拥有者和云服务器抽象为三个进程实体,并且定义进程之间传递的消息和用来传输消息的通道,完成了对整个系统的CSP建模。同时,本文使用模型检测工具PAT来对建立的模型进行实现和验证。我们验证了 TESAC模型的无死锁性、安全性和顺序性,其中在安全性中引入了三种入侵类型。通过对验证结果进行分析,发现TESAC在入侵者存在的情形下,不满足安全性和顺序性。文中给出了入侵者成功入侵的典型案例,并对案例作出了详细的表述。为了提高TESAC的可靠性,我们利用数字签名的方法对系统做了改进和优化。改进后模型的验证结果表明,我们的改进方案可以有效提高TESAC的安全性。