# 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  
As Figure 1 shows, in the asymmetric ratchet phase, after obtaining [PERSON]'s prekey bundle, [PERSON] sends the generated keys and messages to B. Upon receiving the message, [PERSON] responds to [PERSON]. The two parties then repeat this process to communicate. According to the description in Section 2, in the asymmetric ratchet phase of the _Signal_ protocol, the strong authentication property to be verified is given by \(SP\models auth(I_{3},2)\wedge SP\models auth(R_{3},3)\). As Figure 3 shows, we assume that the honest principals \(A\
eq B\) both behave according to the honest principle (Equation (5)). According to the definition of the basic sequence, each thread of \(A\) and \(B\) is an instance of the basic sequence. Let \(thr_{1}\) be an instance on \(I_{3}\), and for \(Atom\)-typed parameters \(PKB\)-\(B\), \(rchpk_{1}^{A}\), \(rchpk_{2}^{B}\), \(Rclhpk_{3}^{A}\), \(m_{1}\), \(m_{2}\), \(m_{3}\), \(s_{1}\), \(s_{2}\), \(s_{3}\), there exists an event sequence \(e_{0}<_{\text{loc}}e_{1}<_{\text{loc}}\cdots<_{\text{loc}}e_{8}\), and the event instance of \(thr_{1}\) is as follows:  
Figure 4: Basic sequence of the symmetric ratchet phase. \[\left\{ \begin{array}{l}\mathit{New}(e_{0})=\langle\mathit{PKB}-B\rangle\wedge\\ DH(e_{1})=\langle\mathit{rcbrk}_{1}^{A}\rangle\wedge\\ \mathit{Encrypt}(e_{2})=\langle m_{1},\mathit{rcbrk}_{1}^{A},s_{1}\rangle \wedge\\ \mathit{Send}(e_{3})=\langle s_{1}\rangle\wedge\\ \mathit{Rcv}(e_{4})=\langle s_{2}\rangle\wedge\\ \mathit{Decrypt}(e_{5})=\langle m_{2},\langle\mathit{rcbrk}_{1}^{A},\mathit{ rcbrk}_{2}^{B}\rangle,S_{2}\rangle\wedge\\ DH(e_{6})=\langle\mathit{rcbrk}_{2}^{B},\mathit{rcbrk}_{3}^{A}\rangle \wedge\\ \mathit{Encrypt}(e_{7})=\langle m_{3},\langle\mathit{rcbrk}_{2}^{B},\mathit{ rcbrk}_{3}^{A}\rangle,s_{3}\rangle\wedge\\ \mathit{Send}(e_{8})=\langle s_{3}\rangle\end{array} \right\} \tag{16}\]  
According to \(\mathit{AxiomD}\) (Equation (10)) and \(\mathit{Axioms}\) (Equation (5)), there exists an event \(e^{\prime}\) such that \(e^{\prime}<e_{5}\wedge\mathit{DEMatch}(e^{\prime},e_{5})\wedge\mathit{loc}(e^ {\prime})=A\lor\mathit{loc}(e^{\prime})=B\). In the basic sequence, actions containing \(\mathit{Encrypt}\) are included in \(I_{1},I_{3},R_{2}\). Since it is based on the current event, all future events are not considered, thus \(I_{3}\) is excluded. This implies that in \(I_{1}\) or \(R_{2}\), there exists a basic sequence that could potentially match with \(I_{3}\). Assume \(e^{\prime}\) is an instance in \(R_{2}\), then for \(\mathit{Atom}\)-typed values \(\mathit{PKB}\)-\(A^{\prime}\), \(\mathit{rcbrk}_{1}^{A^{\prime}}\), \(\mathit{rcbrk}_{2}^{B^{\prime}}\), \(m_{1}^{\prime},m_{2}^{\prime},s_{2}^{\prime}\), there exists a sequence of events \(e_{0}^{\prime},e_{1}^{\prime},e_{2}^{\prime},e_{3}^{\prime},e_{4}^{\prime}\) on principal \(B\) as follows:  
\[\left\{ \begin{array}{l}e_{0}^{\prime}<_{loc}e_{1}^{\prime}<_{loc}e_{2}^{ \prime}<_{loc}e_{3}^{\prime}<_{loc}e_{4}^{\prime}\\ Rcv(e_{0}^{\prime})=\langle s_{1}^{\prime}\rangle\wedge\mathit{New}(e_{1}^{ \prime})=\langle\mathit{PKB}-A^{\prime}\rangle\wedge\\ \mathit{Decrypt}(e_{2}^{\prime})=\langle m^{\prime},\mathit{rcbrk}_{1}^{A^{ \prime}},s_{1}^{\prime}\rangle\wedge\mathit{Ratchet}(e_{3}^{\prime})=\langle \mathit{rcbrk}_{1}^{A^{\prime}},\mathit{rcbrk}_{2}^{B^{\prime}}\rangle\wedge\\ \mathit{Encrypt}(e^{\prime})=\langle m^{\prime},\langle\mathit{rcbrk}_{1}^{A^ {\prime}},\mathit{rcbrk}_{2}^{B^{\prime}}\rangle,s_{2}^{\prime}\rangle \wedge\mathit{Send}(e_{4}^{\prime})=\langle s_{2}^{\prime}\rangle\end{array} \right\} \tag{17}\]  
\(\mathit{DEMatch}(e^{\prime},e_{5})\) holds by \(\mathit{AxiomD}\) (Equation (10)) and \(\mathit{AxiomE}\) (Equation (11))  
\[\left\{