# 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  
As Figure 4 shows, unlike the asymmetric ratchet phase, in the symmetric ratchet phase, after principal \(A\) sends the encryption key and message to \(B\), if \(B\) has not received the message or does not respond to \(A\) in time upon receiving it, \(A\) can continue sending new keys and messages until a response is received from \(B\). Once \(B\) responds to \(A\), both parties resume normal communication, alternating between ratchet and non-ratchet steps. Therefore, it is sufficient to prove that the symmetric ratchet phase satisfies the strong authentication properties. According to the description in Section 2, the strong authentication properties that need to be verified in the symmetric ratchet phase of the Signal protocol are \(SP\models auth(I_{3},2)\wedge SP\models auth(R_{3},1)\). In the asymmetric ratchet phase, assume that honest principals \(A\
eq B\), and both parties follow the honest principal rule (Equation (5)). According to the definition of the basic sequence, each thread of \(A\) and \(B\) is an instance of a basic sequence. Let \(thr_{1}\) be an instance on \(I_{3}\) and define \(e_{0}<_{loc}e_{1}<_{loc}\dots<_{loc}e_{8}\), where the following events exist:  
\[\left\{ \begin{array}{l}New(e_{0})=\langle PKB-B\rangle\wedge DH(e_{1})= \langle rclpk_{1}^{A}\rangle\wedge\\ \text{\emph{Encrypt}}(e_{2})=\langle m_{1},rchpk_{1}^{A},s_{1}\rangle\wedge\\ \text{\emph{Send}}(e_{3})=\langle s_{1}\rangle\wedge DH(e_{4})=\langle rclpk_ {2}^{A}\rangle\wedge\\ \text{\emph{Decrypt}}(e_{5})=\langle m_{2},rchpk_{2}^{A},s_{2}\rangle\wedge\\ \text{\emph{Send}}(e_{6})=\langle s_{2}\rangle\wedge Rcv(e_{7})=\langle s_{ 3}\rangle\\ \text{\emph{Encrypt}}(e_{8})=\langle m_{3},\langle rclpk_{2}^{A},rchpk_{3}^{ B}\rangle,s_{3}\rangle\end{array} \right\} \tag{23}\]  
According to _Axiom D_ (Equation (10)) and _Axiom S_ (Equation (5)), there exists some event \(e^{\prime}\) such that \(e^{\prime}<e_{8}\wedge\text{\emph{DEMatch}}(e^{\prime},e_{8})\wedge(loc(e^{ \prime})=A\lor loc(e^{\prime})=B)\). In the basic sequence, the _Encrypt()_ action may appear in \(I_{1}\), \(I_{2}\), \(or\)\(R_{3}\). To ensure the availability of event occurrences, the event types involving initiator \(A\) and responder \(B\) must involve both or multiple parties. Therefore, \(I_{1}\) and \(I_{2}\) can be excluded. Assuming \(e^{\prime}\) is an instance from \(R_{3}\), then for _Atom_-type values \(s_{2}^{\prime},s_{3}^{\prime},m_{2}^{\prime},m_{3}^{\prime},rclpk_{2}^{A},rclpk_ {3}^{B}\), there exist events \(e_{0}^{\prime},e_{1}^{\prime},e_{2}^{\prime},e^{\prime},e_{3}^{\prime}\) on principal \(B\). \[\left\{ \begin{array}{l}e_{0}^{\prime}<_{loc}e_{1}^{\prime}<_{loc}e_{2}^{ \prime}<_{loc}e^{\prime}<_{loc}e_{3}^{\prime}\\ \text{\emph{Rcv}}(e_{0}^{\prime})=\langle s_{2}^{\prime}\rangle\wedge\text{ \emph{Decrypt}}(e_{1}^{\prime})=\langle m_{2}^{\prime},rclpk_{3}^{A^{\prime}}, s_{2}^{\prime}\rangle\wedge\\ \text{\emph{Ratchet}}(e_{2}^{\prime})=\langle rchpk_{2}^{A^{\prime}},rchpk_{3}^{ B^{\prime}}\rangle\wedge\\ \text{\emph{Encrypt}}(e^{\prime})=\langle m_{3}^{\prime}\langle rchpk_{2}^{A^{ \prime}},rclpk_{3}^{B^{\prime}}\rangle s_{3}^{\prime}\rangle\wedge\\ \text{\emph{Send}}(e_{3}^{\prime})=\langle s_{3}^{\prime}\rangle\end{array}  \right\} \tag{24}\]  
(Equations (12)-(15)), if a sending event \(s\) that releases a random number \(m\) exists between \(e_{1}^{\prime\prime}\) and \(e_{0}^{\prime}\), then if \(e_{1}^{\prime\prime}\leq s\), it follows that \(e_{1}^{\prime\prime}<e_{0}^{\prime}\); if \(e_{0}^{\prime}\leq s\), then \(e_{0}^{\prime}<_{loc}(j)<e_{1}^{\prime\prime}\). In this case, \(s\) must be on thread \(th_{1}\) of principal \(B\), and based on _Axiom_\(F_{1}\), since there is no sending event between \(e_{1}^{\prime\prime}\) and \(e_{0}^{\prime}\), the random number \(m\) could not have been released before \(e_{1}^{\prime\prime}\). Therefore, we conclude that \(e_{1}^{\prime\prime}<e_{0}^{\prime}\).