## 5 Security Analysis
### Formal Validation  
In the literature researchers have suggested various mechanisms for the validation of security protocols. To formalize security protocols, a mathematical model is necessary, and an active adversary must be capable of calculating its own messages and broadcasting them to the network, impersonating honest participants. For that, many protocol verifiers rely on the symbolic model of cryptography, commonly known as the \"Dolev-Yao model\". The formal validation of our protocol is conducted using the ProVerif tool to establish the non-violation of required security properties: particularly, confidentiality, authentication, delivery proof, and replay protection. For clarity, we present our modeling using a high-level Alice and Bob notation. Additionally, we employ the default Dolev-Yao intruder model, enabling the simulation of an intruder with complete control over the network. The messages sent and received by different entities may be intercepted, analyzed, modified (to the extent of known keys), or sent to other entities for comprehensive evaluation. Therefore, to prevent a man-in-the-middle attack, [PERSON] must confirm that the public key she obtained belongs to the intended communication partner. Verification of [PERSON]'s signed key is essential for this purpose. Subsequently, the HKDF technique is employed to implement the symmetric ratchet, ensuring that the output is cryptographically secure. In the first phase, a secret key and some input data--possibly, a constant--are transmitted to the KDF function. The output of the KDF function is another concealed key.  
In the subsequent step, this new key separates the next KDF key and the encryption key into two distinct components. This marks the turning of the \"ratchet\": a new encryption key is generated while the internal state of the ratchet (the KDF key) is modified. Given the output key, reconstructing the input key of the KDF method is challenging since the algorithm is assume to be cryptographically secure. This means that even if the current state and encryption key are compromised, an attacker cannot recreate older keys. However, they can use the encryption key to decipher a single communication. Additionally, we ensure break-in recovery by varying the input value at each step: if the attacker does not know the input, they cannot infer the ratchet's subsequent state from merely knowing the present one. Therefore in a session, [PERSON] and [PERSON] ensure confidentiality, integrity, authentication, and forward secrecy.  
Furthermore, we conduct a test case ([[https://github.com/[PERSON]/Proverif-Key-Trust-Protocol-](https://github.com/[PERSON]/Proverif-Key-Trust-Protocol-)]([https://github.com/[PERSON]/Proverif-Key-Trust-Protocol-](https://github.com/[PERSON]/Proverif-Key-Trust-Protocol-)), accessed on 13 February 2023) as illustrated in Figure 5. This test case confirms that [PERSON] can successfully send the key used to encrypt [PERSON]'s name to [PERSON]. This indicates that an attacker cannot obtain the key entrusted to [PERSON]. Moreover, a test case is used to test whether an intruder can attack an encrypted contact name in the database. We assume that an attacker grants himself full access to an offline device. The test case passes, indicating that [PERSON]'s name is safe from an attacker who has access to it, as shown in Figure 6. This is guaranteed because the key is stored in [PERSON]'s device.