The Data Distribution Service (DDS) constructs a highly available data transmission middleware based on the publish-subscribe model, widely used in the Internet of Things environment. To improve the security of DDS, the Object Management Group formulated the DDS Security, which provides security mechanisms for DDS in the form of security plugins. However, the security of the DDS Security protocol has not been fully analyzed. We analyze DDS Security through formal methods. We model the security goals and protocol flow of the DDS Security using ProVerif and evaluate whether its security goals can be met in different scenarios. Our analysis confirms previously manually identified vulnerabilities in an automated way and reveals new attacks. We discovered the permission file impersonation attack, the denial of service attack, the degradation attack, and the privacy leakage attack guided by the formal analysis result. For these threats, we propose corresponding mitigation measures and recommendations.