{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,7]],"date-time":"2026-06-07T04:48:50Z","timestamp":1780807730328,"version":"3.54.1"},"reference-count":30,"publisher":"National Library of Serbia","issue":"1","license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ComSIS","COMPUT SCI INF SYST","COMPUT SCI INFORM SY","COMPUTER SCI INFORM","COMSIS J"],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:p>Apache Kafka is an open source distributed messaging system based on the publish-subscribe model, which achieves low latency, high throughput and good load balancing. As a popular messaging system, the transmission of messages between applications is one of the core functions of Kafka. Therefore, the reliability and security of data in the process of message transmission in Kafka have become the focus of attention. The formal methods can analyze whether a model is highly credible. Therefore, it is significant to analyze Kafka messaging mechanism which describes the communication process and rules between each module entity in Kafka from the perspective of formal methods. In this paper, we apply the process algebra CSP (Communicating Sequential Processes) and the model checking tool PAT (Process Analysis Toolkit) to analyze Kafka messaging mechanism. The results of verification show that the model caters for its specification and guarantees the reliability of messages in the normal communication process. Moreover, in order to further analyze the security of Kafka messaging mechanism, we add the intruder model and the authentication protocol Kerberos model and compare the verification results of Kafka messaging mechanism with or without the secure protocol Kerberos. The results show that the Kerberos protocol has improved the security of Kafka messaging mechanism in some aspects, but there are still some security loopholes.<\/jats:p>","DOI":"10.2298\/csis210707057x","type":"journal-article","created":{"date-parts":[[2022,12,23]],"date-time":"2022-12-23T14:49:21Z","timestamp":1671806961000},"page":"277-306","source":"Crossref","is-referenced-by-count":13,"title":["Formalization and verification of Kafka messaging mechanism using CSP"],"prefix":"10.2298","volume":"20","author":[{"given":"Junya","family":"Xu","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jiaqi","family":"Yin","sequence":"additional","affiliation":[{"name":"Northwestern Polytechnical University, Xi\u2019an, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lili","family":"Xiao","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"1078","reference":[{"key":"ref1","unstructured":"Rabbitmq., https:\/\/www.rabbitmq.com\/tutorials\/amqp-concepts.html"},{"key":"ref2","doi-asserted-by":"crossref","unstructured":"Adams, C.: Kerberos authentication protocol. In: van Tilborg, H.C.A., Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd Ed, pp. 674-675. Springer (2011), https: \/\/doi.org\/10.1007\/978-1-4419-5906-5_81","DOI":"10.1007\/978-1-4419-5906-5_81"},{"key":"ref3","doi-asserted-by":"crossref","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560-599 (1984), https:\/\/doi.org\/10.1145\/828.833","DOI":"10.1145\/828.833"},{"key":"ref4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H.: Introduction to model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1-26. Springer (2018), https:\/\/doi.org\/10.1007\/978-3-319-10575-8_1","DOI":"10.1007\/978-3-319-10575-8_1"},{"key":"ref5","unstructured":"Dobbelaere, P., Esmaili, K.S.: Kafka versus rabbitmq: A comparative study of two industry reference publish\/subscribe implementations: Industry paper. In: Proceedings of the 11th ACM International Conference on Distributed and Event-based Systems, DEBS 2017, Barcelona, Spain, June 19-23, 2017. pp. 227-238. ACM (2017), https:\/\/doi.org\/10.1145\/ 3093742.3093908"},{"key":"ref6","doi-asserted-by":"crossref","unstructured":"Eugster, P.T., Felber, P., Guerraoui, R., Kermarrec, A.: The many faces of publish\/subscribe. ACM Comput. Surv. 35(2), 114-131 (2003), https:\/\/doi.org\/10.1145\/857076.857078","DOI":"10.1145\/857076.857078"},{"key":"ref7","doi-asserted-by":"crossref","unstructured":"Fei, Y., Zhu, H.: Modeling and verifying NDN access control using CSP. In: Sun, J., Sun, M. (eds.) Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11232, pp. 143-159. Springer (2018), https:\/\/doi.org\/10.1007\/978-3-030-02450-5_9","DOI":"10.1007\/978-3-030-02450-5_9"},{"key":"ref8","doi-asserted-by":"crossref","unstructured":"Hesse, G., Matthies, C., Uflacker, M.: How fast can we insert? an empirical performance evaluation of apache kafka. In: 26th IEEE International Conference on Parallel and Distributed Systems, ICPADS 2020, Hong Kong, December 2-4, 2020. pp. 641-648. IEEE (2020), https:\/\/doi.org\/10.1109\/ICPADS51040.2020.00089","DOI":"10.1109\/ICPADS51040.2020.00089"},{"key":"ref9","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666-677 (1978), https:\/\/doi.org\/10.1145\/359576.359585","DOI":"10.1145\/359576.359585"},{"key":"ref10","doi-asserted-by":"crossref","unstructured":"Lee, V.Y., Liu, Y., Zhang, X., Phua, C., Sim, K., Zhu, J., Biswas, J., Dong, J.S., Mokhtari, M.: ACARP: auto correct activity recognition rules using process analysis toolkit (PAT). In: Donnelly, M.P., Paggetti, C., Nugent, C.D., Mokhtari, M. (eds.) Impact Analysis of Solutions  for Chronic Disease Prevention and Management - 10th International Conference on Smart Homes and Health Telematics, ICOST 2012, Artiminio, Italy, June 12-15, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7251, pp. 182-189. Springer (2012), https:\/\/ doi.org\/10.1007\/978-3-642-30779-9_23","DOI":"10.1007\/978-3-642-30779-9_23"},{"key":"ref11","doi-asserted-by":"crossref","unstructured":"Liu, A., Zhu, H., Popovic, M., Xiang, S., Zhang, L.: Formal analysis and verification of the PSTM architecture using CSP. J. Syst. Softw. 165, 110559 (2020), https:\/\/doi.org\/10.1016\/j.jss.2020.110559","DOI":"10.1016\/j.jss.2020.110559"},{"key":"ref12","doi-asserted-by":"crossref","unstructured":"Lowe, G., Roscoe, A.W.: Using CSP to detect errors in the TMN protocol. IEEE Trans. Software Eng. 23(10), 659-669 (1997), https:\/\/doi.org\/10.1109\/32.637148","DOI":"10.1109\/32.637148"},{"key":"ref13","unstructured":"PAT: Process analysis toolkit., http:\/\/pat.comp.nus.edu.sg\/"},{"key":"ref14","doi-asserted-by":"crossref","unstructured":"Prabhu, C., Gandhi, R.V., Jain, A.K., Lalka, V.S., Thottempudi, S.G., Rao, P.P.: A novel approach to extend KM models with object knowledge model (OKM) and kafka for big data and semantic web with greater semantics. In: Barolli, L., Hussain, F.K., Ikeda, M. (eds.) Complex, Intelligent, and Software Intensive Systems - Proceedings of the 13th International Conference on Complex, Intelligent, and Software Intensive Systems, CISIS 2019, Sydney, NSW, Australia, 3-5 July 2019. Advances in Intelligent Systems and Computing, vol. 993, pp. 544-554. Springer (2019), https:\/\/doi.org\/10.1007\/978-3-030-22354-0_48","DOI":"10.1007\/978-3-030-22354-0_48"},{"key":"ref15","doi-asserted-by":"crossref","unstructured":"Rooney, S., Urbanetz, P., Giblin, C., Bauer, D., Froese, F., Garc\u00b4es-Erice, L., Tomic, S.: Kafka: the database inverted, but not garbled or compromised. In: Baru, C., Huan, J., Khan, L., Hu, X., Ak, R., Tian, Y., Barga, R.S., Zaniolo, C., Lee, K., Ye, Y.F. (eds.) 2019 IEEE International Conference on Big Data (Big Data), Los Angeles, CA, USA, December 9-12, 2019. pp. 3874- 3880. IEEE (2019), https:\/\/doi.org\/10.1109\/BigData47090.2019.9005583","DOI":"10.1109\/BigData47090.2019.9005583"},{"key":"ref16","unstructured":"Sharvari T, S.N.K.: A study on modern messaging systems- kafka, rabbitmq and NATS streaming. CoRR abs\/1912.03715 (2019), http:\/\/arxiv.org\/abs\/1912.03715"},{"key":"ref17","doi-asserted-by":"crossref","unstructured":"Si, Y., Sun, J., Liu, Y., Dong, J.S., Pang, J., Zhang, S.J., Yang, X.: Model checking with fairness assumptions using PAT. Frontiers Comput. Sci. 8(1), 1-16 (2014), https:\/\/doi.org\/10.1007\/s11704-013-3091-5","DOI":"10.1007\/s11704-013-3091-5"},{"key":"ref18","doi-asserted-by":"crossref","unstructured":"Skeirik, S., Bobba, R.B., Meseguer, J.: Formal analysis of fault-tolerant group key management using zookeeper. In: 13th IEEE\/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013, Delft, Netherlands, May 13-16, 2013. pp. 636-641. IEEE Computer Society (2013), https:\/\/doi.org\/10.1109\/CCGrid.2013.98","DOI":"10.1109\/CCGrid.2013.98"},{"key":"ref19","doi-asserted-by":"crossref","unstructured":"Sun, D., Zhu, H., Fei, Y., Xiao, L., Lu, G., Yin, J.: Formalization and verification of TESAC using CSP. Int. J. Softw. Eng. Knowl. Eng. 29(11&12), 1741-1760 (2019), https:\/\/doi.org\/10.1142\/S0218194019400199","DOI":"10.1142\/S0218194019400199"},{"key":"ref20","unstructured":"Sun, J., Liu, Y., Dong, J.S.: Model checking CSP revisited: Introducing a process analysis toolkit. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation, Third International Symposium, ISoLA 2008, Porto Sani, Greece, October 13-15, 2008. Proceedings. Communications in Computer and Information Science, vol. 17, pp. 307-322. Springer (2008), https:\/\/doi.org\/10.1007\/978-3-540-88479-8_ 22"},{"key":"ref21","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 709-714. Springer (2009), https:\/\/doi.org\/10.1007\/978-3-642-02658-4_59","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"ref22","unstructured":"Tbatou, Z., Asimi, A., Asimi, Y., Sadqi, Y., Guezzaz, A.: A new mutuel kerberos authentication protocol for distributed systems. Int. J. Netw. Secur. 19(6), 889- 898 (2017), http:\/\/ijns.jalaxy.com.tw\/contents\/ijns-v19-n6\/ijns-2017-v19-n6-p889-898.pdf"},{"key":"ref23","doi-asserted-by":"crossref","unstructured":"Thampibal, L., Vatanawood, W.: Formalizing railway network using hierarchical timed coloured petri nets. In: ICIT 2019 - The 7th International Conference on Information Tech nology: IoT and Smart City, Shanghai, China, December 20-23, 2019. pp. 338-343. ACM (2019), https:\/\/doi.org\/10.1145\/3377170.3377221","DOI":"10.1145\/3377170.3377221"},{"key":"ref24","unstructured":"Treat, T.: Benchmarking nats streaming and apache kafka., https:\/\/dzone.com\/articles\/benchmarking-nats-streaming-and-apachekafka"},{"key":"ref25","doi-asserted-by":"crossref","unstructured":"Vucnik, M., Svigelj, A., Kandus, G., Mohorcic, M.: Secure hybrid publish-subscribe messaging architecture. In: Begusic, D., Rozic, N., Radic, J., Saric, M. (eds.) 2019 International Conference on Software, Telecommunications and Computer Networks, SoftCOM 2019, Split, Croatia, September 19-21, 2019. pp. 1-5. IEEE (2019), https:\/\/doi.org\/10.23919\/SOFTCOM.2019.8903868","DOI":"10.23919\/SOFTCOM.2019.8903868"},{"key":"ref26","doi-asserted-by":"crossref","unstructured":"Wang, G., Koshy, J., Subramanian, S., Paramasivam, K., Zadeh, M., Narkhede, N., Rao, J., Kreps, J., Stein, J.: Building a replicated logging system with apache kafka. Proc. VLDB Endow. 8(12), 1654-1655 (2015), http:\/\/www.vldb.org\/pvldb\/vol8\/p1654-wang.pdf","DOI":"10.14778\/2824032.2824063"},{"key":"ref27","doi-asserted-by":"crossref","unstructured":"Wang, H., Zhu, H., Xiao, L., Fei, Y.: Formalization and verification of the openflow bundle mechanism using CSP. Int. J. Softw. Eng. Knowl. Eng. 28(11-12), 1657-1677 (2018), https: \/\/doi.org\/10.1142\/S0218194018400223","DOI":"10.1142\/S0218194018400223"},{"key":"ref28","doi-asserted-by":"crossref","unstructured":"Wu, H.: Research proposal: Reliability evaluation of the apache kafka streaming system. In: Wolter, K., Schieferdecker, I., Gallina, B., Cukier, M., Natella, R., Ivaki, N.R., Laranjeiro, N. (eds.) IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops 2019, Berlin, Germany, October 27-30, 2019. pp. 112-113. IEEE (2019), https: \/\/doi.org\/10.1109\/ISSREW.2019.00055","DOI":"10.1109\/ISSREW.2019.00055"},{"key":"ref29","doi-asserted-by":"crossref","unstructured":"Wu, H., Shang, Z.,Wolter, K.: Performance prediction for the apache kafka messaging system. In: Xiao, Z., Yang, L.T., Balaji, P., Li, T., Li, K., Zomaya, A.Y. (eds.) 21st IEEE International Conference on High Performance Computing and Communications; 17th IEEE International Conference on Smart City; 5th IEEE International Conference on Data Science and Systems, HPCC\/SmartCity\/DSS 2019, Zhangjiajie, China, August 10-12, 2019. pp. 154-161. IEEE (2019), https:\/\/doi.org\/10.1109\/HPCC\/SmartCity\/DSS.2019.00036","DOI":"10.1109\/HPCC\/SmartCity\/DSS.2019.00036"},{"key":"ref30","doi-asserted-by":"crossref","unstructured":"Wu, H., Shang, Z.,Wolter, K.: TRAK: A testing tool for studying the reliability of data delivery in apache kafka. In: Wolter, K., Schieferdecker, I., Gallina, B., Cukier, M., Natella, R., Ivaki, N.R., Laranjeiro, N. (eds.) IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops 2019, Berlin, Germany, October 27-30, 2019. pp. 394-397. IEEE (2019), https:\/\/doi.org\/10.1109\/ISSREW.2019.00101","DOI":"10.1109\/ISSREW.2019.00101"}],"container-title":["Computer Science and Information Systems"],"original-title":[],"language":"en","deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T06:31:57Z","timestamp":1721889117000},"score":1,"resource":{"primary":{"URL":"https:\/\/doiserbia.nb.rs\/Article.aspx?ID=1820-02142200057X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023]]}},"URL":"https:\/\/doi.org\/10.2298\/csis210707057x","relation":{},"ISSN":["1820-0214","2406-1018"],"issn-type":[{"value":"1820-0214","type":"print"},{"value":"2406-1018","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]}}}