# 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.3 Analysis of the Symmetric Ratchet
Similarly, we can also prove that \(e_{3}^{\prime}<e_{7}\), and hence \(SP\vDash auth(I_{3},2)\) is established. Based on the proof of \(SP\vDash auth(I_{3},2)\), we now provide a separate proof for \(SP\vDash auth(R_{3},1)\). Let \(thr_{2}\) be a basic sequence on \(R_{3}\). Define the thread \(thr_{2}\) as having events \(e_{0}<_{loc}e_{1}<_{loc}\cdots<_{loc}e_{4}\). For some _Atom_-type values \(z_{2},s_{3},m_{2},m_{3},rclpk_{2}^{A},rclpk_{3}^{B}\), suppose \(Decrypt(e_{1})=\langle m_{2},rclpk_{2}^{A},s_{2}\rangle\). According to _Axiom_\(D\) and _Axiom_\(S\), there exists an event \(e^{\prime}\) such that \(e^{\prime}<e_{1}\wedge DEMatch(e^{\prime},e_{1})\wedge(loc(e^{\prime})=A\lor loc (e^{\prime})=B)\). Since principal \(B\) follows the honesty axiom and mutual authentication protocol, \(e^{\prime}\) must be a valid instance of a basic sequence. The \(Encrypt()\) action can appear in either \(I_{1}\) or \(I_{2}\). Assuming \(e^{\prime}\in I_{2}\), then for _Atom_-type values \(rclpk_{2}^{A^{\prime}},m_{2}^{\prime},s_{2}^{\prime}\), the following must exist on principal \(A\): \(Encrypt(e^{\prime})=\langle m_{2}^{\prime},rclpk_{2}^{A^{\prime}},s_{2}^{\prime}\rangle\). Thus, from \(DEMatch(e^{\prime},e_{1})\), we obtain \(rclpk_{2}^{A^{\prime}}=rclpk_{2}^{A}\wedge s_{2}^{\prime}=s_{2}\wedge m_{2}^{ \prime}=m_{2}\), which leads to \(Send(e_{1}^{\prime})=\langle s_{2}\rangle\). Hence, \(e^{\prime}\) is an instance from \(I_{2}\), and matches with \(e_{1}\), forming a weakly matching pair \(Send(e_{1}^{\prime})=\langle s_{2}\rangle=Rcv(e_{0})\). Similarly, \(I_{1}\) can be excluded through analogous reasoning. Next, it suffices to confirm the event order \(e_{1}^{\prime}<e_{0}\). Based on axioms such as _Axiom_F, we can reason that if there exists a sending event \(s\) that releases a random number \(m\) between \(e_{1}^{\prime}\) and \(e_{0}\), then if \(e_{1}^{\prime}\leq s\), it follows that \(e_{1}^{\prime}<e_{0}\); if \(e_{0}\leq s\), then there exists \(j\) such that \(e_{0}<_{loc}(j)<e_{1}^{\prime}\). At this point, \(s\) must be on thread \(th_{2}\) of principal \(B\). According to _Axiom_\(F_{1}\), there exists no sending event between \(e_{0}\) and \(e_{1}^{\prime}\), hence random number \(m\) could not have been released before \(e_{1}^{\prime}\). From this reasoning, we conclude \(e_{1}^{\prime}<e_{6}\). Therefore, \(SP\vDash auth(R_{3},1)\) holds. In conclusion, based on the above proof, we arrive at the result that both the asymmetric and symmetric ratchet phases in the _Signal_ protocol satisfy strong mutual authentication properties. This can be written as \(SP\vDash auth(I_{3},2)\wedge auth(R_{3},3)\) and \(SP\vDash auth(I_{3},2)\wedge auth(R_{3},1)\). In addition, we construct a symbolic model of the Signal protocol's ratchet mechanism using the Tamarin prover to verify the strong authentication property between the I3 and R3 stages. The verification result is consistent with our theoretical analysis based on LoET. Further details can be found in B.