# 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
It is known that there exists a sending event \(s\) between \(e_{3}\) and \(e_{0}^{\prime}\) that releases a random number \(m\). If \(e_{3}\leq s\), we can obtain \(e_{3}<e_{0}^{\prime}\). otherwise, If \(e_{0}^{\prime}\leq s\), then must exist \(e_{0}^{\prime}<\mathit{loc}(j)<e_{3}\). In this case, \(s\) must be the result of a process on the main thread \(th_{1}\) of \(B\). According to \(\mathit{AxiomF}\) (Equation (7)), it is known that \(e_{3}\) and \(e_{0}\) do not exist in the sending event, which implies that the random number \(m\) will not be released before \(e_{3}\). Therefore, we can conclude that \(e_{3}<e_{0}^{\prime}\), and similarly, it can be proven that \(e_{4}<e_{4}^{\prime}\). Thus, \(\mathit{SP}\models\)\(\mathit{auth}1(l_{3},2)\) is established. Similarly, it can be verified that \(\mathit{SP}=\mathit{auth}(l_{3},2)\). Let \(\mathit{thr}_{2}\) be a basic sequence on \(R_{3}\). Define a sequence of events on thread \(\mathit{thr}_{2}\) as \(e_{0}<_{\mathit{loc}}e_{1}<_{\mathit{loc}}\cdots<_{\mathit{loc}}e_{7}\). For some information of type \(\mathit{Atom}\), including \(s_{1},s_{2},s_{3},m_{1},m_{2},m_{3},\mathit{rclnpk}_{1}^{A},\mathit{rclnpk}_{2 }^{B},\mathit{rclnpk}_{3}^{A}\), we have \(\mathit{Decrypt}(e_{7})=\langle m_{3},\langle\mathit{rclnpk}_{2}^{B},\mathit{rclnpk }_{3}^{A}\rangle,s_{3}\rangle\). According to \(\mathit{AxiomD}\) and \(\mathit{AxiomS}\), there exists some event \(e^{\prime}\) such that \(e^{\prime}<e_{7}\wedge\mathit{DEMatch}(e^{\prime},e_{7})\wedge(\mathit{loc}(e ^{\prime})=A\lor\mathit{loc}(e^{\prime})=B)\). Since principal \(B\) follows the honesty axiom and mutual authentication protocol, \(e^{\prime}\) must be a valid instance in the basic sequence, which includes \(\mathit{Encrypt}(e)\) events from \(I_{3}\), \(I_{1}\), \(R_{2}\). Assume that \(e^{\prime}\) is one such instance from \(I_{3}\); then for \(\mathit{Atom}\)-type data \(\mathit{rclnpk}_{1}^{A},\mathit{rclnpk}_{2}^{B},\mathit{rclnpk}_{3}^{A},m_{2}^{ \prime},m_{3}^{\prime},s_{2}^{\prime},s_{3}\), the following events exist in principal: \(A\): \(e_{0},e_{1},e_{2},e^{\prime},e_{3}\), and we have \(\mathit{Encrypt}(e^{\prime})=\langle m_{3}^{\prime},\langle\mathit{rclnpk}_{2}^{B },\mathit{rclnpk}_{3}^{A}\rangle,s_{3}^{\prime}\rangle\). Therefore, \(\mathrm{DEMatch}(e^{\prime},e_{7})\) holds. According to \(\mathit{AxiomD}\) and \(\mathit{AxiomE}\), we know that there exists an event \(e^{\prime}\) in \(I_{3}\) such that \(\mathit{Send}(e_{3}^{\prime})=s_{3}=\mathit{Rcv}(e_{6})\), forming a weakly matching pair. Similarly, \(I_{1}\) and \(R_{2}\) can be excluded. Since it has been proven that \(e^{\prime}\) is an event from \(I_{3}\), there must exist another event \(e^{\prime\prime}\) such that \(e^{\prime\prime}<e_{1}^{\prime}\wedge\mathit{DEMatch}(e^{\prime\prime},e_{1}^{ \prime})\wedge(\mathit{loc}(e^{\prime\prime})=A\lor\mathit{loc}(e^{\prime\prime})=B)\). The proof process can reference \(\mathit{auth}(I_{3},2)\). We then have \(s_{2}=Send(e_{5})\). Likewise, it can be derived that \(e^{\prime\prime\prime}<e_{2}\wedge\text{DEMatch}(e^{\prime\prime\prime},e_{2}) \wedge(\text{loc}(e^{\prime\prime\prime})=A\vee\text{loc}(e^{\prime\prime \prime})=B)\), which yields \(send(e_{3})=rcv(e_{0}^{\prime})\). This completes the proof of three weakly matching pairs. Next, we need to prove that \(e_{3}^{\prime}<e_{6}\), \(e_{5}<e_{0}^{\prime}\), \(e_{3}<e_{0}^{\prime}\), thereby completing the proof of strong authentication. According to extension of _Axiom F_ and the _has_ rule, we can deduce as follows: Suppose a sending event \(s\) releases random number \(m\) and occurs between \(e_{3}\) and \(e_{6}\). If \(e_{3}\leq s\), we get \(e_{3}<e_{6}\). Otherwise, if \(e_{6}\leq s\), then \(e_{6}<loc(j)<e_{3}^{\prime}\). In this case, \(s\) must be a member on thread \(th_{2}\) of principal \(B\). According to _Axiom F_, we know that \(e_{6}\) and \(e_{3}\) are not part of the send event, \(m\) will not be released before \(e_{3}\). Therefore, we conclude that \(e_{3}<e_{6}\).