# Formal Safety Assessment and Improvement of DDS Protocol for Industrial Data Distribution Service
## 1 Introduction  
With the Internet of Things (IoT) technology's rapid development, IoT devices are being widely used and integrated into an increasing number of applications, the basic components of IoT devices are numerous terminals, transmission networks and clouds, which correspond to the three layers of the IoT system's perception layer, network layer, and application layer [1; 2]. Each layer should apply some security rules to an IoT implementation for it to be secure. Only by resolving the security issues related to IoT can the future of IoT frameworks be guaranteed [3]. Application scenarios and the security of different levels of protocols have become crucial considerations as a result of the development of IoT technology. In many devices, IoT devices are connected through insecure connections over the Internet. For many IoT applications, including important industrial, medical, and personal ones, security is a crucial aspect. IoT protocols are generally divided into two categories, one is the transmission protocol and the other is the communication protocol. The DDS protocol is a communication protocol, and similar protocols include Advanced Message Queuing Protocol (AMQP), Message Queuing Telemetry Transport (MQTT), etc. DDS, MQTT, and AMQP are all based on the publish/subscribe model [4; 5]. The publish/subscribe framework has the characteristics of service self-discovery, dynamic expansion, and event filtering. It solves the problem of rapid acquisition of data sources, addition and exit of things in the application layer of the IoT system, interest subscription, reducing bandwidth traffic and other issues, to achieve loose coupling in space, loose coupling in time, and loose coupling in synchronization. With the help of service policies, DDS can effectively control and manage the use of resources, such as network bandwidth and memory space, and can also control data reliability, real-time and data survival time. By using these service quality policies flexibly, DDS not only in the narrowband wireless environment, but also in the broadband wiredcommunication environment, a data distribution system that meets real-time requirements can be developed. At present, there is a lack of research on the security issues of the DDS protocol. For example, there is a lack of formal security analysis and security mechanism evaluation. To solve this problem, in this paper we will use the protocol formal analysis method to model the DDS protocol and conduct security assessment. The formal analysis method refers to the method of describing the system model by mathematical or logical methods, and verifying whether the system meets the requirements through a certain form of reasoning. The use of formal analysis methods for security protocol verification was first proposed by [PERSON] and [PERSON] [6], and later adopted by [PERSON] and [PERSON] and published important results in 1983 [7]. The formal analysis tool in this paper uses CPN Tools, which can dynamically simulate the model with the help of CPN Tools [8; 9]. The visual interface allows users to observe the execution process of each step of the model and judge whether there are security vulnerabilities in the protocol model through the state space [10]. Specifically, this paper contributes to three areas:  
1. We investigate the security of the DDS protocol using formal model identification based on CPN theory and Dolev-Yao adversaries;
2. The CPN modeling tool is used to model the DDS protocol, and the model's correctness is checked. When the Dolev-Yao model is used to assess the protocol's security, it is discovered that there are security flaws;
3. In order to address the protocol's security flaws, a new improved solution is put forth, and its security is confirmed by simulating an adversary attack model. The roadmap of this paper is as follows: Section 2 discusses the current related work. Section 3 discusses the choice of tools and methods, the CPN model, and the working mechanism of the protocol.