{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,7]],"date-time":"2026-06-07T04:48:49Z","timestamp":1780807729562,"version":"3.54.1"},"reference-count":29,"publisher":"World Scientific Pub Co Pte Ltd","issue":"11","funder":[{"DOI":"10.13039\/501100001809","name":"the National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62032024"],"award-info":[{"award-number":["62032024"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"the Digital Silk Road Shanghai International Joint Lab of Trustworthy Intelligent Software","award":["22510750100"],"award-info":[{"award-number":["22510750100"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2025,11]]},"abstract":"<jats:p>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\u2019s advantages, it is gaining increasing attention from industries. Hence, ensuring the reliability of Graphene becomes paramount.<\/jats:p>\n                  <jats:p>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.<\/jats:p>","DOI":"10.1142\/s0218194025410037","type":"journal-article","created":{"date-parts":[[2025,4,11]],"date-time":"2025-04-11T09:55:26Z","timestamp":1744365326000},"page":"1573-1599","source":"Crossref","is-referenced-by-count":1,"title":["Validating Secure Cloud Communication Mechanisms of Graphene with CSP-Based Modeling"],"prefix":"10.1142","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-6659-6906","authenticated-orcid":false,"given":"Jianhao","family":"Liu","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, P.\u00a0R.\u00a0China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3266-0084","authenticated-orcid":false,"given":"Zhiru","family":"Hou","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, P.\u00a0R.\u00a0China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0214-8565","authenticated-orcid":false,"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, P.\u00a0R.\u00a0China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"219","published-online":{"date-parts":[[2025,5,24]]},"reference":[{"key":"S0218194025410037BIB002","volume-title":"TCP\/IP Protocol Suite","author":"Forouzan B. A.","year":"2002"},{"issue":"7","key":"S0218194025410037BIB003","first-page":"20","volume":"46","author":"Kumar S.","year":"2012","journal-title":"Int. J. Comput. Appl."},{"key":"S0218194025410037BIB005","volume-title":"SSL and TLS: Theory and Practice","author":"Oppliger R.","year":"2023"},{"key":"S0218194025410037BIB006","volume-title":"NDSS","author":"Modadugu N.","year":"2004"},{"key":"S0218194025410037BIB007","first-page":"435","volume-title":"IEEE Symp. Security and Privacy","author":"Ronen E.","year":"2019"},{"key":"S0218194025410037BIB008","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813653"},{"key":"S0218194025410037BIB009","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2016.2548426"},{"key":"S0218194025410037BIB010","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-020-00511-w"},{"key":"S0218194025410037BIB011","volume-title":"Amazon Web Services: Overview of Security Processes","author":"Amazon","year":"2015"},{"key":"S0218194025410037BIB013","first-page":"160","volume-title":"2nd Int. Symp. Agent, Multi-agent Systems and Robotics","author":"Liang C.","year":"2016"},{"key":"S0218194025410037BIB014","doi-asserted-by":"publisher","DOI":"10.6028\/jres.106.023"},{"key":"S0218194025410037BIB015","doi-asserted-by":"publisher","DOI":"10.1109\/SPC.2014.7086230"},{"key":"S0218194025410037BIB016","doi-asserted-by":"publisher","DOI":"10.1109\/SMART50582.2020.9336800"},{"key":"S0218194025410037BIB017","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985"},{"key":"S0218194025410037BIB018","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"S0218194025410037BIB019","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-013-3091-5"},{"key":"S0218194025410037BIB020","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88479-8_22"},{"key":"S0218194025410037BIB021","doi-asserted-by":"publisher","DOI":"10.1109\/CCOMS.2019.8821735"},{"key":"S0218194025410037BIB022","doi-asserted-by":"publisher","DOI":"10.1109\/SmartTechCon.2017.8358562"},{"key":"S0218194025410037BIB023","volume-title":"Process Algebra: Equational Theories of Communicating Processes","author":"Baeten J. C.","year":"2010"},{"key":"S0218194025410037BIB024","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80025-X"},{"key":"S0218194025410037BIB025","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"S0218194025410037BIB026","doi-asserted-by":"publisher","DOI":"10.1109\/32.637148"},{"key":"S0218194025410037BIB027","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-19052-1_11"},{"key":"S0218194025410037BIB028","doi-asserted-by":"publisher","DOI":"10.1145\/3599731"},{"key":"S0218194025410037BIB029","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE62328.2024.00057"},{"key":"S0218194025410037BIB030","doi-asserted-by":"publisher","DOI":"10.1007\/s11036-023-02181-z"},{"key":"S0218194025410037BIB031","doi-asserted-by":"publisher","DOI":"10.18293\/SEKE2019-122"},{"key":"S0218194025410037BIB032","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194023500535"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194025410037","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T03:22:51Z","timestamp":1762831371000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S0218194025410037"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,24]]},"references-count":29,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2025,11]]}},"alternative-id":["10.1142\/S0218194025410037"],"URL":"https:\/\/doi.org\/10.1142\/s0218194025410037","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,24]]}}}