# Formal Safety Assessment and Improvement of DDS Protocol for Industrial Data Distribution Service
## 2 Related Work  
Security studies are critical to the DDS protocol. Based on the analysis of the security threats faced by DDS and the corresponding strategies, [PERSON] et al. [11] propose a DDS secure communication middleware model, including identity authentication, authority control, and data encryption and decryption functions. Although this method combines the discovery mechanism and Quality of Service (QoS) negotiation mechanism of DDS, realizes the custom configuration of security protection level and encryption algorithm, and meets the flexibility and efficiency requirements of upper-layer applications, it will make the discovery of DDS secure communication middleware match. There is a small increase in latency and publish-subscribe latency. [PERSON] et al. [12] propose a way to expand the combination of DDS built-in topics and digital certificates to realize DDS identity authentication. Although this method ensures the security of the data distribution service, it consumes a lot of computing time and affects the real-time performance of the system. Focusing on the lack of fairness, consistency, and integrity of identity authentication and key agreement protocols, [PERSON] et al. [13] propose a high-security identity authentication protocol based on Diffie-Hellman key exchange and asymmetric encryption. Although this method solves the security problems, such as lack of fairness in key negotiation, inability to verify the consistency of shared key, and lack of integrity of session process in the original protocol, it is not flexible enough for users to configure security services. [PERSON] et al. [14] propose a new method sDDS-Sec, which is a method to apply DDS security extensions to sDDS. Although this approach enables secure and reliable pub/sub communication in low-power wireless networks in IoT scenarios, the availability of platforms is not widely applicable.  
[PERSON] et al. [15] details five attack methods that may be used in client-side attacks against DDS-based systems, which are based on 5 DDS security questions [16]. Through modeling and demonstration, then combined into an end-to-end verification scenario, the experiments show that these security issues are not addressed, or may reveal new security issues. The security functions and threats of protocol standards are well investigated and deduced in the literature. However, the security characteristics of protocol stacks can only be ascertained by modeling and demonstrations rather than through rigorous formal analysis. [PERSON] et al. [17] combined three communication protocols suitable for automotive and IoT scenarios. A multi-protocol gateway is proposed to successfully facilitate the data exchange between different entities, expand the applicability of the target technology in V2X scenarios, and at the same time confirm the compatibility between protocols. [PERSON] et al. [18] proposed a new approach to improve the authorization of the DDS security model using ABAC and formalized the decision-making process with a proof of decidability. Therefore, it is crucial to use formal methods to examine security vulnerabilities that arise during protocol interaction [19].  
In summary, DDS protocol security analysis lacks formal verification. Based on the CPN theory, this paper simulates the interaction process of the DDS protocol, and introduces attackers by simulating the interaction process of the protocol to discover the security problems of the protocol itself. Then we propose a new scheme based on protocol standard improvement and verify its security. The new scheme is verified to be more secure.