# Formal Safety Assessment and Improvement of DDS Protocol for Industrial Data Distribution Service
## 4 DDS Protocol Modeling
### CPN Modeling for DDS Protocol  
In order to precisely represent the network communication process and to reduce the model's complexity, the protocol model is condensed into three layers: top, middle, and bottom. A detailed description of the message flow follows the subdividing of each layer, then subdividing each layer leads to a detailed analysis of the protocol's message flow. Figure 4: Message flow model of DDS protocol. \begin{table}
\begin{tabular}{c c} \hline \hline
**Name** & **Color Set Definition** \\ \hline SignS & \begin{tabular}{c} colset SignS = product NONCE * PrivateKey; \\ Enc \\ \end{tabular} & \begin{tabular}{c} colset Enc = product Shared Key * PublicKey; \\ colset SignMF = product HashNenc * \\ \end{tabular} \\ SignMF & \begin{tabular}{c} privateKey; \\ \end{tabular} \\ MSG1 & \begin{tabular}{c} colset MSG1 = product NONCE * CertM; \\ \end{tabular} \\ MSG2 & \begin{tabular}{c} colset MSG2 = record n:NONCE * cCertS * \\ \end{tabular} \\ MSG3 & \
\begin{tabular}{c} colset MSG3 = record e:Enc * sm:SignMF; \\ \end{tabular} \\ Decryption function &
\begin{tabular}{c} fun DecryptionKey(k:PublicKey) = case k of \\ PKm => SKm 1 PKs => SKs; \\ \end{tabular} \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Model’s color set definition. Figure 5 displays the top-level CPN model of the DDS protocol. A top-level model simulates the interaction between protocols in a broad sense, including both parties involved in the protocol, network channels, and transmission information. Figure 6 illustrates the mid-level protocol design, which has five alternative transitions and six places. When the two parties establish interaction, the alternative transition Publisher on the left describes the process of participant M establishing connection information to participant S, and the alternative transition Publisher' describes the process of M processing and replying to the connection information. The middle NETBase describes the communication process of the transmitted information in the network channel. The alternative transition Subscriber on the right describes the process of S processing and replying to the connection information. Substitute transition Subscriber' describes the process of S's processing and comparison of security data. The alternative transition NETBase is illustrated in Figure 7. In the process of establishing a channel for the transmission of publish-subscribe messages, the transition Mes1, Mes2, and Mes3 imitate the process of initiating an authenticated message from M to S and the authentication of the message delivered by S to M, respectively. Figure 5: A top-level model for the DDS protocol. Figure 6: The mid-level model of the DDS protocol. The alternative transition Publisher is illustrated in Figure 8. Through the place of Msg1, the transition of NmCertM is assembled into an information packet and sent to the network channel. The alternative transition Subscriber is illustrated in Figure 9. After the data are successfully received, the validity of the certificate is verified through the Validate of the place. After the verification is successful, the message is synthesized through the transition of CombineMes, and the message is sent to the network channel through Msg2. The alternative transition Publisher' is illustrated in Figure 10. After successfully receiving the data, decompose the message through the transition of DecM2, get the atomic message and verify the legitimacy of the message through Validate of the place. If the  
Figure 8: Publisher internal model for alternative transition. Figure 7: Alternative transition NETBase’s internal model. Figure 9: Subscriber internal model for alternative transition. verification is successful, the message is synthesized through the transition EnchKa, and the message is sent to the network channel through Msg3.