# Formal Analysis of DTLS-SRTP Combined Protocol Based on Logic of Events
## 5 Formal Analysis of DTLS-SRTP Combined Protocol
### 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. \(I_{1}=New(m_{1}),Encrypt(<m_{1},PK_{B},S_{1}>),Send(<A,S_{1}>)\)  
\(I_{2}=Rcv(<B,S_{2}>)\)  
\(I_{3}=Decrypt(<<m_{1},m_{2}>,SK_{A},S_{2}>),Encrypt(<<m_{2},S_{2}>,k_{\rm m},S _{3}>),Send(S_{3})\)  
\(R_{1}=Rcv(<A,S_{1}>)\)  
\(R_{2}=Decrypt(<m_{1},SK_{B},S_{1}>),New(m_{2}),Encrypt(<<m_{1},m_{2}>,PK_{A},S _{2}>),Send(<B,S_{2}>)\)  
\(R_{3}=Rcv(S_{3})\)  
Based on the obtained basic sequence, define the DTLS protocol as \(protocol([I_{1},I_{2},I_{3},R_{1},R_{2},R_{3}])\). The strong identity authentication property we need to verify is \(DS\models auth(I_{3},2)\wedge DS\models auth(R_{3},3)\). Starting with the proof of \(DS\models auth(I_{3},2)\), assume honest entities \(A\
eq B\), and that they follow the DTLS protocol. Assume thread thr\({}_{1}\) is an instance of \(I_{3}\), and let \(e_{0}<_{loc}e_{1}<_{loc}e_{2}<_{loc}...<_{loc}e_{6}\) be the actions on thr\({}_{1}\). Then, \(e_{0},...,e_{6}\) all have \(A\) as their principal. For some atoms \(m_{1},m_{2},S_{1},S_{2},S_{3}\)  
\[ \begin{pmatrix}New(e_{0})=m_{1}\wedge Encrypt(e_{1})=<<m_{1},PK_{B},S_{1}>> \wedge Send(e_{2})=S_{1}\wedge\\ Rcv(e_{3})=S_{2}\wedge Decrypt(e_{4})<<m_{1},m_{2}>,SK_{A},S_{2}>\end{pmatrix}  \tag{7}\]  
According to \(Axiom\)S and \(Axiom\)D, there exists an event \(e^{{}^{\prime}}\) such that \(e^{{}^{\prime}}<e_{4}\wedge DEMatch(e_{4}e^{{}^{\prime}})\wedge loc(e^{{}^{ \prime}})=B\) holds. Thus, \(Encrypt(e^{{}^{\prime}})=<<m_{1},m_{2}>,SK_{A},S_{2}>\). Since entity \(B\) follows the DTLS protocol, the event \(e^{{}^{\prime}}\) must be an instance of this protocol's basic sequence. The actions containing \(Encrypt()\) 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^{{}^{\prime}}_{1},m^{{}^{\prime}}_{2},S^{{}^{\prime}}_{2}\) and entity \(C\), there exists an event \(e^{{}^{\prime}}_{0}<_{loc}e^{{}^{\prime}}\); thus, \(New(e^{{}^{\prime}}_{0})=m^{{}^{\prime}}_{1}\wedge Encrypt(e^{{}^{\prime}})= <<m^{{}^{\prime}}_{1},m^{{}^{\prime}}_{2}>,SK_{A},S^{{}^{\prime}}_{2}>\). By  
Figure 4: DTLS protocol basic sequence. the lemma, it follows that \(e_{0}=e_{0}^{{}^{\prime}}\); hence, \(A=loc(e_{0})=loc(e_{0}^{{}^{\prime}})=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}}\) 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:  
\[ \begin{pmatrix}e_{0}^{{}^{\prime}}<_{loc}e_{1}^{{}^{\prime}}<_{loc}e_{2}^{{}^{ \prime}}<_{loc}e_{3}^{{}^{\prime}}=e^{{}^{\prime}}<_{loc}e_{4}^{{}^{\prime}} \wedge Rcv(e_{0}^{{}^{\prime}})=<D,S_{1}^{{}^{\prime}}>\wedge\\ Decrypt(e_{1}^{{}^{\prime}})=<m_{1}^{{}^{\prime\prime}},SK_{B},S_{1}^{{}^{ \prime}}>New(e_{2}^{{}^{\prime}})=m_{2}^{{}^{\prime\prime}}\wedge\\ Encrypt(e_{3}^{{}^{\prime}})=<<m_{1}^{{}^{\prime\prime}},m_{2}^{{}^{\prime \prime}}>,SK_{A},S_{2}^{{}^{\prime\prime}}>\wedge Send(e_{4}^{{}^{\prime}})=S_ {2}^{{}^{\prime\prime}}\end{pmatrix}  \tag{8}\]  
Therefore, the first two messages in the original thread are \(e_{2}\) and \(e_{3}\). It can be determined that \(Send(e_{2})=S_{1}=Rcv(e_{0}^{{}^{\prime}})\) and \(Send(e_{4}^{{}^{\prime}})=S_{2}=Rcv(e_{3})\). 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(e_{0}^{{}^{\prime}})=S_{1}\), then \(e_{0}^{{}^{\prime}}\) possesses \(New(e_{0})\).