# Formal Safety Assessment and Improvement of DDS Protocol for Industrial Data Distribution Service
## 8 Conclusions  
In this paper, the security of the DDS protocol is mainly discussed. In order to evaluate and improve the security of the protocol, we adopt a model checking method combining the Dolev-Yao attack model and CPN theory. First, the protocol is originally  
\begin{table}
\begin{tabular}{c c c c c} \hline \hline
**Scheme** & **Attack Model** & **Targeted Attack** & **Intuitive Graphic** & **State Space** &
\begin{tabular}{c} **Verify Functional** \\ **Correctness** \\ \end{tabular} \\ \hline Ref. [15] & NO & YES & YES & NO & YES \\ Ref. [18] & NO & NO & NO & YES \\ Ref. [38] & YES & YES & NO & YES \\ Our scheme & YES & YES & YES & YES \\ \hline \hline \end{tabular}
\end{table}
Table 8: Scheme comparison analysis.  
modeled and validated using the CPN Tools modeling tool and CPN theory; second, in order to evaluate the security of the original model, the Dolev-Yao attacker model was introduced; finally, a new approach to deal with the security flaws in the protocol is proposed. Security verification should be performed using CPN Tools after the original protocol has been improved, it is shown that the improved scheme effectively resists man-in-the-middle replay attack and increases protocol security. In addition, CPN Tools can introduce ASK-CTL temporal logic formulas to describe the nature of the system, use rigorous mathematical theory to analyze the correctness of the model, and the verification results show that the model meets the expected design requirements. However, during the research process for this paper, a man-in-the-middle attack on the network channel is the only attack that is considered in this paper, as other attacks on the protocol are not considered. With the advent of Industry 4.0 and the new popularity of the Internet of Vehicles (IoV), the DDS protocol in the automotive field will have large-scale applications with its advantages [40]. In the future, it can be considered to be applied in the wireless network environment on the premise of achieving industrial real-time performance and accuracy. The next step will consider the secure storage of the private key within the protocol and the security of the protocol under other forms of attack.  
Conceptualization, J.D., C.G., and T.F.; methodology, J.D.; software, C.G.; validation, J.D., C.G., and T.F.; formal analysis, J.D. and C.G.; investigation, J.D., C.G., and T.F.; resources, J.D.; data curation, C.G.; writing--original draft preparation, J.D.; writing--review and editing, J.D. and C.G.; visualization, J.D. and C.G.; supervision, T.F.; project administration, J.D.; funding acquisition, J.D. and T.F. All authors have read and agreed to the published version of the manuscript.  
This research was funded by the National Natural Science Foundation of China (Grant No. 62162039, 61762060) and the Foundation for the Key Research and Development Program of Gansu Province, China (Grant No.20 YF3 GA016), and the Science and Technology Planning Project of Gansu Province, China (Grant No. 20 JR10 RA185).  
Not applicable.  
Not data were used to support this study.  
The authors would like to thank all editors and reviewers for their valuable comments and suggestions and all funding for the great help and support of this research.  
The authors declare no conflicts of interest.  
The following abbreviations are used in this manuscript:  
\begin{tabular}{l l} DDS & Data Distribution Service \\ CPN & Colored Petri Net \\ IoT & Internet of Things \\ AMQP & Advanced Message Queuing Protocol \\ MQTT & Message Queuing Telemetry Transport \\ QoS & Quality of Service \\ ML & Markup Language \\ GUI & Graphical User Interface \\ TCPN & Timed Colored Petri Nets \\ HCPN & Hierarchical Colored Petri Nets \\ OMG & Object Management Group \\ SOME/IP & Scalable service-Oriented MiddlewarE over IP \\ DDSI & DDS Interoperability Wire Protocol \\ DCPS & Data-Centric Publish-Subscribe \\ \end{tabular}