# Formal Analysis of DTLS-SRTP Combined Protocol Based on Logic of Events
## 1 Introduction  
Security protocols on networks offer a diverse range of security services. Given the potential prevalence of malicious activities in complex network environments, the design of security protocols is susceptible to errors. Deficiencies in protocol design may inadvertently provide avenues for attackers. Existing technologies predominantly focus on the analysis of individual protocols without considering the impracticality of concurrent use of other protocols. For instance, when sharing keys between entities and servers, these keys may be established by various sub-protocols; however, the security of keys cannot be assured in the interaction among sub-protocols. If a specific key exchange protocol is employed for key establishment, the preservation of security among sub-protocols cannot be guaranteed [1]. In addition, independent protocols may interact in diverse manners. For example, users may select the same key for two distinct network services, or servers may employ identical keys for different protocols [2]. Even if individual protocols are proven to be secure, there is no security guarantee when they share keys. Consequently, a more formalized reasoning about compositional security is required, where security assurances for composite protocols can be inferred from the security guarantees of individual protocols. One notable advancement in the formal analysis of composite protocols is the Protocol Composition Logic (PCL) [3]. PCL provides support for compositional reasoning and has been applied in numerous case studies. Formal methods have proven their utility in the design and analysis of security protocols. They provide a rigorous framework and techniques that facilitate the discovery of new vulnerabilities and conduct thorough security analyses. Rooted in precise mathematical concepts and language, formal methods offer clear semantics and explicit expressions. Theorem proving is a crucial technique within formal methods, characterizing security protocols as axiomatic systems and delineating desired properties as theorems to be proven. The focus of theorem proving is on the correctness of protocols, and the process of proofis challenging to automate. Logic of Events Theory [4; 5] represents a logical approach to theorem proving, employed to delineate the message actions of encryption protocols during interactive processes. Logic of Events Theory formalizes the foundational primitives of security protocols, establishing a model encompassing addresses and events to demonstrate the security properties of protocols. In-depth research by numerous experts and scholars has led to significant advancements in Logic of Events Theory. In the ever-evolving landscape of digital communication, the security of real-time audio transmission has emerged as a significant topic in both research and practice. With the proliferation of VoIP and other real-time communication technologies, the imperative to safeguard communication content from eavesdropping and tampering has become increasingly pressing. The introduction of the DTLS-SRTP protocol is a proactive response to this demand, aiming to provide a robust and efficient solution for secure communication. The core concept behind DTLS-SRTP is the integration of the Datagram Transport Layer Security (DTLS) protocol with the Secure Real-time Transport Protocol (SRTP) to overcome the challenges faced by SRTP in connectionless and multipath communication environments [6]. DTLS is a channel security protocol that encompasses integrated key management, parameter negotiation, and secure data transmission [7; 8]. Its security mechanisms include key exchange, authentication, and data encryption, ensuring that both communicating parties can engage in real-time audio transmission within a secure environment. In addition, DTLS-SRTP employs cutting-edge cryptographic algorithms and protocol design principles to provide the highest level of protection. In summary, the primary contributions of this paper are as follows:  
1.