# Formal Analysis of Ratchet Protocols Based on Logic of Events
## 3 Formal Analysis of the Signal Protocol
### Formal Verification of Strong Authentication Properties
#### 3.3.2 Analysis of the Asymmetric Ratchet
\begin{array}{l}\mathit{Plaintext}(e^{\prime})=\mathit{Plaintext}(e _{5})\wedge\\ \mathit{ciphertext}(e^{\prime})=\mathit{ciphertext}(e_{5})\wedge\\ \mathit{MatchingKey}(\mathit{key}(e^{\prime}),\mathit{key}(e_{5}))\quad \Rightarrow\\ \mathit{rcbrk}_{1}^{A^{\prime}}=\mathit{rcbrk}_{1}^{A}\wedge\mathit{rcbrk}_{2 }^{B^{\prime}}=\mathit{rcbrk}_{2}^{B}\wedge\\ \mathit{s}_{2}^{\prime}=s_{2}\wedge m_{2}^{\prime}=m_{2}\end{array} \right\} \tag{18}\]  
From the Equations (16)-(18), it can be derived that  
\[\left\{ \begin{array}{l}e_{0}^{\prime}<_{loc}e_{1}^{\prime}<_{loc}e_{2}^{ \prime}<_{loc}e_{2}^{\prime}<_{loc}e_{4}^{\prime}\\ Rcv(e_{0}^{\prime})=\langle s_{1}\rangle\wedge\\ \mathit{New}(e_{1}^{\prime})=\langle\mathit{PKB}-A\rangle\wedge\\ \mathit{Decrypt}(e_{2}^{\prime})=\langle m_{1},\mathit{rcbrk}_{1}^{A}\rangle \wedge\\ \mathit{Ratchet}(e_{3}^{\prime})=\langle\mathit{rcbrk}_{1}^{A},\mathit{ rcbrk}_{2}^{B}\rangle\wedge\\ \mathit{Encrypt}(e^{\prime})=\langle m_{2},\langle\mathit{rcbrk}_{1}^{A}, \mathit{rcbrk}_{2}^{B}\rangle,s_{2}\rangle\wedge\\ \mathit{Send}(e_{4}^{\prime})=\langle s_{2}\rangle\end{array} \right\} \tag{19}\]  
The Equation (19) shows that \(e^{\prime}\) is an instance of \(R_{2}\). At this point, \(e^{\prime}\) matches \(e_{5}\), so it can be excluded from \(I_{1}\). Similarly, analyzing the \(\mathit{Decrypt}()\) event in \(R_{2}\), it must exist in an event \(e^{\prime\prime}\), such that \(e^{\prime\prime}\in\mathit{DEMatch}(e^{\prime\prime},e_{2})\wedge\mathit{ loc}(e^{\prime\prime})=A\vee\mathit{loc}(e^{\prime\prime})=B\), thus making \(\mathit{Encrypt}(e^{\prime\prime})=\langle m_{1},\mathit{rclnpk}_{1}^{A},s_{1}\rangle\). Assuming that \(e^{\prime\prime}\) is an instance on \(I_{1}\), for the \(\mathit{Atom}\) type of \(\mathit{PKB}\)-\(\mathit{B},\mathit{rclnpk}_{1}^{A},m_{1},s_{1}\), the event on the main body \(A\) would be as follows:  
\[\left\{ \begin{array}{l}e_{0}^{\prime\prime}<_{\mathit{loc}}e_{1}^{\prime \prime}<_{\mathit{loc}}e^{\prime\prime}<_{\mathit{loc}}e_{2}^{\prime\prime}\\ \mathit{New}(e_{0}^{\prime\prime})=\langle\mathit{PKB}-B^{\prime\prime} \rangle\wedge\\ \mathit{DH}(e_{1}^{\prime\prime})=\langle\mathit{rclnpk}_{1}^{A^{\prime \prime}}\rangle\wedge\\ \mathit{Encrypt}(e^{\prime\prime})=\langle m_{1}^{\prime\prime},\mathit{rclnpk }_{1}^{A^{\prime\prime}},s_{1}^{\prime\prime}\rangle\wedge\\ \mathit{Send}(e_{2}^{\prime\prime})=\langle s_{1}^{\prime\prime}\rangle\end{array} \right\} \tag{20}\]  
\(\mathit{DEMatch}(e^{\prime\prime},e_{2}^{\prime})\) holds by \(\mathit{AxiomD}\) (Equation (10)) and \(\mathit{AxiomE}\) (Equation (11))  
\[\left\{ \begin{array}{l}\mathit{Plaintext}(e^{\prime\prime})=\mathit{Plaintext }(e_{2}^{\prime})\wedge\\ \mathit{ciphertext}(e^{\prime\prime})=\mathit{ciphertext}(e_{2}^{\prime}) \wedge\\ \mathit{MatchingKeys}(key(e^{\prime\prime}),key(e_{2}^{\prime}))\quad \Rightarrow\\ \mathit{rclnpk}_{1}^{A^{\prime\prime}}=\mathit{rclnpk}_{1}^{A}\wedge s_{1}^{ \prime\prime}=s_{1}\wedge m_{1}^{\prime\prime}=m_{1}\end{array} \right\} \tag{21}\]  
From the Equations (19)-(21), it can be derived that  
\[\left\{ \begin{array}{l}\mathit{New}(e_{0}^{\prime\prime})=\langle\mathit{ PKB}-\mathit{B}\rangle\wedge\\ \mathit{DH}(e_{1}^{\prime\prime})=\langle\mathit{rclnpk}_{1}^{A}\rangle\wedge \\ \mathit{Encrypt}(e^{\prime\prime})=\langle m_{1},\mathit{rclnpk}_{1}^{A},s_{1} \rangle\wedge\\ \mathit{Send}(e_{2}^{\prime\prime})=\langle s_{1}\rangle\end{array} \right\} \tag{22}\]  
The Equation (22) shows that \(e^{\prime\prime}\) is an instance on \(I_{1}\), and it matches \(e_{2}^{\prime}\). From the above proof, we can deduce that \(\mathit{Send}(e_{3})=\mathit{Rcv}(e_{4})\) and \(\mathit{Send}(e_{4}^{\prime})=\mathit{Rcv}(e_{4})\), which forms two weak matching pairs, \(\mathit{Send},\mathit{Rcv}\). Next, we need to confirm the event order, \(e_{3}<e_{0}\) and \(e_{4}^{\prime}<e_{4}\), to prove the strong matching property. From the extension of \(\mathit{AxiomF}\) (Equation (7)) and the _has_ rule (Equations (12)-(15)).