## 7 Security Analysis and Cryptographic Guarantees
### Formal Security Proof in the Canetti-Krawczyk Model
We acknowledge that IND-CPA security does not directly imply ciphertext pseudorandomness. However, for hash-derived values unknown to the adversary, this simulation is sound under standard assumptions. A more conservative approach would involve using an encryption scheme with _pseudorandom ciphertexts_ (IND-PRIV), or alternatively modeling the encryption function in the random oracle model as well. These considerations are left as possible refinements in future work. The purpose of replacing the ciphertexts with random bitstrings in this experiment is to simulate their behavior under the assumption that the adversary does not know the underlying plaintexts, which are hash values of inputs derived only by honest parties. If the adversary has not queried the random oracle with the exact inputs, then from its perspective, the ciphertexts reveal no additional information and can be replaced with random strings. This technique allows us to isolate the ciphertext's contribution to the adversary's advantage and supports the reduction to IND-CPA security. While the encryption is used for authentication, not confidentiality, this transformation ensures that the simulation remains indistinguishable under standard cryptographic assumptions. With respect to the above, the transition is made from the idealized random oracle environment of \(\mathsf{Exp}_{\mathcal{E}}^{\Pi^{\prime},1}(k)\) to a setting where the ciphertexts exchanged during the protocol execution are no longer computed via the actual encryption function \(\mathsf{Enc}_{\mathsf{sk}}(\cdot)\), but are instead simulated using uniformly random values. The purpose of this step is to isolate the impact of ciphertext content on the adversary's distinguishing advantage. In the refined protocol \(\Pi^{\prime}\), the initiator and responder transmit ciphertexts:  
\[\Gamma_{3}=\mathsf{Enc}_{\mathsf{sk}_{\mathcal{A}}}(H(\mathsf{pk}_{\mathcal{ A}}\parallel\Gamma_{1})),\quad\Psi_{3}=\mathsf{Enc}_{\mathsf{sk}_{\mathcal{B}}}(H( \mathsf{pk}_{\mathcal{B}}\parallel\Psi_{1})).\]  
In this experiment, these values are replaced by randomly sampled bitstrings of the same length as the original ciphertexts:  
\[\Gamma_{3}^{*}\leftarrow\{0,1\}^{\lambda},\quad\Psi_{3}^{*}\leftarrow\{0,1\}^ {\lambda},\]  
where \(\lambda\) is the ciphertext length in bits. These random values are generated lazily--that is, at the moment they are first required--and stored in a lookup table to ensure consistency for repeated references. Since the encryption scheme \(\mathsf{Enc}\) is assumed to be IND-CPA secure, it follows that the adversary \(\mathcal{E}\) cannot distinguish between a real encryption of a known value and a uniformly random bitstring, unless it queries the corresponding message to the random oracle. Formally, this is captured by the following bound:  
\[\left|\Pr\left[\mathsf{Exp}_{\mathcal{E}}^{\Pi^{\prime},2}(k)=1\right]-\Pr \left[\mathsf{Exp}_{\mathcal{E}}^{\Pi^{\prime},1}(k)=1\right]\right|\leq \epsilon_{\text{enc}}(k),\]  
where \(\epsilon_{\text{enc}}(k)\) is a negligible function derived from the IND-CPA security of the encryption scheme. To support the above reduction, we construct a hypothetical adversary \(\mathcal{E}^{\prime}\) that breaks the IND-CPA security of \(\mathsf{Enc}\) by embedding the challenge ciphertext into one of the protocol's encrypted values (e.g., replacing \(\Gamma_{3}\)). If \(\mathcal{E}\) can distinguish the simulation from a real run with non-negligible probability, then \(\mathcal{E}^{\prime}\) can use this to decide whether the challenge ciphertext encrypts a real hash value or a random string--contradicting the assumption that \(\mathsf{Enc}\) is IND-CPA secure. Therefore, from the perspective of \(\mathcal{E}\), the distributions of \(\Gamma_{3}^{*}\) and \(\Psi_{3}^{*}\) are computationally indistinguishable from their real encrypted counterparts under the encryption key of the respective parties.