Formal Analysis of DTLS-SRTP Combined Protocol Based on Logic of Events

Abstract

Security analysis of composite protocols is a critical issue in the field of network security. In complex network environments, the traditional approach of analyzing a single protocol becomes inadequate when dealing with scenarios involving multiple interactions and combinations of protocols. To address this challenge, this paper extends the Logic of Events Theory (LoET) and proposes a method for proving the security of composite protocols. Building upon the Logic of Events Theory, we introduce sequential composition rules, ordering rules, and relevant axioms. We incorporate the concept of invariants and formally abstract the DTLS-SRTP protocol, thereby verifying the mutual authentication and confidentiality of the two sub-protocols. In conclusion, our study demonstrates that the extended Logic of Events Theory offers an effective means of verifying the security of composite protocols.

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 proof is 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:

• Extension of sequential composition axioms, ordering axioms, and relevant invariants based on the foundation of Logic of Events Theory. Introduction of the concept of invariants and proposal of a proof method for verifying the security of composite protocols.
• Abstraction of the security properties of the DTLS-SRTP protocol using Logic of Events. Formal depiction of the interaction processes of its sub-protocols, DTLS and SRTP, and separate proofs for mutual authentication and confidentiality.
• Proof of the security of the DTLS-SRTP protocol after sequential composition using the proposed composite protocol proof method.

The remainder of this paper is organized as follows. Related work is presented in Section 2. Section 3 introduces Logic of Events Theory, elucidating the properties to be satisfied during protocol analysis and the axioms and rules necessary for proving mutual authentication and confidentiality. Section 4 outlines the composite protocol proof method and introduces the DTLS-SRTP protocol. Section 5 provides a detailed exposition of the security proof for the DTLS-SRTP protocol. Finally, Section 6 offers our conclusions and outlines avenues for future work.

2. Related Work

When analyzing composite protocols, it is commonly assumed that protocol participants have successfully shared secrets to abstract sub-protocols. However, the combination of two independently proven secure encryption protocols may not necessarily maintain security. Fábrega et al. introduced the chain space method [9], which has yielded theoretical results regarding the composition of protocols. The chain space method attempts to identify abstract properties that two protocols must satisfy for secure composition. In 2019, Hagihara et al. [10] also formally verified a voting protocol using the chain space method. However, this method exhibits deficiencies in the efficiency of verifying composite protocols and considering sequential combinations. Canetti et al. proposed a generic framework [11] for proving the secure composition of protocols and revised this framework in 2020, addressing multiple ambiguities and modeling issues present in previous versions [12]. In 2022, Canetti et al. [13] used this secure composition framework to model and analyze the Signal messaging protocol.

The Logic of Events Theory adopted in this paper shares similarities with this framework, but LoET demonstrates a stronger characterization capability for the security properties of protocols and is more conducive to the verification of protocol properties. Datta et al. [14] introduced Protocol Composition Logic (PCL), whose authentication proof process is concise and supports compositional reasoning for complex security protocols. In 2021, Lei et al. [15] extended the PCL theory to formally analyze a security protocol based on a public-key cryptosystem from the aspects of authentication, confidentiality, and data integrity. However, PCL can only describe a subset of cryptographic protocols and cannot handle protocols with data signatures, a limitation addressed by Logic of Events Theory. Cremers et al. [16] introduced the concept of independence in composite protocol sets, defined relevant security property classes, and proved many theorems within this class, but did not specifically discuss how to perform sequential protocol composition. In 2020, Zhang et al. [17] proposed an automated compositional analysis technique for authentication protocols, reducing verification time. However, formal methods are still required for compositional reasoning in protocol combinations. In 2021, Gondron et al. [18] constructed a general framework to express the vertical composition of application and channel protocols, contrasting sequential and parallel combinations with horizontal composition. They independently verified several layers of protocol stacks. In our work, we also consider this aspect, using the DTLS protocol as the transport layer handshake protocol and the SRTP protocol as the application protocol for sequential composition, proving its security properties.

3. Logic of Events

Logic of Events [4], is one of the formal methods that describes protocols and algorithms in distributed systems. The fundamental framework of Logic of Events mainly consists of a theoretical foundation, a theoretical system (including logical axioms and inference), and a formal description system [5]. The theoretical foundation is employed to model the initial cryptographic systems. The theoretical system provides a comprehensive reasoning system for the proofs of cryptographic protocols. The formal description system describes and defines the thread sequences and matching sessions of the protocol.

3.1. Symbol Description

The basic symbols and semantics of LoET are shown in

Table 1. The basic notations and semantics.

Symbol	Semantics
ID	Participants in the agreement
Atom	Unpredictable information
Data	Plaintext
e	Event
E	Event set
nonce	Random number
loc(e)	The location of event e
has	Logic contains
<	Cause and effect sequence of events
||	Logically independent
Key(e)	The secret key of the principal of event e
bs	Basic sequence

.

3.2. Basic Definition

3.2.1. Sequence of Events

In the context of identifying points where information is transmitted during execution, such points are referred to as events, denoted as e. The definition of $info\left(e\right)$ is the raw information associated with the event e. The structure of an event sequence is defined as $<E,loc,<,info>$ where < represents a transmission relation on E. In Logic of Events Theory, the address $loc\left(e\right)$ of an event e is the entity where it occurs. The causal sequence of events on the same entity is denoted as $(e^{\prime }<e\wedge loc\left(e^{\prime }\right)=loc\left(e\right))$, abbreviated as $e^{\prime }<{ }_{loc}e$.

3.2.2. Event Classes

Event classes categorize events during the protocol interaction process to characterize the actions of the protocol. The event classes define seven types of events: send, receive, challenge, signature, verification, encryption, and decryption. Each event class encompasses associated information, and the types of this information are determined by the corresponding event class. The list of types includes the following:

$$\begin{array}{c}New:EClass\left(Atom\right)\hfill \\ Send,Rcv:EClass\left(Data\right)\hfill \\ Encrypt,Decrypt:EClass(Data\times Key\times Atom)\hfill \\ Sign,Verify:EClass(Data\times Id\times Atom)\hfill \end{array}$$

3.3. Axiom System

Logic of Events theory (LoET) utilizes axioms and relevant inference rules to prove the security of protocols. This paper will exclusively introduce the axioms and rules relevant to protocol analysis.

3.3.1. Key Axiom

The Key Axiom defines the matching relationships between keys. A symmetric key matches only itself, and a private key matches the corresponding public key. Matching keys is a symmetric relationship and no two principals have the same private key. Additionally, the Key Axiom requires three additional functions defined as $Honest:Id\to B$, Id represents the honest subject, the type is Boolean, $MatchingKeys:Key\to Key\to B$, the function constructs the relationship between keys, and the type is Boolean. $PrivKey:Id\to Atom$. The function allocates an atom to each body, the type is the atomic type. The specific definition of the Key Axiom is as follows:

$$\begin{array}{c}AxiomK:\forall A,B:Id.k,k^{\prime }:Key.\forall a:Atom\\ \left(\begin{array}{c}MatchingKeys(k,k^{\prime })\iff MatchingKeys(k^{\prime },k)\wedge \hfill \\ MatchingKeys\left(Symm\right(a),k)\iff k=Symm\left(a\right)\wedge \hfill \\ MatchingKeys\left(PrivKey\right(A),k)\iff k=A\wedge \hfill \\ MatchingKeys(A,k)\iff k=PrivKey\left(A\right)\wedge \hfill \\ PrivKey\left(A\right)=PrivKey\left(B\right)\iff A=B\hfill \end{array}\right)\end{array}$$

(1)

3.3.2. Causal Axiom

The Causality Axiom comprises three axioms: $AxiomR$, $AxiomV$, and $AxiomD$. It establishes the causal correspondence between events in the $Rcv$ class, $Verify$ class, and $Decrypt$ class with their respective events in the $Send$ class, $Sign$ class, and $Encrypt$ class. In other words, before any receiving or verification event, there must be a corresponding sending or signing event with the relevant information. This is specifically expressed as follows:

$$\left(\begin{array}{c}AxiomR:\forall e:E\left(Rcv\right)\exists e^{\prime }:E\left(Send\right).(e^{\prime }<e)\wedge Rcv\left(e\right)=Send\left(e^{\prime }\right)\\ AxiomV:\forall e:E\left(Verify\right):e^{\prime }:E\left(Sign\right).(e^{\prime }<e)\wedge Verify\left(e\right)=Sign\left(e^{\prime }\right)\\ AxiomD:\forall e:E\left(Decrypt\right)\exists e^{\prime }:E\left(Encrypt\right).(e^{\prime }<e)\wedge DEMatch(e,e^{\prime })\\ DEMatch(e,e^{\prime })\equiv {\hspace{0.17em}}_{def}plaintext\left(e\right)=plaintext\left(e^{\prime }\right)\wedge \\ ciphertext\left(e\right)=ciphertext\left(e^{\prime }\right)\wedge MatchingKeys(key\left(e\right),key\left(e^{\prime }\right))\end{array}\right)$$

(2)

3.3.3. Honest Axiom

In a protocol, honest entities do not disclose their private keys. Therefore, signature events have honest signers, and encryption and decryption events involving the private key of an honest entity must occur on that entity. The Honest Axiom is formulated as follows:

$$\begin{array}{c}AxiomS:\\ \forall A:Id.\forall s:E\left(Sign\right).\forall e:E\left(Encrypt\right).\forall d:E\left(Decrypt\right).Honest\left(A\right)\Rightarrow \\ \left(\begin{array}{c}singer\left(s\right)=A\Rightarrow \left(loc\right(s)=A)\wedge \hfill \\ key\left(e\right)=PrivateKey\left(A\right)\Rightarrow \left(loc\right(e)=A)\wedge \hfill \\ key\left(d\right)=PrivateKey\left(A\right)\Rightarrow \left(loc\right(d)=A)\hfill \end{array}\right)\end{array}$$

(3)

3.4. Expansion of Logic of Events Theory

3.4.1. Invariant Concept

In the process of proving the mutual authentication property of a protocol, the Honest Rule is employed to infer whether honest entities in the protocol have executed the correct operations. The set of formulas proved by Honesty Rules in the process of proving authentication and confidentiality are called invariants. The set of invariants includes two invariants, ${\mathsf{\Gamma }}_1$ and ${\mathsf{\Gamma }}_2$, where ${\mathsf{\Gamma }}_1$ and ${\mathsf{\Gamma }}_2$ are given by the following expressions:

$$\begin{array}{c}{\mathsf{\Gamma }}_1,{\mathsf{\Gamma }}_2\vDash auth(bs,n)\equiv {\hspace{0.17em}}_{def}\forall A,B.\forall thr.\wedge \hfill \\ (Honest\left(A\right)\wedge Honest\left(B\right)\wedge Q_1(A,B)\wedge Q_2(A,B)\wedge \hfill \\ A\ne B\wedge loc\left(thr\right)=bs(A,B,thr))\hfill \end{array}$$

3.4.2. Sequential Combination Rules

The sequential composition rule ensures the correct combination of sub-protocols. Assuming the post-event of protocol $Q_1$ is e and the pre-event of protocol $Q_2$ is $e^{\prime }$, then there exists a sequential composition $\forall e,e^{\prime }\in (E\left(Send\right)\vee E\left(Rcv\right)\vee E\left(Encrypt\right)\vee E\left(Decrypt\right))$. The events e and $e^{\prime }$ each contain relevant information and include the atoms a and b, i.e., e has a and $e^{\prime }$ has b. The specific definition of e has a is as follows:

$$\left(\begin{array}{c}\mathrm{e}hasa{\equiv }_{def}\\ (e\in E(New)\wedge New(e\left)hasa\right)\vee \\ (e\in E(Send)\wedge Send(e\left)hasa\right)\vee \\ (e\in E(\mathrm{Re}ceive)\wedge \mathrm{Re}ceive(e\left)hasa\right)\vee \\ (e\in E(Encrypt)\wedge Encrypt(e\left)hasa\right)\vee \\ (e\in E(Decrypt)\wedge Decrypt(e\left)hasa\right)\vee \\ (e\in E(Sign)\wedge Sign(e\left)hasa\right)\vee \\ (e\in E(Verify)\wedge Verify(e\left)hasa\right)\end{array}\right)$$

(4)

If the post-event output of protocol $Q_1$ matches the pre-event input of protocol $Q_2$, then the protocols $Q_1$ and $Q_2$ can be sequentially composed, and as a result,

$$\left(\begin{array}{c}\forall Q_1,Q_2:(Q_1\ne Q_2),\forall e,e^{\prime }:(\mathrm{e}\in Q_1,e^{\prime }\in Q_2)\forall a,b:Atom\\ Matching(a,b)\iff Matching(b,a)\wedge \\ Send\left(e\right)=Rcv\left(e^{\prime }\right)\vee Sign\left(e\right)=Verify\left(e^{\prime }\right)\vee Decrypt\left(e\right)=Encrypt\left(e^{\prime }\right)\end{array}\right)$$

(5)

Lemma 1.

If the protocol Q is a sequential composition of protocols $Q_1$ and $Q_2$, and if the following formulas hold for the subjects A and B in protocol Q, we can conclude that the invariant set ${\mathsf{\Gamma }}_1\cup {\mathsf{\Gamma }}_2$ also holds for protocol Q.

$$\left(\begin{array}{c}\forall e:E,\forall A,B:Id,A\in Q_1,B\in Q_2\hfill \\ \forall th{r}_1,th{r}_2.(inOneof(e,th{r}_1,bss,A)\wedge inOneof(e,th{r}_2,bss,B))\hfill \end{array}\right)\Rightarrow Q\supset {\mathsf{\Gamma }}_1,{\mathsf{\Gamma }}_2$$

3.4.3. Sorting Rules

The combination of these axioms allows the derivation of sequential relationships between behaviors of different threads. We introduce new predicates, $Fresh$ and $FirstSend$. $Fresh$ signifies that, except for the subject itself, no other subject can receive the atomic action a or any message containing a. $FirstSend$ indicates that a subject sends a particular message for the first time, and neither the subject nor any other subject has sent that message before. If a message m is sent in thread $th{r}_1$ and m is fresh before being sent, it implies that $th{r}_1$ is sending message m for the first time. If a different thread $th{r}_2$ performs an action $m^{\prime }$ involving m, then the sending action of $th{r}_1$ must occur before the mentioned action of $th{r}_2$. The definitions are as follows:

$$\left(\begin{array}{c}New\left(e\right)=m\Rightarrow Fresh(e,m)\vee \\ \forall A:Id.\exists e:E\left(New\right).\forall e^{\prime }:E\left(Send\right)Joc\left(e\right)=loc\left(e^{\prime }\right)=A\wedge \\ e<e^{\prime }\wedge e^{\prime }has{m}^{\prime }\wedge Fresh(e^{\prime },m^{\prime })\Rightarrow FirstSend(e^{\prime },m,m^{\prime })\vee \\ \forall A:Id.\forall e^{\prime }:E.\wedge e^{\prime }hasm\wedge loc\left(e^{\prime }\right)=A\Rightarrow e^{\prime }<e\end{array}\right)$$

(6)

3.5. Protocol Authentication Proof Process

In the protocol proof process based on LOET, we first abstract the interaction flow between the initiator and responder of the protocol. Subsequently, we prove matching sessions based on the preconditions and postconditions of the protocol states. Finally, we consider the proof of weak authentication properties and strong authentication properties. In addition to proving authentication properties, it is essential to consider the definition of basic sequences in the protocol and analyze the one-sided sequences of the initiator and responder. The proof of protocol authentication can only be established when both sides of the sequence are proven to possess strong authentication properties. The protocol security proof process based on Logic of Events is illustrated in Figure 1. The specific steps are as follows.

(1)

Begin by formally describing the protocol, constructing standardized basic sequences for initiators and responders, and defining the strong authentication properties that the protocol needs to verify.

(2)

Under the assumption of honest entities, analyze the thread messages and define actions on the selected thread as an instance of the basic sequence. Specify the matching sessions that need to be proven and proceed to demonstrate unilateral authentication for initiators or responders.

(3)

Confirm whether the matching events comply with the current matching session. If they do, proceed with subsequent proofs. If not, continue filtering matching sessions until the current matching event satisfies weak matching.

(4)

With the weak matching confirmed, analyze the matching length during the protocol interaction process. Prove strong matching sessions based on relevant axioms and rules in Logic of Events.

(5)

If the strong authentication property for one party is successfully proven, proceed to prove the strong authentication property for the other party. If only one party satisfies the strong authentication property, it indicates that the protocol as a whole still does not meet the strong authentication requirement. Successful proof in both directions is necessary for the overall strong authentication property of the protocol to be established.

4. Combination Protocol Proof Method

In this section, we interpret the sequential composition of the protocol as syntactic operations on the basic sequence and propose relevant methods for proving the security properties of composite protocols. Clearly, the sequential composition of protocols does not yield a unique result. Typically, when we perform sequential composition of protocols, we consider specific role combinations. For instance, in the case of two-party protocols, we define corresponding initiator and responder roles. The ordering rules and sequential composition rules are the primary rules used to construct modular correctness proofs for protocols. Composite protocols must respect each other’s invariants. The method for proving properties of the sequential composition of two protocols involves the following steps:

(1)

Construct and prove the security properties of each protocol $Q_1$ and $Q_2$ separately.

(2)

Identify the invariant sets ${\mathsf{\Gamma }}_1$ and ${\mathsf{\Gamma }}_2$ used in the proof of security properties for the two sub-protocols. The formulas contained in these sets are typically proven using honest rules in both protocols.

(3)

Independently verify that the security properties of the two sub-protocols are preserved in the invariant set ${\mathsf{\Gamma }}_1\cup {\mathsf{\Gamma }}_2$. If the postcondition of protocol $Q_1$ matches the precondition of protocol $Q_2$, apply the ordering rule to sequentially compose them.

(4)

Prove that the invariant set ${\mathsf{\Gamma }}_1\cup {\mathsf{\Gamma }}_2$ holds for the security properties of the composite protocol Q. The specific process of proving the protocol combination based on Logic of Events is shown in Figure 2.

5. Formal Analysis of DTLS-SRTP Combined Protocol

The DTLS-SRTP protocol is designed for point-to-point media sessions involving only two participants, distinguished as the authenticating party and the authenticated party. In this context, the client is defined as the authenticated party, while the server is defined as the authenticating party. We operate under the premise that both communicating parties possess pre-agreed symmetric keys. Given the practical scenario in which data packets may be lost or reordered in a UDP environment, we employ an extended of Logic of Events Theory to formally prove the mutual authentication between the communicating parties. Subsequently, we demonstrate the confidentiality of the communication process to ensure the security of the protocol.

5.1. DTLS-SRTP Protocol Analysis

DTLS (Datagram Transport Layer Security) and SRTP (Secure Real-time Transport Protocol) can be combined to provide end-to-end security, especially in real-time communication. The protocol is divided into a handshake phase and a key exchange phase, as illustrated in the sequence diagram in Figure 3.

Here are the steps of the protocol interaction:

(1)

The client and server establish a connection by initiating a handshake negotiation to establish a secure communication channel. During the handshake, the client sends a timestamp $T_s$ and a random number $R_1$ to the server.

(2)

The server sends information containing the digital certificate $CA$ and the session key K to the client.

(3)

The client verifies the digital certificate $CA$. Upon successful verification, it encrypts the random number $R_2$ using the key K and sends it to the server. Data encrypted with the public key can only be decrypted by the server’s private key. Once the DTLS handshake is successful, the communicating parties share session data.

(4)

The server verifies the client’s digital certificate and decrypts the encrypted $R_2$ using its private key. At this point, the handshake phase is completed, and the key exchange phase begins.

(5)

After the DTLS protocol connection is established, the SRTP protocol requires a set of encryption keys and authentication keys to ensure the confidentiality and integrity of media data. The shared key $P{K}_s$ is calculated through an encryption algorithm with the following formula: $P{K}_s=K_s\times C_{pk}=K_c\times S_{pk}$, where $K_s$, $C_{pk}$, $K_c$, and $S_{pk}$ are encryption parameters negotiated by the SRTP protocol.

(6)

Using the derived encryption key $P{K}_s$, the client encrypts a message $R_3$ and sends it to the server. The server also sends an encrypted message $R_4$ to the client. Once both parties successfully decrypt the messages, the protocol’s key exchange phase is complete, and secure transmission of communication data can begin.

5.2. DTLS Protocol Mutual Authentication Certificate

Abstract the interaction process of DTLS protocol through Logic of Events and describe the protocol, as shown in Figure 4.

To verify the mutual authentication of the DTLS protocol, one must employ the concept of a basic sequence to sequence the interaction process. The following formula is the basic sequence of DTLS protocol.

$$\begin{array}{c}{I}_1=N\mathrm{e}w\left(m_1\right),Encrypt\left(<m_1,P{K}_B,S_1>\right),Send(<A,S_1>)\hfill \\ I_2=Rcv(<B,S_2>)\hfill \\ I_3=Decrypt\left(<<m_1,m_2>,S{K}_A,S_2>\right),Encrypt\left(<<m_2,S_2>,k_{\mathrm{m}},S_3>\right),Send\left(S_3\right)\hfill \\ R_1=Rcv(<A,S_1>)\hfill \\ R_2=Decrypt\left(<m_1,S{K}_B,S_1>\right),N\mathrm{e}w\left(m_2\right),Encrypt\left(<<m_1,m_2>,P{K}_A,S_2>\right),Send(<B,S_2>)\hfill \\ R_3=Rcv\left(S_3\right)\hfill \\ R_4=Decrypt\left(<m_2,S{K}_B,S_3>\right)\hfill \end{array}$$

Based on the obtained basic sequence, define the DTLS protocol as $protocol\left([I_1,I_2,I_3,R_1,R_2,R_3]\right)$. The strong identity authentication property we need to verify is $DS\vDash auth(I_3,2)\wedge DS\vDash auth(R_3,3)$.

Starting with the proof of $DS\vDash auth(I_3,2)$, assume honest entities $A\ne B$, and that they follow the DTLS protocol. Assume thread $\mathrm{th}{\mathrm{r}}_1$ is an instance of $I_3$, and let $e_0<{\hspace{0.17em}}_{loc}{e}_1<{\hspace{0.17em}}_{loc}{e}^2<{\hspace{0.17em}}_{loc}\dots <{\hspace{0.17em}}_{loc}{e}_6$ be the actions on ${\mathrm{thr}}_1$. Then, $e_0,\dots ,e_6$ all have A as their principal. For some atoms $m_1,m_2,S_1,S_2,S_3$

$$\left(\begin{array}{c}N\mathrm{e}w\left(e_0\right)=m_1\wedge Encrypt\left(e_1\right)=<<m_1,P{K}_B,S_1>>\wedge Send\left(e_2\right)=S_1\wedge \hfill \\ Rcv\left(e_3\right)=S_2\wedge Decrypt\left(e_4\right)<<m_1,m_2>,S{K}_A,S_2>\hfill \end{array}\right)$$

(7)

According to $AxiomS$ and $AxiomD$, there exists an event $e^{\prime }$ such that $e^{\prime }<e_4\wedge DEMatch(e_4,e^{\prime })\wedge loc\left(e^{\prime }\right)=B$ holds. Thus, $Encrypt\left(e^{\prime }\right)=<<m_1,m_2>,\mathrm{S}{\mathrm{K}}_{\mathrm{A}},S_2>$. Since entity B follows the DTLS protocol, the event $e^{\prime }$ must be an instance member of this protocol’s basic sequence. The actions containing $Encrypt\left(\right)$ are $I_1,I_2,I_3,R_1,R_2,R_3$. If $e^{\prime }$ is an instance of $I_3$, then for atoms $m_1^{\prime },m_2^{\prime },S_2^{\prime }$ and entity C, there exists an event $e_0^{\prime }<{\hspace{0.17em}}_{loc}{e}^{\prime }$; thus, $New\left(e_0^{\prime }\right)=m_1^{\prime }\wedge Encrypt\left(e^{\prime }\right)=<<m_1^{\prime },m_2^{\prime }>,\mathrm{S}{\mathrm{K}}_{\mathrm{A}},S_2^{\prime }>$. By the lemma, it follows that $e_0=e_0^{\prime }$; hence, $A=loc\left(e_0\right)=loc\left(e_0^{\prime }\right)=B$, which contradicts the assumption. Therefore, $I_3$ is ruled out. If $e^{\prime }$ is an instance of $R_1$, then for atoms $m_1^{\prime \prime },m_2^{\prime \prime },S_1^{\prime },S_2^{\prime \prime }$ and entity D, there exist events $e_0^{\prime },e_1^{\prime },e_2^{\prime },e_3^{\prime },e_4^{\prime }$ on entity B. We can derive the following equation:

$$\left(\begin{array}{c}{e}_0^{\prime }{<}_{loc}{e}_1^{\prime }{<}_{loc}{e}_2^{\prime }{<}_{loc}{e}_3^{\prime }=e^{\prime }{<}_{loc}{e}_4^{\prime }\wedge Rc\nu \left(e_0^{\prime }\right)=<D,S_1^{\prime }>\wedge \hfill \\ Decrypt\left(e_1^{\prime }\right)=<m_1^{\prime \prime },S{K}_B,S_1^{\prime }>New\left(e_2^{\prime }\right)=m_2^{\prime \prime }\wedge \hfill \\ Encrypt\left(e_3^{\prime }\right)=<<m_1^{\prime \prime },m_2^{\prime \prime }>,S{K}_A,S_2^{\prime \prime }>\wedge Send\left(e_4^{\prime }\right)=S_2^{\prime \prime }\hfill \end{array}\right)$$

(8)

Therefore, the first two messages in the original thread are $e_2$ and $e_3$. It can be determined that $Send\left(e_2\right)=S_1=Rcv\left(e_0^{\prime }\right)$ and $Send\left(e_4^{\prime }\right)=S_2=Rcv\left(e_3\right)$. This establishes a weak matching session of length 2. To prove a strong matching session, it is necessary to demonstrate that $e_2<e_0^{\prime }$ and $e_4^{\prime }<e_3$. Since $Rcv\left(e_0^{\prime }\right)=S_1$, then $e_0^{\prime }$ possesses $New\left(e_0\right)$. Assuming $A\ne B$, there exists a sending event S releasing a random number m between $e_0$ and $e_0^{\prime }$. If $e_2<h$, then the ordering is $e_2<e_0^{\prime }$. By using $AxiomF$ and the lemma, we can derive the following expression:

$$\left(\begin{array}{c}<D,<m_1^{\prime \prime },m_2^{\prime \prime }>,{\mathrm{SK}}_A,S_2^{\prime \prime }>=<B,<m_1,m_2>,{\mathrm{SK}}_A,S_2^{\prime }>\\ D=A,m_1^{\prime \prime }=m_1,m_2^{\prime \prime }=m_2,S_1^{\prime }=S_1,S_2^{\prime \prime }=S_2,e_3^{\prime }=e^{\prime }\end{array}\right)$$

(9)

If $e_0<{\hspace{0.17em}}_{loc}h<{\hspace{0.17em}}_{loc}{e}_2$, then h must be a member of some other thread of subject A. However, there could be other sequences in the protocol that accidentally release the random number m before the intended release. By the lemma, we know that there is no sending action between $e_0$ and $e_2$ in thread $th{r}_1$, meaning that the random number m will not be released before $e_2$. We infer $e_4^{\prime }<e_3$ from $AxiomF$ and $AxiomS$. Since $e_3$ possesses $m_2$ and $m_2=New\left(e_2^{\prime }\right)$, which is not released before $e_4^{\prime }$, we have proven $DS\vDash auth(I_3,2)$. Similarly, it can be demonstrated that $DS\vDash auth(R_3,3)$. Thus, mutual authentication property of the DTLS protocol is established.

5.3. SRTP Protocol Confidentiality Certification Process

The simplified interaction process of the SRTP protocol is shown in Figure 5 below:

(1)

Since subjects A and B have previously negotiated the key $k_s$ in the preceding subprotocol, subject A sends the random number $N_a$ to subject B.

(2)

Subject B encrypts the random number using the key $k_s$ and sends the encrypted message to A.

(3)

After receiving the ciphertext, subject A decrypts it using the decryption key $k_s^{\prime }$, obtaining the random number n, which is then encrypted and sent to subject B.

(4)

Subject B verifies the consistency of the sent and received random numbers, and upon confirmation, begins communication with subject A using the key $k_s$. The formal description of the SRTP protocol using Logic of Events theory is illustrated in Figure 6 below.

Using Logic of Events theory, the basic sequence of the SRTP protocol is as follows:

$$\begin{array}{c}{I}_1=N\mathrm{e}w\left({\mathrm{n}}_1\right),\mathrm{Send}\left(<\mathrm{A},{\mathrm{n}}_1>\right)\hfill \\ I_2=\mathrm{Rcv}(<B,S_4>),Decrypt\left(<<{\mathrm{n}}_1,S_3>,k_s,S_4>\right),Encrypt\left(<<{\mathrm{n}}_1>,k_s^{\prime },S_5>>\right),\mathrm{Send}\left(S_5\right)\hfill \\ R_1=\mathrm{Rcv}(<A,{\mathrm{n}}_1>),Encrypt\left(<<{\mathrm{n}}_1,S_3>,k_s,S_4>\right),\mathrm{Send}(<B,S_4>)\hfill \\ R_2=\mathrm{Rcv}\left(S_5\right),Decrypt\left(<<{\mathrm{n}}_1>,k_s^{\prime },S_5>>\right)\hfill \end{array}$$

First, it is necessary to introduce the concepts of $SafeMsg(M,s,K)$ and $Safethr(X,s)$. The definition of $SafeMsg(M,s,K)$ indicates that the secret S in message M is protected by a key from the key set K, where the key set K consists of the public or private keys of subjects A and B. $Safethr(X,s)$ represents that all secrets s sent in the protocol’s sending events are sent by subject X, and they maintain the same security properties. The formal definition of $Safethr(X,s)$ is as follows.

$$\begin{array}{c}Safethr(X,s){\equiv }_{def}\forall M.SafeMsg(M,s,K)\hfill \\ {\equiv }_{def}\left(\begin{array}{c}\forall X.\forall e\in E\left(Send\right).\forall M.\hfill \\ Send\left(e\right)=M\wedge loc\left(e\right)=X\hfill \end{array}\right)\hfill \end{array}$$

(10)

Let $(e_1,e_2,\dots ,e_i,\dots ,e_n)$ represent the complete event sequence of the protocol, where $e_i$ denotes the i-th sending event executed by the intruder. Before the $Send$ event in $I_2$, both subject A and subject B adhere to the honesty axiom in the protocol’s event sequence. Therefore, in the event sequence of the protocol, the random number n is a confidential challenge shared between subject A and subject B, as expressed by the following equation.

$$\left(\begin{array}{c}\forall A^{\prime },B^{\prime }:Id.\exists e\in E\left(New\right).\exists e^{\prime }\in E\left(Encrypt\right).\hfill \\ New\left(e\right)=n\wedge Encrypt\left(e^{\prime }\right)=(<...,N_a,...>,{k^{\prime }}_b,s_1)\hfill \\ \wedge loc\left(e\right)=loc\left(e^{\prime }\right)=A^{\prime }\wedge Honest\left(A^{\prime }\right)\hfill \end{array}\right)\Rightarrow B^{\prime }=B$$

(11)

For the honest subject A, who serves as the protocol initiator, A generates a random number n and encrypts it using the key of subject B before sending it out. The transmitted information adheres to the format described in the protocol and is not altered. Therefore, it can be inferred that the identities of both subjects are known. This is expressed by the following formula.

$$\forall e\in E\left(New\right).New\left(e\right)=m\wedge loc\left(e\right)=A^{\prime }\Rightarrow Honest\left(A^{\prime }\right)\wedge A^{\prime }=A$$

That is, if there exists an honest subject who performs the last sending event in the sequence, it can be determined that this subject is the honest subject A. Through the analysis of the sending events in the basic sequence, we can obtain the following:

$$\left(\begin{array}{c}\forall X.\exists e_1,e_2:E\left(Send\right).\exists S\hfill \\ S=Encrypt\left(<<\mathrm{n}>,k_s^{\prime },S_5>>\right)\wedge New\left(e_1\right)=n\wedge loc\left(e_1\right)=X\Rightarrow \hfill \\ Send\left(e_2\right)=S\left|\right|n\wedge loc\left(e_2\right)=X\hfill \end{array}\right)$$

(12)

In the protocol’s sending events, if a subject encrypts and sends a ciphertext S or a random number n, then based on the above formula, it is possible to determine the subject who performed that sending event. Suppose there is any $thr$ as an instance on $R_1$, let $e_3<e_4<e_5<e_6<e_7$ be the actions on $thr$, and the addresses of $e_0,e_1,\dots ,e_7$ are all $B^{\prime }$. For the atoms $s_3,n,k_s,n^{\prime },{k^{\prime }}_s,{s^{\prime }}_3$, we have

$$\begin{array}{c}Rcv\left(e_3\right)={s^{\prime }}_3\wedge Decrypt\left(e_4\right)=(<B^{\prime },n,k_s>,k_a,{s^{\prime }}_3)\wedge \hfill \\ Encrypt\left(e_5\right)=(msg,k_b,s_4)\wedge Send\left(e_6\right)={s^{\prime }}_4\hfill \end{array}$$

For $e_4\in E\left(Decrypt\right)$, $Decrypt\left(e_4\right)=(<A^{\prime },n,k_s>,k_b,s_4)$ according to the decryption axiom $AxiomD$:

$$DEMatch(e_4^{\prime },e_4)\equiv \left(\begin{array}{c}plaintext\left(e_4^{\prime }\right)=plaintext\left(e_4\right)\hfill \\ \wedge ciphertext\left(e_4^{\prime }\right)=ciphertext\left(e_4\right)\hfill \\ \wedge MatchingKeys(key\left(e_4^{\prime }\right);key\left(e_4\right)\hfill \end{array}\right)$$

(13)

Therefore, we have $Has(A^{\prime },n)$, where $A^{\prime }=loc\left(e_4^{\prime }\right)$, considering the events before the decryption event $e_7$:

$$\left(\begin{array}{c}\forall B^{\prime }:Id.\forall e\in E\left(Send\right).\forall e^{\prime }\in E.\forall M.\hfill \\ Send\left(e\right)=M\wedge SafeMsg(M,s,k)\hfill \\ \wedge e<e^{\prime }<e_7\wedge loc\left(e^{\prime }\right)=B^{\prime }\hfill \\ \wedge Has(A^{\prime },n)\hfill \end{array}\right)\Rightarrow \left(\begin{array}{c}\exists k\in \mathcal{K}.Has(A^{\prime },k)\hfill \\ \vee \exists e^{\prime \prime }\in E\left(New\right).\hfill \\ New\left(e^{\prime \prime }\right)=n\wedge loc\left(e^{\prime \prime }\right)=A^{\prime }\hfill \end{array}\right)$$

(14)

Therefore, we have $Has(A^{\prime },k_a)\vee Has(A^{\prime },k_b)$, and by the key axiom $AxiomK$, we can deduce $A^{\prime }=A\vee A^{\prime }=B$. Further, by the following formula:

$$\begin{array}{cc}\hfill & \left(\begin{array}{c}\mathit{Safethr}(X,s)\wedge \mathit{Has}(X,M)\\ \wedge \mathit{SafeMsg}(M,s,k)\end{array}\right)\Rightarrow \left(\begin{array}{c}\exists k\in K.\mathit{Has}(X,k)\vee \\ \exists e\in E\left(New\right).New\left(e\right)=n\\ \wedge \mathit{loc}\left(e\right)=X\end{array}\right)\hfill \\ \hfill & \Rightarrow \left(\forall X:Id.Has(X,n)\Rightarrow (X=A\vee X=B)\right)\hfill \end{array}$$

(15)

In summary, the SRTP protocol satisfies confidentiality.

5.4. Sequential Combination of DTLS and SRTP

We now proceed to prove the security properties of the combined protocol by combining the mutual authentication of the DTLS protocol and the secrecy of the SRTP protocol. In this process, we follow the previously mentioned method of proving sequential composition. According to the above proof process, ${\mathsf{\Gamma }}_1$ satisfies the mutual authentication property of the DTLS protocol, where ${\mathsf{\Gamma }}_1$ contains the set of formulas

$${\mathsf{\Gamma }}_1\equiv \left\{\begin{array}{c}signer\left(s_1\right)=A\Rightarrow (loc\left(s_1\right)=A)\wedge key\left(e^{\prime }\right)=privateKey\left(A\right)\Rightarrow \hfill \\ \left(loc\left(e^{\prime }\right)\right)=A\wedge key\left(e^{\prime \prime }\right)=privateKey\left(A\right)\Rightarrow (loc\left(e^{\prime \prime }\right)=A)\hfill \\ signer\left(s_2\right)=B\Rightarrow (loc\left(s_2\right)=B)\wedge key\left(e_1^{\prime }\right)=privateKey\left(B\right)\Rightarrow \hfill \\ \left(loc\left(e_1^{\prime }\right)\right)=B\wedge key\left(e_2^{\prime \prime }\right)=privateKey\left(B\right)\Rightarrow (loc\left(e_2^{\prime \prime }\right)=B)\hfill \end{array}\right\}$$

(16)

where the invariant set ${\mathsf{\Gamma }}_2$ for the SRTP protocol is empty, as the honesty rules were not used in proving the secrecy property of the protocol. Therefore, the invariant set becomes ${\mathsf{\Gamma }}_1\cup {\mathsf{\Gamma }}_2={\mathsf{\Gamma }}_1$. We can conclude that the security property of the DTLS protocol satisfies the combined invariant set.

By replacing the post-event of the DTLS protocol with the pre-event of the SRTP protocol and applying the sequential composition rule, we obtain:

$${\mathsf{\Gamma }}_1\vDash \mathrm{Send}\left(e\right)=\mathrm{Rcv}\left(e^{\prime }\right)\vee \mathrm{Sign}\left(e\right)=\mathrm{Verify}\left(e^{\prime }\right)\vee \mathrm{Decrypt}\left(e\right)=\mathrm{Encrypt}\left(e^{\prime }\right)$$

From the proof processes of the DTLS and SRTP protocols, we can infer that the thread $th{r}_1$ containing the last send event in the DTLS protocol and the thread $th{r}_2$ containing the first receive event in the SRTP protocol are the same. Based on Lemma 1, when the conditions hold for the principals A and B in both sub-protocols, we can conclude that the invariant set ${\mathsf{\Gamma }}_1\cup {\mathsf{\Gamma }}_2$ holds for the combined protocol Q. Thus, the security property of the DTLS-SRTP composite protocol is established.

5.5. Results and Analysis

This chapter employs an extended LoET to provide a security proof for the DTLS-SRTP protocol. Through an analysis of the protocol interaction process, a description of the protocol authentication procedure, and the formal modeling of the protocol’s basic sequences, both sub-protocols are formally modeled. By deriving formulas, it is demonstrated that the sub-protocols satisfy mutual authentication and confidentiality. The proof results indicate that the DTLS-SRTP protocol is secure under the fulfillment of the underlying assumptions.

We have chosen the classic theorem-proving method of Protocol Composition Logic (PCL) [19,20] for comparison with LoET. The selection of PCL and Event Logic for comparison is motivated by the similarity of these two theories, both capable of proving the security of composite protocols. Through analysis and comparison, several conclusions can be drawn:

• PCL is limited in proving the authenticity of signature protocols only and cannot analyze other non-signature authentication protocols. In contrast, LoET can analyze the authenticity of both signature and non-signature protocols.
• PCL lacks a definition for the pre-order behavior sequences of threads, leading to a lack of rigor in modeling the interaction actions among entities in cryptographic protocol instances. This deficiency fails to ensure the correlation between different basic sequences. In contrast, LoET explicitly defines the thread mechanisms for formal modeling of cryptographic protocols. The specification of thread states is achieved through atomic independence, ensuring the rigor of the modeling.
• PCL, during the analysis of cryptographic protocols, can only capture a partial content of the security properties, demonstrating a lesser capability in characterizing protocol security properties compared to LoET.

Model checking [21] is an automated method for verifying concurrent systems with a finite state space. It exhaustively explores the state space to determine whether safety goals can be achieved. The proof methodology in LoET treats the satisfaction of protocol specifications as logical propositions. Through a set of inference rules, it employs deductive reasoning to prove these propositions. Model checking often encounters issues such as state explosion and numerical limitations, making it suitable for relatively small-scale cryptographic protocols. On the other hand, LoET focuses more on the correctness of cryptographic protocols without the need to consider problems like state explosion.

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:

• 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.
• 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.