## 7 Security Analysis and Cryptographic Guarantees
### Formal Security Proof in the Canetti-Krawczyk Model
Combining these steps yields the following bound on the total advantage of the adversary in the real experiment:  
**Lemma 1** (Sequence-of-Experiments Conclusion). : _Let \(\Pi^{\prime}\) be the refined authenticated key agreement protocol, and let \(\mathcal{E}\) be any PPT adversary in the \(CK\) model. Then, under the assumptions of IND-CPA security of Enc, the random oracle behavior of \(H\), and the hardness of the ECDLP, the advantage of \(\mathcal{E}\) in breaking the AKE security of \(\Pi^{\prime}\) satisfies:_  
\[\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{|}.\]0_where each \(\varepsilon(\cdot)\) is a negligible function in the security parameter \(k\)._  
Proof. : Let us denote by \(\mathcal{E}\) a probabilistic polynomial-time adversary that interacts with protocol \(\Pi^{\prime}\) in the authenticated key exchange (AKE) experiment under the Canetti-Krawczyk model. We consider the sequence of experiments:  
\[\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{|}.\]1  
We define the advantage of \(\mathcal{E}\) in the real experiment 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{|}.\]2  
To bound this advantage, we apply the triangle inequality over the sequence of experiments:  
\[\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{|}.\]3 \[\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{|}.\]4 \[\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{|}.\]5 \[\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{|}.\]6 \[\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{|}.\]7  
Each of these differences is bounded by the security assumption related to the respective experiment:  
* \(\big{|}\Pr[\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},0}=1]-\Pr[\mathrm{Exp}_{ \mathcal{E}}^{\Pi^{\prime},1}=1]\big{|}\leq\varepsilon_{\mathrm{hash}}(k)\), due to the random oracle assumption on \(H\);
* \(\big{|}\Pr[\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},1}=1]-\Pr[\mathrm{Exp}_{ \mathcal{E}}^{\Pi^{\prime},2}=1]\big{|}\leq\varepsilon_{\mathrm{enc}}(k)\), from the IND-CPA security of Enc;
* \(\big{|}\Pr[\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},2}=1]-\Pr[\mathrm{Exp}_{ \mathcal{E}}^{\Pi^{\prime},3}=1]\big{|}\leq\varepsilon_{\mathrm{ecdplp}}(k)\), by the hardness of the ECDLP;
* \(\big{|}\Pr[\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},3}=1]-\tfrac{1}{2}\Big{|}\) remains as is, by definition. By substituting these bounds, we obtain \[\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{|}.\]8 But by construction of experiment \(\mathrm{Exp}_{\mathcal{E}}^{\Pi^{\prime},3}(k)\), where the session key is replaced with a uniformly random string, it follows that \[\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{|}.\]9 Therefore, this concludes as \[\Gamma_{2}=H(\mathsf{pk}_{\mathcal{A}}\parallel\Gamma_{1}),\qquad\Psi_{2}=H( \mathsf{pk}_{\mathcal{B}}\parallel\Psi_{1}).\]0 as claimed. Therefore, the existence of a non-negligible advantage \(\mathrm{Adv}_{\mathcal{E}}^{\Pi^{\prime},\mathrm{AKE}}(k)\) would imply a violation of at least one of the underlying cryptographic assumptions, contradictingtheir presumed hardness.