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 utilize process algebra CSP to model the TCP-based communication processes within the Graphene architecture. Subsequently, we model the UDP-based communication processes as well. Then, we employ the model checker PAT to run the CSP models for both protocols and subsequently verify six properties: Deadlock Freedom, Divergence Freedom, Data Reachability, Cloud User Faking, Cloud Instance Faking, and Central Key Server Faking. According to the verification results, our models for both TCP and UDP satisfy all of the aforementioned properties. Therefore, we can conclude that the communication execution processes for both TCP and UDP in the Graphene architecture fulfill the anticipated security standards, thus indicating the reliability of the system.