{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T15:28:27Z","timestamp":1783438107669,"version":"3.54.6"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2022,5,9]],"date-time":"2022-05-09T00:00:00Z","timestamp":1652054400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,5,9]],"date-time":"2022-05-09T00:00:00Z","timestamp":1652054400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mobile Netw Appl"],"published-print":{"date-parts":[[2022,10]]},"DOI":"10.1007\/s11036-022-01986-8","type":"journal-article","created":{"date-parts":[[2022,5,9]],"date-time":"2022-05-09T03:23:46Z","timestamp":1652066626000},"page":"2049-2067","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Verification of RabbitMQ with Kerberos Using Timed Automata"],"prefix":"10.1007","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3492-1591","authenticated-orcid":false,"given":"Ran","family":"Li","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jiaqi","family":"Yin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Phan Cong","family":"Vinh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,5,9]]},"reference":[{"key":"1986_CR1","first-page":"199","volume":"25","author":"M Kinoshita","year":"2017","unstructured":"Kinoshita M, Konoura H, Koike T, Leibnitz K, Murata M (2017) High throughput dequeuing technique in distributed message queues for IoT. J Inf Process 25:199\u2013208","journal-title":"J Inf Process"},{"key":"1986_CR2","unstructured":"Jiang Y, Liu Q, Qin C, Su J, Liu Q (2019) Message-oriented middleware: A review. In: BigCom. IEEE, pp 88\u201397"},{"key":"1986_CR3","doi-asserted-by":"crossref","unstructured":"Liu Y, Zhang L J, Xing C (2020) Review for message-oriented middleware. In: Internet of Things - ICIOT 2020. Springer International Publishing, Cham, pp 152\u2013159","DOI":"10.1007\/978-3-030-59615-6_12"},{"key":"1986_CR4","unstructured":"VMware (2022) RabbitMQ. https:\/\/www.rabbitmq.com\/. Accessed 6 March 2022"},{"key":"1986_CR5","unstructured":"Apache (2022a) Kafka. https:\/\/kafka.apache.org\/. Accessed 6 March 2022"},{"key":"1986_CR6","unstructured":"Apache (2022b) ActiveMQ. https:\/\/activemq.apache.org\/. Accessed 6 March 2022"},{"key":"1986_CR7","unstructured":"Apache (2022c) RocketMQ. https:\/\/rocketmq.apache.org\/. Accessed 6 March 2022"},{"key":"1986_CR8","unstructured":"OASIS (2022) AMQP. https:\/\/www.amqp.org\/. Accessed 6 March 2022"},{"key":"1986_CR9","doi-asserted-by":"crossref","unstructured":"Appel S, Sachs K, Buchmann AP (2010) Towards benchmarking of AMQP. In: DEBS. ACM, pp 99\u2013100","DOI":"10.1145\/1827418.1827438"},{"key":"1986_CR10","doi-asserted-by":"crossref","unstructured":"Hunkeler U, Truong HL, Stanford-Clark AJ (2008) MQTT-S - A publish\/subscribe protocol for wireless sensor networks. In: COMSWARE. IEEE, pp 791\u2013798","DOI":"10.1109\/COMSWA.2008.4554519"},{"key":"1986_CR11","unstructured":"Mimouni SE, Bouhdadi M (2015) Formal modeling of the simple text oriented messaging protocol using event-b method. In: AICCSA. IEEE Computer Society, pp 1\u20134"},{"key":"1986_CR12","unstructured":"Osinski T, Dandoush A (2018) XMPP as a scalable multi-tenants isolation solution for onos-based software-defined cloud networks. In: CNSM. IEEE Computer Society, pp 300\u2013303"},{"issue":"9","key":"1986_CR13","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/35.312841","volume":"32","author":"BC Neuman","year":"1994","unstructured":"Neuman BC, Ts\u2019o TY (1994) Kerberos: an authentication service for computer networks. IEEE Commun Mag 32(9):33\u201338","journal-title":"IEEE Commun Mag"},{"key":"1986_CR14","doi-asserted-by":"crossref","unstructured":"Li R, Yin J, Zhu H (2020) Modeling and analysis of RabbitMQ using UPPAAL. In: TrustCom. IEEE, pp 79\u201386","DOI":"10.1109\/TrustCom50675.2020.00024"},{"key":"1986_CR15","unstructured":"UPPAAL (2022) http:\/\/uppaal.org. Accessed 6 March 2022"},{"key":"1986_CR16","doi-asserted-by":"crossref","unstructured":"Behrmann G, David A, Larsen KG (2004) A tutorial on UPPAAL. In: SFM, Springer, Lecture Notes in Computer Science, vol 3185, pp 200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"1986_CR17","doi-asserted-by":"crossref","unstructured":"Dobbelaere P, Esmaili KS (2017) Kafka versus RabbitMQ: A comparative study of two industry reference publish\/subscribe implementations: Industry paper. In: DEBS. ACM, pp 227\u2013238","DOI":"10.1145\/3093742.3093908"},{"key":"1986_CR18","doi-asserted-by":"crossref","unstructured":"Matic M, Ivanovic S, Antic M, Papp I (2019) Health monitoring and auto-scaling RabbitMQ queues within the smart home system. In: ICCE-Berlin. IEEE, pp 380\u2013384","DOI":"10.1109\/ICCE-Berlin47944.2019.8966229"},{"key":"1986_CR19","doi-asserted-by":"crossref","unstructured":"Prabhu C, Gandhi RV, Jain AK, Lalka VS, Thottempudi SG, Rao PP (2019) A novel approach to extend KM models with Object Knowledge Model (OKM) and Kafka for big data and semantic web with greater semantics. In: CISIS, Springer, Advances in Intelligent Systems and Computing, vol 993, pp 544\u2013554","DOI":"10.1007\/978-3-030-22354-0_48"},{"issue":"6","key":"1986_CR20","doi-asserted-by":"publisher","first-page":"333","DOI":"10.12720\/jcm.13.6.333-337","volume":"13","author":"A Ofenloch","year":"2018","unstructured":"Ofenloch A, Greif F (2018) A flexible distributed simulation environment for Cyber-Physical Systems using ZeroMQ. J Commun 13(6):333\u2013337","journal-title":"J Commun"},{"key":"1986_CR21","first-page":"8338,616:1","volume":"2021","author":"S Chaisawat","year":"2021","unstructured":"Chaisawat S, Vorakulpipat C (2021) Towards achieving personal privacy protection and data security on integrated E-Voting model of blockchain and message queue. Secur Commun Networks 2021:8338,616:1\u20138338,616:14","journal-title":"Secur Commun Networks"},{"key":"1986_CR22","doi-asserted-by":"crossref","unstructured":"Hong XJ, Yang HS, Kim YH (2018) Performance analysis of RESTful API and RabbitMQ for microservice web application. In: ICTC. IEEE, pp 257\u2013259","DOI":"10.1109\/ICTC.2018.8539409"},{"key":"1986_CR23","doi-asserted-by":"crossref","unstructured":"Estrada N, Astudillo H (2015) Comparing scalability of message queue system: ZeroMQ vs RabbitMQ. In: CLEI. IEEE, pp 1\u20136","DOI":"10.1109\/CLEI.2015.7360036"},{"key":"1986_CR24","doi-asserted-by":"crossref","unstructured":"Ionescu VM (2015) The analysis of the performance of RabbitMQ and ActiveMQ. In: RoEduNet. IEEE, pp 132\u2013137","DOI":"10.1109\/RoEduNet.2015.7311982"},{"key":"1986_CR25","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-662-63079-2_8","volume":"15","author":"A Rodr\u00edguez","year":"2021","unstructured":"Rodr\u00edguez A, Kristensen LM, Rutle A (2021) Verification of the MQTT IoT protocol using property-specific CTL sweep-line algorithms. Trans Petri Nets Other Model Concurr 15:165\u2013183","journal-title":"Trans Petri Nets Other Model Concurr"},{"key":"1986_CR26","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-662-60651-3_5","volume":"14","author":"A Rodr\u00edguez","year":"2019","unstructured":"Rodr\u00edguez A, Kristensen L M, Rutle A (2019a) Formal modelling and incremental verification of the MQTT IoT protocol. Trans Petri Nets Other Model Concurr 14:126\u2013145","journal-title":"Trans Petri Nets Other Model Concurr"},{"key":"1986_CR27","unstructured":"Rodr\u00edguez A, Kristensen LM, Rutle A (2019b) On CTL model checking of the MQTT IoT protocol using the sweep-line method. In: PNSE@Petri Nets\/ACSD, CEUR-WS.org, CEUR Workshop Proceedings, vol 2424, pp 57\u201372"},{"key":"1986_CR28","unstructured":"Rodr\u00edguez A, Kristensen LM, Rutle A (2018) On modelling and validation of the MQTT IoT protocol for M2M communication. In: PNSE@Petri Nets\/ACSD, CEUR-WS.org, CEUR Workshop Proceedings, vol 2138, pp 99\u2013118"},{"key":"1986_CR29","doi-asserted-by":"crossref","unstructured":"Xu J, Yin J, Zhu H, Xiao L (2021) Modeling and verifying producer-consumer communication in Kafka using CSP. In: ECBS. ACM, pp 9:1\u20139:10","DOI":"10.1145\/3459960.3459961"},{"issue":"6","key":"1986_CR30","doi-asserted-by":"publisher","first-page":"1324","DOI":"10.1007\/s11390-020-0537-8","volume":"35","author":"Q Lin","year":"2020","unstructured":"Lin Q, Wang S, Zhan B, Gu B (2020) Modelling and verification of real-time publish and subscribe protocol using UPPAAL and simulink\/stateflow. J Comput Sci Technol 35(6):1324\u20131342","journal-title":"J Comput Sci Technol"},{"key":"1986_CR31","doi-asserted-by":"crossref","unstructured":"Fei Y, Zhu H, Li X (2018) Modeling and verification of NLSR protocol using UPPAAL. In: TASE. IEEE Computer Society, pp 108\u2013115","DOI":"10.1109\/TASE.2018.00022"},{"key":"1986_CR32","doi-asserted-by":"crossref","unstructured":"Sun M, Lu Y, Feng Y, Zhang Q, Liu S (2021) Modeling and verifying the CKB blockchain consensus protocol. Mathematics 9(22)","DOI":"10.3390\/math9222954"},{"key":"1986_CR33","doi-asserted-by":"crossref","unstructured":"Kwon S, Son S, Choi Y, Lee J (2021) Protocol fuzzing to find security vulnerabilities of RabbitMQ. Concurr Comput Pract Exp 33(23)","DOI":"10.1002\/cpe.6012"},{"key":"1986_CR34","doi-asserted-by":"publisher","first-page":"40,735","DOI":"10.1109\/ACCESS.2018.2856904","volume":"6","author":"H Li","year":"2018","unstructured":"Li H, Niu Y, Yi J, Li H (2018) Securing offline delivery services by using Kerberos authentication. IEEE Access 6:40,735\u201340,746","journal-title":"IEEE Access"},{"key":"1986_CR35","doi-asserted-by":"crossref","unstructured":"Xu C, Zhu H, Xie W (2017) Modeling and verifying identity authentication security of HDFS using CSP. In: APSEC. IEEE Computer Society, pp 259\u2013268","DOI":"10.1109\/APSEC.2017.32"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-022-01986-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11036-022-01986-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-022-01986-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,24]],"date-time":"2022-10-24T09:23:20Z","timestamp":1666603400000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11036-022-01986-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,9]]},"references-count":35,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["1986"],"URL":"https:\/\/doi.org\/10.1007\/s11036-022-01986-8","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"value":"1383-469X","type":"print"},{"value":"1572-8153","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,9]]},"assertion":[{"value":"4 April 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 May 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"We have no competing interests to declare that are relevant to the content of this article. This article does not involve ethics issues.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Competing interests"}}]}}