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.

As IoT in a multi-server environment increases resources’ utilization, more and more problems of IoT authentication and key agreement are being revealed. The Authentication and Key Agreement (AKA) protocol plays an important role in solving these problems. Many AKA protocols have been proposed, and some of them support their own verifications. However, a unifying verification framework for multi-server IoT is lacking. In this article, we propose a formal verification framework of AKA protocols for multi-server IoT (FVF-AKA). It supports the construction of CSP models for the AKA protocol, the implementation of the CSP models in PAT with C#, and the verification of formal models. With the help of C#, many complex functions in the AKA protocol can be implemented. We also design an algorithm to support automatic conversion from the CSP model to the PAT model. FVF-AKA can verify four fundamental properties (deadlock freedom, entity legitimacy, timeout delay, and session key consistency). It also supports the verification of security properties for the AKA protocol suffering from four different attacks (relay attacks, denial of service attacks, server spoofing attacks, and session key attacks). Our approach can be applied to most AKA protocols for multi-server IoT generally. By applying FVF-AKA to two AKA protocols, we can verify whether they satisfy the fundamental properties and analyze their security properties in vulnerable environments. Our work would help to analyze the AKA protocol for multi-server IoT and provide the foundation for the analysis of enhancing its security and robustness.