# Formal Analysis of Ratchet Protocols Based on Logic of Events
## 2 Logic of Events Theory
### Fundamental Concepts
#### 2.2.3 Axioms of the Logic of Events Theory  
Key Axiom: The Key Axiom (_AxiomK_) is symmetric, the symmetric key corresponds uniquely to the principal that holds it. The key material is unique to each principal; different principals cannot share the same private key. Moreover, the private key held by principal A can only correspond to its own public key, as shown below  
\[\left\{\begin{array}{c}AxiomK:\forall A,B:Id.\forall k,k^{\prime}:Key. \forall a:Atom.\\ \\ MatchingKeys(k,k^{\prime})\Leftrightarrow MatchingKeys(k^{\prime},k) \wedge\\ MatchingKeys(Summ(a),k)\Leftrightarrow k=Summ(a)\wedge\\ MatchingKeys(PriKey(A),k)\Leftrightarrow k=A\wedge\\ MatchingKeys(A,k)\Leftrightarrow k=PriKey(A)\wedge\\ \\ Prikey(A)=Prikey(B)\Leftrightarrow A=B\end{array}\right\} \tag{4}\]  
Honest Axiom: LoET includes the Honest function to assert the honesty of a principal. An honest principal does not disclose its private key during protocol interactions. Furthermore, all encryption, decryption, and signature events are assumed to occur on honest principals. The Honest Axiom (_AxiomS_) characterizes the behavior of trustworthy signers as follows:  
\[\left\{\begin{array}{c}AxiomS:\forall A:Id.\forall s:E(sign).\forall e:E( Encrypt).\forall d:E(Decrypt).\\ \\ Honest(A)\Rightarrow signer(s)=A\Rightarrow(loc(s)=A)\wedge\\ \\ key(e)=PrivateKey(A)\Rightarrow(loc(e)=A)\wedge\\ \\ key(d)=PrivateKey(A)\Rightarrow(loc(d)=A)\end{array}\right\} \tag{5}\]  
Flow Relation Axiom: Flow Relation is a correlation between events in a causal order of a random number. The flow of atom \(a\) from action \(e_{1}\) to action \(e_{2}\) is described \(e_{1}\overset{a}{\rightarrow}e_{2}\), there are three scenarios. The first case is that atom \(a\) from \(e_{1}\) and \(e_{2}\) are located in the same body; the second case is when there are send and receive events, and \(a\) is sent in clear text; in the third case, \(a\) is located in the plaintext of the encryption event and flows with  
\[\begin{cases}\mathit{New}:\mathit{EClass}(\mathit{Atom})\\ \mathit{Send},\mathit{Rcv}:\mathit{EClass}(\mathit{Data})\\ \mathit{Encrypt},\mathit{Decrypt}:\mathit{EClass}(\mathit{Data}\times \mathit{key}\times\mathit{Atom})\\ \mathit{Sign},\mathit{Verify}:\mathit{EClass}(\mathit{Data}\times\mathit{ Id}\times\mathit{Atom})\end{cases} \tag{8}\]  
However, these events do not cover all protocol operations, including those involved in the ratchet encryption mechanism. We extend the event class by introducing new types--\(\mathit{DH}\) and _ratchet_--to more effectively model ratchet encryption. These extensions provide an abstract and precise formal description of ratchet protocols, defined as follows:  
\[\begin{cases}\mathit{DH}:\mathit{EClass}(\mathit{Data}\times\mathit{Key} \times\mathit{Atom})\\ \mathit{Ratchet}:\mathit{EClass}(\mathit{Data}\times\mathit{Key}\times \mathit{Atom})\end{cases} \tag{9}\]  
If there exists an event \(e_{1}\in E(\mathit{DH})\), then the principal \(A\) performs a series of computations within \(e_{1}\) to generate an initial symmetric encryption key for future long-term message sessions. If there exists an event \(e_{2}\in E(\mathit{Ratchet})\), then the principal \(B\) updates the ratchet key to generate a new temporary ratchet key.