A confusion about HMQV?

Question

As the full version of HMQV is very long, I will give a graph of it below

---

\begin{array}{@{}l@{}c@{}l@{}} \hat{A} && \hat{B} \\ (a,A=g^a)&&(b,B=g^b) \\ x\in_R[1,q-1],\quad X=g^x \\ & \xrightarrow{\textstyle \hat{A},\hat{B},X} \\ %&& verify \; X \in G^* \\ && y\in_R [1,q-1],\quad Y=g^y \\ & \xleftarrow {\textstyle \hat{B},\hat{A},Y} \\ && d=\bar{H}(X,\hat{B}), \quad e=\bar{H}(Y,\hat{A}) \\ && s_B=y+eb,\quad \sigma_B=(XA^d)^{s_B} \\ && K=H(\sigma_B) \\ %verify \; Y \in G^*\\ d=\bar{H}(X,\hat{B}), \quad e=\bar{H}(Y,\hat{A}) \\ s_A=x+da,\quad \sigma_A=(YB^e)^{s_A} \\ K=H(\sigma_A) \\ \end{array}

---

$a$ and $A=g^a$ are static private key and public key of party $\hat{A}$ ($\hat{A}$ denote the identity of a user ) respectively ,and the same with $\hat{B}$ .

HMQV appears in 2005, while the eCK model appears in 2007. After that , nobody try to prove the security of HMQV under eCK model, although,intuitively it's secure under eCK. So, I wonder that why nobody give a proof of it ? Could someone give a sketch of proving HMQV under eCK model?

Answer 1

In this paper it is shown that the security model under which HMQV was designed (CK-HMQV) and the eCK model are incomparable based on their security prerequisites, adversary model, and application domain. Essentially, there are known protocols which are secure in the eCK model but insecure in the CK-HMQV and other protocols which are secure in the CK-HMQV but insecure in the eCK model.

Specifically, for the HMQV model the author states:

The HMQV protocol is insecure in eCK because the adversary can trivially reveal the session key in the two-initiators scenario, as in the proof of Theorem 3. The insecurity is based on a mismatch between the equivalence type of matching sessions and the equivalence type of derived keys.

The definitions of equivalence for session and keys can be found for Definition 3 and 4. The equivalences $\approx_A$, $\approx_B$, $\approx_C$ and $\approx_D$ for sessions basically define conditions that need to be satisfied for sessions to be equivalent and the key equivalence means that sessions which are equivalent with respect to $\approx$ yield the same derived keys.

Theorem 3 states that: Role-symmetric protocols with key type $\approx_A$ or $\approx_B$ are insecure in eCK.

Where a protocol is said to be role-symmetric, when the messages of each role (sender, receiver) are identical up to their order (which holds for the HMQV protocol).

Now, HMQV is role-symmetric and the key equivalence type is $\approx_A$ and the matching sessions equivalence type used in the proof is $\approx_A$ (see Table 2). Unfortunately, this means that HMQV cannot be secure in the eCK security model.

Consequently, the HMQV protocol as it is can not shown to be secure in the eCK model, although it may intuitively seem to be the case (but security models for AKE are quite complicated and there can be very tricky issues which are not that obvious).

Observe that as stated by the author in Section 2.5 that eCK-matching is equal to CKHMQV-matching $\wedge$ $s_{role}\neq s'_{role}$.

This basically says that for matching sessions $s$ and $s'$ which are equivalent, i.e., lead to the same derived key, it must not be the case that they can be obtained when conducted in the same role (sender or receiver) in the security game. Thats what is stated in the cited part above. This indicates that one way to modify HMQV to provide eCK security is to break the role symmetry and/or include session identifiers into the messages (but I am no expert in AKE and this my intuition :)