## 7 Security Analysis and Cryptographic Guarantees
### Formal Security Proof in the Canetti-Krawczyk Model
As a result, the adversary's distinguishing advantage is preserved up to a negligible additive factor, and we may proceed to the next experiment without violating the underlying security assumptions. Security Scenario 3: \(\mathsf{Exp}_{\mathcal{E}}^{\Pi^{\prime},3}(k)\)--Session Key Replaced with Random  
In this final experiment, denoted \(\mathsf{Exp}_{\mathcal{E}}^{\Pi^{\prime},3}(k)\), the session key returned by the Test query is replaced with a uniformly random bitstring of the same length as the original key, instead of being computed as  
\[K=[\kappa_{\mathcal{A}}][\kappa_{\mathcal{B}}]\Phi.\]All other interactions and protocol behaviors remain identical to those in \(\text{Exp}_{\mathcal{E}}^{\Pi^{\prime},2}(k)\). The adversary \(\mathcal{E}\) continues to interact with oracles for Send, Reveal, and Corrupt, but it cannot distinguish whether the session key in the challenged session was derived from real protocol values or chosen uniformly at random. This step allows us to assess the _indistinguishability_ of the session key from random. If the adversary succeeds in distinguishing the real key from a random one, it implies that it has learned some non-trivial function of both ephemeral scalars \(\kappa_{\mathcal{A}}\) and \(\kappa_{\mathcal{B}}\) or has broken the underlying cryptographic assumptions. Formally, we define the adversary's advantage in this experiment as  
\[\text{Adv}_{\mathcal{E}}^{\Pi^{\prime},\text{AKE}}(k)=\bigg{|}\Pr\Bigl{[} \text{Exp}_{\mathcal{E}}^{\Pi^{\prime},3}(k)=1\Bigr{]}-\frac{1}{2}\bigg{|}.\]  
Under the assumption that the Elliptic Curve Discrete Logarithm Problem (ECDLP) is intractable and that the scalars \(\kappa_{\mathcal{A}}\) and \(\kappa_{\mathcal{B}}\) are independently and uniformly chosen for each session and never revealed, we argue that  
\[\text{Adv}_{\mathcal{E}}^{\Pi^{\prime},\text{AKE}}(k)\leq\varepsilon(k),\]  
where \(\varepsilon(k)\) is a negligible function in the security parameter \(k\). This completes the sequence of experiments used in our proof. By bounding the adversary's distinguishing advantage in each transition, we conclude that the refined protocol \(\Pi^{\prime}\) achieves authenticated key exchange (AKE) security in the Canetti-Krawczyk model. Reduction. Assume there exists a probabilistic polynomial-time adversary \(\mathcal{E}\) that can distinguish the output of experiment \(\text{Exp}_{\mathcal{E}}^{\Pi^{\prime},3}(k)\) from a random bit with non-negligible advantage. Then, by the sequence-of-experiments technique, we show that this implies the existence of a reduction that violates one of the underlying security assumptions of the protocol. We consider each transition between adjacent experiments:  
* Transition from \(\text{Exp}_{\mathcal{E}}^{\Pi^{\prime},0}(k)\) to \(\text{Exp}_{\mathcal{E}}^{\Pi^{\prime},1}(k)\) replaces the hash function \(H(\cdot)\) with a random oracle. An adversary capable of distinguishing this transformation contradicts the assumption that \(H\) behaves as an ideal random oracle. Let the distinguishing advantage be denoted \(\varepsilon_{\text{hash}}(k)\). * Transition from \(\text{Exp}_{\mathcal{E}}^{\Pi^{\prime},1}(k)\) to \(\text{Exp}_{\mathcal{E}}^{\Pi^{\prime},2}(k)\) replaces ciphertexts \(\Gamma_{3}\) and \(\Psi_{3}\) with random values. An adversary who detects this change can be used to build an IND-CPA distinguisher for the encryption scheme Enc. Let the corresponding advantage be \(\varepsilon_{\text{enc}}(k)\). * Transition from \(\text{Exp}_{\mathcal{E}}^{\Pi^{\prime},2}(k)\) to \(\text{Exp}_{\mathcal{E}}^{\Pi^{\prime},3}(k)\) replaces the real session key with a uniformly random key. Any non-negligible distinguishing advantage in this step implies that the adversary has obtained information about \([\kappa_{\mathcal{A}}][\kappa_{\mathcal{B}}]\Phi\) from \(\Gamma_{1}\) and \(\Psi_{1}\) without knowledge of the ephemeral scalars, violating the hardness of the ECDLP. Let this advantage be denoted \(\varepsilon_{\text{ecdlp}}(k)\).