## 7 Security Analysis and Cryptographic Guarantees
### Formal Security Proof in the Canetti-Krawczyk Model
The advantage of \(\mathcal{E}\) in this experiment is defined as  
\[\mathrm{Adv}_{\mathcal{E}}^{\Pi^{\prime},\mathrm{AKE}}(k)=\bigg{|}\Pr\Bigl{[} \mathsf{Exp}_{\mathcal{E}}^{\Pi^{\prime},0}(k)=1\Bigr{]}-\frac{1}{2}\bigg{|}.\]  
This experiment reflects the full, unmodified behavior of the protocol as it would occur in an actual deployment, using real cryptographic primitives and without simulation. All deviations introduced in subsequent experiments will be analyzed relative to this baseline. Security Scenario 1: \(\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},1}(k)\)--Replacement of the Hash Function with a Random Oracle  
In this experiment, we transition from the real-world execution model defined in \(\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},0}(k)\) to an idealized setting in which the hash function \(H(\cdot)\) used within the protocol is replaced by a truly random oracle. The objective of this transformation is to simplify the security analysis by abstracting away any structural properties of the hash function and modeling it as a black-box function with ideal behavior. In the original protocol \(\Pi^{\prime}\), the hash function \(H\) is used to compute commitments that bind ephemeral values to long-term identities:  
\[\Gamma_{2}=H(\mathsf{pk}_{\mathcal{A}}\parallel\Gamma_{1}),\qquad\Psi_{2}=H( \mathsf{pk}_{\mathcal{B}}\parallel\Psi_{1}).\]  
In this experiment, \(H\) is modeled as a _random oracle_\(\mathcal{RO}\), which behaves as follows:  
On input \(x\in\{0,1\}^{*}\), if \(x\) has not been queried before, sample \(y\leftarrow\{0,1\}^{\mu}\) uniformly at random and store \((x,y)\) in a global table. If \(x\) was queried previously, return the same \(y\) as before. Here, \(\mu\) denotes the output length of the hash function, typically matching the security parameter (e.g., 256 bits). Both the adversary \(\mathcal{E}\) and the honest parties have access to this oracle \(\mathcal{RO}\), and the responses are consistent across all interactions. The purpose of this transformation is to remove any dependency on the specific implementation or internal structure of \(H\), under the assumption that hash functions used in cryptographic protocols are designed to emulate random oracles. This abstraction is widely accepted in the security analysis of key exchange protocols and digital signatures. Since the only modification in \(\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},1}(k)\) relative to \(\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},0}(k)\) is the treatment of \(H\) as a random oracle, and assuming that \(H\) is collision-resistant and behaves like a pseudo-random function in practice, the difference in \(\mathcal{E}\)'s success probability between these two experiments is negligible:  
\[\left|\Pr\left[\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},1}(k)=1\right]-\Pr \left[\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},0}(k)=1\right]\right|\leq \varepsilon_{\mathrm{hash}}(k),\]  
where \(\varepsilon_{\mathrm{hash}}(k)\) is negligible in \(k\). This is justified by invoking the standard assumption that secure hash functions, such as SHA-256, behave indistinguishably from ideal random oracles in adversarial settings. Therefore, this transition allows us to conduct the remainder of the security analysis under the random oracle model (ROM), which simplifies subsequent reductions while preserving the adversary's effective view of the protocol. Security Scenario 2 \(\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},2}(k)\)--Simulation of Ciphertexts  
In this experiment, the ciphertexts \(\Gamma_{3}\) and \(\Psi_{3}\) are replaced by random bitstrings of identical length. This step relies on the assumption that, under the _random oracle model_, the adversary cannot predict the encrypted values (e.g., \(H(\mathsf{pk}_{A}\parallel\Gamma_{1})\)) unless it queries the oracle on the exact same input. Assuming the adversary does not make such queries, and given that the underlying encryption scheme is IND-CPA secure, we can simulate the ciphertexts without affecting the adversary's distinguishing advantage.