{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:09:26Z","timestamp":1753884566034,"version":"3.41.2"},"reference-count":25,"publisher":"World Scientific Pub Co Pte Ltd","issue":"06","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J CIRCUIT SYST COMP"],"published-print":{"date-parts":[[2025,4]]},"abstract":"<jats:p> New Simple Queue (NSQ) is a distributed messaging platform developed in Golang that can handle billions of daily messages. Its distributed architecture ensures high fault tolerance and availability. Given NSQ\u2019s widespread application across various fields, it is crucial to focus on the system\u2019s robustness and data transmission security. Therefore, a rigorous mathematical logic analysis of NSQ\u2019s messaging mechanism is essential for verifying its reliability. This paper formalizes NSQ\u2019s core components using Communicating Sequential Processes (CSP), resulting in a comprehensive formal model of the system. Furthermore, this paper utilizes the Process Analysis Toolkit (PAT) for practical implementation of the model, verifying five critical properties of the NSQ system. And the verification results demonstrate that the NSQ system successfully satisfies these essential properties, highlighting its flexibility, robustness and efficient messaging service capabilities. Moreover, this paper focuses on formalizing and verifying the security mechanisms in NSQ\u2019s data transmission. By integrating the Transport Layer Security (TLS) protocol into the NSQ system and employing a man-in-the-middle model to simulate deception and interception attacks, it is demonstrated that the TLS protocol enhances the security of NSQ data transmission. This paper also proposes upgrading from one-way to two-way certificate authentication to further enhance TLS data security. Experimental results reveal that despite significant security improvements with the TLS protocol, producer and consumer processes remain vulnerable to spoofing attacks under specific insecure network conditions, leading to potential data leaks. Therefore, the TLS protocol can significantly improve the data security of the NSQ system. <\/jats:p>","DOI":"10.1142\/s0218126625501452","type":"journal-article","created":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T14:44:48Z","timestamp":1731681888000},"source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification and Security Analysis of Go-based New Simple Queue System"],"prefix":"10.1142","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3266-0084","authenticated-orcid":false,"given":"Zhiru","family":"Hou","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Danyang","family":"Wang","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiaqi","family":"Yin","sequence":"additional","affiliation":[{"name":"Northwestern Polytechnical University, Xi\u2019an, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sini","family":"Chen","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2025,1,27]]},"reference":[{"key":"S0218126625501452BIB001","doi-asserted-by":"publisher","DOI":"10.1145\/230798.230809"},{"key":"S0218126625501452BIB003","doi-asserted-by":"publisher","DOI":"10.1109\/ICIST.2014.6920368"},{"key":"S0218126625501452BIB004","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"volume-title":"Communicating Sequential Processes","year":"1985","author":"Hoare C. A. R.","key":"S0218126625501452BIB005"},{"key":"S0218126625501452BIB007","doi-asserted-by":"publisher","DOI":"10.1088\/1742-6596\/1544\/1\/012122"},{"key":"S0218126625501452BIB008","first-page":"74","volume-title":"QuASoQ 2023: 11th Int. Workshop on Quantitative Approaches to Software Quality","author":"Wang D.","year":"2023"},{"key":"S0218126625501452BIB010","doi-asserted-by":"publisher","DOI":"10.1109\/USBEREIT51232.2021.9455072"},{"key":"S0218126625501452BIB011","doi-asserted-by":"publisher","DOI":"10.13052\/jcsm2245-1439.414"},{"key":"S0218126625501452BIB012","first-page":"1","volume-title":"2017 3rd Int. Conf. Advances in Computing, Communication and Automation (ICACCA)","author":"Bhushan B.","year":"2017"},{"key":"S0218126625501452BIB014","doi-asserted-by":"publisher","DOI":"10.1109\/18.54902"},{"key":"S0218126625501452BIB015","doi-asserted-by":"publisher","DOI":"10.1007\/s11036-022-01989-5"},{"key":"S0218126625501452BIB016","doi-asserted-by":"publisher","DOI":"10.2298\/CSIS210707057X"},{"key":"S0218126625501452BIB017","volume-title":"ActiveMQ in Action","volume":"47","author":"Snyder B.","year":"2011"},{"key":"S0218126625501452BIB018","doi-asserted-by":"publisher","DOI":"10.15439\/2014F48"},{"key":"S0218126625501452BIB019","doi-asserted-by":"publisher","DOI":"10.14778\/2824032.2824063"},{"key":"S0218126625501452BIB020","doi-asserted-by":"publisher","DOI":"10.1109\/ICICTA.2017.72"},{"key":"S0218126625501452BIB023","doi-asserted-by":"publisher","DOI":"10.1109\/CLOUD53861.2021.00050"},{"key":"S0218126625501452BIB024","doi-asserted-by":"publisher","DOI":"10.1109\/ICCST49569.2021.9717379"},{"key":"S0218126625501452BIB025","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126619500610"},{"key":"S0218126625501452BIB026","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126619501779"},{"key":"S0218126625501452BIB027","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126605002714"},{"key":"S0218126625501452BIB028","doi-asserted-by":"publisher","DOI":"10.1109\/32.637148"},{"key":"S0218126625501452BIB029","doi-asserted-by":"publisher","DOI":"10.1002\/smr.2371"},{"key":"S0218126625501452BIB030","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126613400380"},{"key":"S0218126625501452BIB031","doi-asserted-by":"publisher","DOI":"10.1007\/s11036-022-01986-8"}],"container-title":["Journal of Circuits, Systems and Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218126625501452","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,15]],"date-time":"2025-04-15T04:11:13Z","timestamp":1744690273000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S0218126625501452"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,27]]},"references-count":25,"journal-issue":{"issue":"06","published-print":{"date-parts":[[2025,4]]}},"alternative-id":["10.1142\/S0218126625501452"],"URL":"https:\/\/doi.org\/10.1142\/s0218126625501452","relation":{},"ISSN":["0218-1266","1793-6454"],"issn-type":[{"type":"print","value":"0218-1266"},{"type":"electronic","value":"1793-6454"}],"subject":[],"published":{"date-parts":[[2025,1,27]]},"article-number":"2550145"}}