# 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.1 Formal Description of Basic Sequences  
In the Signal protocol, apart from the registration phase--during which A and B register their identities and public keys with the server and request each other's pre-key bundles--the server does not participate in the conversation. Therefore, we focus only on the interaction between the two communicating parties. The asymmetric and symmetric ratchet phases of the Signal protocol are described using basic sequences. We define _Initiator A_ and _Responder B_ to represent both parties in the interaction. Specifically, \(I_{1}\), \(I_{2}\), \(I_{3}\) are the basic sequences of _Initiator A_, while \(R_{1},R_{2},R_{3}\) are the basic sequences of _Responder B_, as illustrated in Figures 3 and 4. The notations is explained in Table 2.  
Figure 3 illustrates the formalized basic event sequences \(I_{1}\), \(I_{2}\), and \(I_{3}\) of the initiator A during the asymmetric ratchet phase of the Signal protocol. Each sequence represents a distinct round in the message exchange:  
* \(\mathbf{I_{1}}\) captures the initial message transmission from [PERSON] to B, where [PERSON] uses Diffie-Hellman (DH) to generate an ephemeral key and encrypts the message;
* \(\mathbf{I_{2}}\) models the reception of [PERSON]'s response, including decryption using [PERSON]'s previous key and updating [PERSON]'s ratchet key for forward secrecy;
* \(\mathbf{I_{3}}\) reflects [PERSON]'s subsequent message to [PERSON], built upon the updated ratchet state.  
These sequences collectively represent the progression of ratcheted state transitions at the initiator's side, and form the basis for verifying the strong authentication property \(SP\models auth(I_{3},2)\).  
Figure 4 illustrates the formalized basic event sequences \(R_{1}\), \(R_{2}\), and \(R_{3}\) of the responder B during the symmetric ratchet phase of the Signal protocol. Each sequence models a message processing step by B after receiving messages from A:  
\begin{table}
\begin{tabular}{c c} \hline \hline
**Notations** & **Description** \\ \hline \(PKB\)-\(X\) & Prekey bundle of \(X\) \\ \(rcl\mathbf{p}k_{x}^{y}\) & The \(x\)-th ratchet key generated by party \(y\) \\ \(m_{x}\) & The \(x\)-th ciphertext of the sender \\ \(s_{x}\) & The \(x\)-th message \\ \hline \hline \end{tabular}
\end{table}
Table 2: Notation descriptions.  
Figure 3: Basic sequence of the asymmetric ratchet phase.  
* \(\mathbf{R_{1}}\) depicts the initial decryption of the received ciphertext from A using the ratcheted key, enabling B to retrieve the plaintext message;
* \(\mathbf{R_{2}}\) represents the generation of a new ratchet key by B and the encryption of a response message to A, establishing a new ratcheted state;
* \(\mathbf{R_{3}}\) shows the reception and decryption of a subsequent message from A using the updated ratchet key.  
These sequences collectively capture the symmetric ratcheting process on the responder's side, where key updates are driven by key derivation functions (KDFs) rather than new Diffie-Hellman exchanges. They form the basis for verifying the strong authentication property \(SP\models auth(R_{3},1)\).  
Whether in the asymmetric or symmetric ratchet interaction phase, if the _Signal_ protocol can ensure that two threads at different states establish a strongly matching session, then it satisfies the properties of strong authentication. Therefore, we define the _Signal_ authentication protocol as \(Protocol(I_{1},I_{2},I_{3},R_{1},R_{2},R_{3})\), abbreviated as \(SP\). Next, we analyze the dual ratchet processes separately.