# Formal Analysis of DTLS-SRTP Combined Protocol Based on Logic of Events
## 5 Formal Analysis of DTLS-SRTP Combined Protocol
### 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  
Figure 5: SRTP protocol principle. 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:  
\(I_{1}=New(n_{1}),\text{Send}(\textless A,n_{1}>)\)  
\(I_{2}=\text{Rcv}(<B,S_{4}>),Decrypt(<<n_{1},S_{3}>,k_{s},S_{4}>),Encrypt (<<n_{1}>,k_{s}^{\prime},S_{5}>>),\text{Send}(S_{5})\)  
\(R_{1}=\text{Rcv}(<A,n_{1}>),Encrypt(<<n_{1},S_{3}>,k_{s},S_{4}>),\text{Send}( <B,S_{4}>)\)  
\(R_{2}=\text{Rcv}(S_{5}),Decrypt(<<n_{1}>,k_{s}^{\prime},S_{5}>>)\)  
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{split} Safethr(X,s)\equiv_{def}\forall M.SafeMsg(M,s,K)\\ \equiv_{def}\begin{pmatrix}\forall X.\forall e\in E(Send). \forall M.\\ Send(e)=M\wedge loc(e)=X\end{pmatrix}\end{split}  \tag{10}\]  
Let \((e_{1},e_{2},...,e_{l},...,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. \[ \begin{split}\begin{pmatrix}\forall A^{\prime},B^{\prime}:Id. \exists e\in E(New).\exists e^{\prime}\in E(Encrypt).\\ New(e)=n\wedge Encrypt(e^{\prime})=(<...,N_{a},...>,k_{b}^{\prime},s_{1})\\ \wedge loc(e)=loc(e^{\prime})=A^{\prime}\wedge Honest(A^{\prime})\end{pmatrix} \Rightarrow B^{\prime}=B\end{split}  \tag{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,  
Figure 6: SRTP protocol basic sequence. it can be inferred that the identities of both subjects are known. This is expressed by the following formula. \[\forall e\in E(New).New(e)=m\wedge loc(e)=A^{\prime}\Rightarrow Honest(A^{\prime} )\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:  
\[ \begin{pmatrix}\forall X.\exists e_{1},e_{2}:E(Send).\exists S\\ S=Encrypt\big{(}<<n>,k^{\prime}_{s},S_{5}>>\big{)}\wedge New(e_{1})=n\wedge loc (e_{1})=X\Rightarrow\\ Send(e_{2})=S||n\wedge loc(e_{2})=X\end{pmatrix}