Rigorous Security Analysis of RabbitMQ Broker with Concurrent Stochastic Games

Modern Internet of Things architectures encompass various computational logic and communication protocols. However, the security issues inherent in these systems pose significant risks, especially at the device edges. Addressing security threats on the deployed communication edges is imperative to ensure a robust and secure communication system. In this study, we propose an approach that utilizes the Concurrent Stochastic Game model (CSG) to specify the behavior of RabbitMQ Broker in the context of IoT systems precisely while considering potential data corruption attacks. For parametrizable evaluation, these attacks and their frequencies are learned. We implement the CSG model in PRISM games for automated analysis, leveraging reward Probabilistic Alternating Temporal Logic (rPATL) to model security requirements as game goals. Empirical validation of the work is presented via an industrial case study that shows how data corruption attacks can impact the sensed data in water dam infrastructure. This assessment gives valuable insights into the RabbitMQ deployment at the edge.