# Formal Safety Assessment and Improvement of DDS Protocol for Industrial Data Distribution Service
## 6 New Scheme of DDS Protocol
### Performance Analysis and Methods Comparison for New Scheme  
This section makes a comparative analysis of the improved new schemes of DDS protocol. In practical application scenarios, protocol security is particularly important. By adding a new security mechanism, the security of the protocol is improved. At the same time, when the timestamp is added in the new protocol improvement scheme, the calculation and communication will increase, and the delay of the new scheme will increase slightly compared with the original scheme. According to the improved protocol operation, we define the time spent on encryption and decryption in the protocol process as _Ten_ and _Tde_, and the time spent generating data as _Tge_, the time required for verification and hash function calculation is _Tv_ and _Th_, respectively. The time required for Entity M is: _3 Ten + Th  
\begin{table}
\begin{tabular}{c c c c c c c} \hline \hline  & \multicolumn{3}{c}{**Original Model**} & \multicolumn{3}{c}{**New Scheme**} \\ \cline{2-7}
**Type** & **REY-ATK** & **TAR-ATK** & **SPF-ATK** & **REY-ATK** & **TAR-ATK** & **SPF-ATK** \\ \hline State Space & 5830 & 680 & 420 & 12,196 & 1086 & 676 \\ Nodes & 21,319 & 1854 & 1056 & 50,418 & 3038 & 1790 \\ State Space & 21,319 & 1854 & 1056 & 50,418 & 3038 & 1790 \\ Arcs & 0 & 0 & 0 & 0 & 0 & 0 \\ Strongly Connected & 5830 & 680 & 420 & 12,196 & 1086 & 676 \\ Nodes & & & & & & \\ Strongly Connected Arcs & 21,319 & 1854 & 1056 & 50,418 & 3038 & 1790 \\ Dead Markings & 2 & 2 & 1 & 1 & 2 & 1 \\ Live transition & 0 & 0 & 0 & 0 & 0 & 0 \\ Instances & & & & & & \\ Dead transition & 0 & 0 & 0 & 0 & 0 & 0 \\ instances & & & & & & \\ \hline \hline \end{tabular}
\end{table}
Table 6: State space comparison under three attack models.  
\begin{table}
\begin{tabular}{c c c} \hline \hline
**Type** & **Original Attacker Model** & **New Scheme** \\ \hline State Space Nodes & 10,380 & 21,036 \\ State Space Arcs & 39,504 & 88,576 \\ Strongly Connected Nodes & 10,380 & 21,036 \\ Strongly Connected Arcs & 39,504 & 88,576 \\ Dead Markings & 6 & 4 \\ Live transition instances & 0 & 0 \\ Dead transition instances & 0 & 0 \\ \hline \hline \end{tabular}
\end{table}
Table 7: State space comparison between the original attacker model and the new scheme attacker model.  
Figure 22: Protocol termination status query under replay attack.  
\(+3 Tv+2 Tge\); the time required for Entity S is: \(2 Ten+Tde+3 Tv+Tge\); and the total time spent is: \(5 Ten+Tde+6 Tv+3 Tge+Th\). There is not much impact on the performance of the original protocol.  
We compared the formal analysis method used in this paper with other methods. Ref. [15] focuses on client-side attacks, models and demonstrates five attacks in independent and isolated environments, these security issues can be used as an attack method against dd's based systems; Ref. [18] proposes an ABAC-based DDS security model authorization improvement method, and incorporates the ABAC entity into the security model that defines ABAC behavior across RTPS and DCPS, and implements the model in XACML; Ref. [38] proposes an attacker model that leverages network reconnaissance provided by leaky context, combined with formal verification and model checking to arbitrarily infer the underlying topology and reachability of information flows, enabling targeted attacks, such as selective denial of service, adversarial partitioning of the data bus, or exploiting of vendor-implemented vulnerabilities. Through the comparative analysis in Table 8, the scheme proposed in this paper can not only provide an intuitive and accurate graphical description and verify the correctness of protocol functions, but also discover the attack types of the protocol. At the same time, the scheme improves the introduced attack model and solves the problem of state space explosion in traditional model checking methods, this analysis scheme can be used to conduct security analysis and research on other protocols.