# Formal Analysis of DTLS-SRTP Combined Protocol Based on Logic of Events
## 6 Conclusions and Future Work  
Formal methods are considered one of the most advantageous approaches for analyzing the security of security protocols. Logic of Events theory is a formal method based on subordinated theorem proving, used for analyzing the security of distributed systems and security protocols. We have demonstrated that as long as two protocols satisfy the primitives in Logic of Events theory for modeling composite protocols, they can be safely sequentially composed. This paper extends and enhances the Logic of Events theory, applying it to prove the security properties of the DTLS-SRTP protocol. The main contributions and innovations of this work are as follows:  
1. Extension of Logic of Events theory rules: Building upon the existing Logic of Events theory, we expand the predicate formulas to characterize the states of protocol principals. The extensions include predicates for expressing message freshness and the primacy of send events. We provide corresponding formal definitions, enhancing the analytical capabilities of Logic of Events theory and reducing complexity and redundancy in protocol analysis.
2. Introduction of a proof method for Logic of Events combined protocols: Extending the original proof of mutual authentication in Logic of Events theory, we introduce an expanded proof system for secrecy. This extension encompasses the characterization of message confidentiality and explicit reasoning about potential attacker behaviors. We introduce sequential composition rules to describe the security properties of combined protocols. These enhancements and innovations contribute to a more powerful and expressive Logic of Events theory, providing an effective framework for analyzing and proving the security properties of composite protocols like DTLS-SRTP.  
We propose a general method for the verification of combined protocols: any attack on a combination of two protocols can be abstracted into a basic sequence attacking one of the protocols. Building upon the current research findings, future research directions may include exploring parallel combinations and asymmetric combinations. Our combination theorem is applicable to scenarios where two protocols interact in arbitrary ways. We demonstrate how to use the extended combination theorem in Logic of Events to verify the security of a shared key protocol. However, our current focus is exclusively on the security properties of mutual authentication and confidentiality. We believe that Logic of Events theory can be further extended to encompass other security attributes.  
Conceptualization, M.X. and Y.Z.; methodology, Y.Z.; validation, Y.Z. and Z.L.; formal analysis, Y.Z. and F.C.; investigation, Z.L. and F.C.; writing--original draft preparation, Y.Z.; writing--review and editing, M.X. and Z.L. All authors have read and agreed to the published version of the manuscript.  
This work was supported by the National Natural Science Foundation of China (No. 62362033), Jiangxi \"Double Thousand Plan\" (No. JXSQ2023201009), and Jiangxi Provincial Natural Science Foundation (No. 20224 ACB202006).  
Not applicable.  
Data Availability Statement: Data are contained within the article.  
The authors declare no conflict of interest.