Verification of RabbitMQ with Kerberos Using Timed Automata

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.