Validating Secure Cloud Communication Mechanisms of Graphene with CSP-based Modeling

Cloud communication, as a core component of the cloud computing architecture, relies on the communication mechanism of TCP/UDP protocols. However, with the popularity of cloud communication, the security threats that it faces are also becoming increasingly severe. Graphene is a new cloud communication security architecture that targets both TCP and UDP communication. It provides security assurance during data transmission and authentication for cloud users and cloud service providers, effectively addressing some of the shortcomings of traditional security protocols. In light of Graphene’s advantages, it is gaining increasing attention from industries. Hence, ensuring the reliability of Graphene becomes paramount. In this paper, we first use process algebra CSP to model the TCP-based communication process of the Graphene architecture. Then, we use the model checker PAT to run the CSP model of Graphene and subsequently verify six properties, including Deadlock Freedom, Divergence Freedom, Data Reachability, Cloud User Faking, Cloud Instance Faking, and Central Key Server Faking. According to the verification results, our model satisfies all the above six properties. Therefore, we can conclude that the TCP communication execution process in the Graphene architecture fulfills the anticipated security standards, thus indicating that the system is reliable.