Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Mobile Networks and Applications
Published in: Mobile Networks and Applications 5/2022

09-05-2022

Verification of RabbitMQ with Kerberos Using Timed Automata

Authors: Ran Li, Jiaqi Yin, Huibiao Zhu, Phan Cong Vinh

Published in: Mobile Networks and Applications | Issue 5/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

RabbitMQ, an implementation of Advanced Message Queuing Protocol (AMQP), is a very popular message middleware. It supports concurrency, guarantees sequential consistency, and enables independent applications and services to communicate. Consequently, it is of great significance to ensure the secure communication of RabbitMQ. Therefore, Kerberos, a network authentication protocol, is introduced to combine with RabbitMQ to address this security issue. In this paper, we apply formal methods to model and verify RabbitMQ with Kerberos. By utilizing UPPAAL, RabbitMQ is abstracted to timed automata. Further, we validate the constructed model with the simulator in UPPAAL. On this basis, we verify whether RabbitMQ meets some basic but essential properties, including Reachability of Data, Concurrency, Sequence Consistency and Heartbeat Mechanism. Additionally, the security property Secure Communication is verified as well. From the verification results via UPPAAL, it can be found that RabbitMQ can totally cater for these properties and it maintains secure communication under the umbrella of Kerberos.
previous article A Semantic Knowledge based Context-aware Formalism for Smart Border Surveillance System
next article Modeling and Verifying PSO Memory Model Using CSP

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
Show more products
Literature
1.
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–208
2.
Jiang Y, Liu Q, Qin C, Su J, Liu Q (2019) Message-oriented middleware: A review. In: BigCom. IEEE, pp 88–97
3.
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–159
4.
5.
6.
7.
8.
9.
Appel S, Sachs K, Buchmann AP (2010) Towards benchmarking of AMQP. In: DEBS. ACM, pp 99–100
10.
Hunkeler U, Truong HL, Stanford-Clark AJ (2008) MQTT-S - A publish/subscribe protocol for wireless sensor networks. In: COMSWARE. IEEE, pp 791–798
11.
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–4
12.
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–303
13.
Neuman BC, Ts’o TY (1994) Kerberos: an authentication service for computer networks. IEEE Commun Mag 32(9):33–38CrossRef
14.
Li R, Yin J, Zhu H (2020) Modeling and analysis of RabbitMQ using UPPAAL. In: TrustCom. IEEE, pp 79–86
15.
16.
Behrmann G, David A, Larsen KG (2004) A tutorial on UPPAAL. In: SFM, Springer, Lecture Notes in Computer Science, vol 3185, pp 200–236
17.
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–238
18.
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–384
19.
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–554
20.
Ofenloch A, Greif F (2018) A flexible distributed simulation environment for Cyber-Physical Systems using ZeroMQ. J Commun 13(6):333–337CrossRef
21.
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–8338,616:14
22.
Hong XJ, Yang HS, Kim YH (2018) Performance analysis of RESTful API and RabbitMQ for microservice web application. In: ICTC. IEEE, pp 257–259
23.
Estrada N, Astudillo H (2015) Comparing scalability of message queue system: ZeroMQ vs RabbitMQ. In: CLEI. IEEE, pp 1–6
24.
Ionescu VM (2015) The analysis of the performance of RabbitMQ and ActiveMQ. In: RoEduNet. IEEE, pp 132–137
25.
Rodríguez 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–183MathSciNetCrossRef
26.
Rodríguez 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–145CrossRef
27.
Rodríguez 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–72
28.
Rodríguez 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–118
29.
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–9:10
30.
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–1342CrossRef
31.
Fei Y, Zhu H, Li X (2018) Modeling and verification of NLSR protocol using UPPAAL. In: TASE. IEEE Computer Society, pp 108–115
32.
Sun M, Lu Y, Feng Y, Zhang Q, Liu S (2021) Modeling and verifying the CKB blockchain consensus protocol. Mathematics 9(22)
33.
Kwon S, Son S, Choi Y, Lee J (2021) Protocol fuzzing to find security vulnerabilities of RabbitMQ. Concurr Comput Pract Exp 33(23)
34.
Li H, Niu Y, Yi J, Li H (2018) Securing offline delivery services by using Kerberos authentication. IEEE Access 6:40,735–40,746CrossRef
35.
Xu C, Zhu H, Xie W (2017) Modeling and verifying identity authentication security of HDFS using CSP. In: APSEC. IEEE Computer Society, pp 259–268
Metadata
Title
Verification of RabbitMQ with Kerberos Using Timed Automata
Authors
Ran Li
Jiaqi Yin
Huibiao Zhu
Phan Cong Vinh
Publication date
09-05-2022
Publisher
Springer US
Published in
Mobile Networks and Applications / Issue 5/2022
Print ISSN: 1383-469X
Electronic ISSN: 1572-8153
DOI
https://doi.org/10.1007/s11036-022-01986-8

Other articles of this Issue 5/2022

Mobile Networks and Applications 5/2022 Go to the issue

OriginalPaper

An Energy Efficient Uplink Scheduling and Resource Allocation for M2M Communications in SC-FDMA Based LTE-A Networks

OriginalPaper

Microdata Analytics of Out-of-pocket and Catastrophic Health Spending in Mexico: an Analysis by Quantiles

OriginalPaper

An Angle Rotate-QAM aided Differential Spatial Modulation for 5G Ubiquitous Mobile Networks

OriginalPaper

Digital Twin Framework for Large-Scale Optimization Problems in Supply Chains: A Case of Packing Problem

OriginalPaper

Modeling and Verifying PSO Memory Model Using CSP

OriginalPaper

A Framework for Similarity Search in Streaming Time Series based on Spark Streaming