Extended Canetti-Krawczyk - Clean Session Definition

Question

In the extended Canetti-Krawczyk (eCK) model [1] the adversary $\mathcal{M}$ is allowed to make a sequence of queries, eventually performs a $Test(sid)$ query, receives a value $C$ and at some point later has to guess whether $C$ was the session key or a random value. In order for $\mathcal{M}$ to win the experiment, they have to both guess the challenge correctly and the test session has to be clean. The latter means none of the following conditions may be true:

• $\mathcal{A}$ or $\mathcal{B}$ is an adversary-controlled party. This means in particular that $\mathcal{M}$ chooses or reveals both the long-term and ephemeral secret keys for the party and performs all communications and computations on behalf of the party.
• $\mathcal{M}$ reveals the session key of $sid$ or $sid^*$ (if the latter exists).
• Session $sid^*$ exists and $\mathcal{M}$ reveals either both $sk_\mathcal{A}$ and $esk_\mathcal{A}$, or both $sk_\mathcal{B}$ and $esk_\mathcal{B}$
• Session $sid^*$ doesn't exist and $\mathcal{M}$ reveals either $sk_\mathcal{B}$ or both $sk_\mathcal{A}$ and $esk_\mathcal{A}$

The first condition appears to state, that the adversary $\mathcal{M}$ would not be allowed to perform a man-in-the-middle attack on the test session between $\mathcal{A}$ and $\mathcal{B}$.

As far as I can tell, the original CK model didn't make such a restriction and intuitively I don't see why the adversary would be forbidden to impersonate the parties to each other. It would demonstrate that the adversary is able to break the authentication of the AKE protocol and as such it wouldn't be secure.

Am I misunderstanding the definition or is this actually forbidden in the model? If a MITM is allowed, then please point out the particular aspect of the model definition that allows this.

[1] LaMacchia, Brian, Kristin Lauter, and Anton Mityagin. "Stronger security of authenticated key exchange." International conference on provable security. Springer, Berlin, Heidelberg, 2007.

Answer 1

The first condition appears to state, that the adversary $\mathcal M$ would not be allowed to perform a man-in-the-middle attack on the test session between $\mathcal A$ and $\mathcal B$.

This is not correct. The eCK model does allow MitM attacks.

For some more background on formal AKE models see this question. To quickly recap, in an AKE model (including the eCK model) the adversary is assumed to control the entire network and can re-route, change, and drop message as it sees fit. In particular, this means that the adversary can do MitM attacks almost by definition. Then, to measure the adversary's ability to break the protocol, the adversary is given a Test session (a running instance of the protocol at some party, say $\mathcal A$) for which it is asked to distinguish its real session key from a random key. If the adversary can't do this, then we say that the protocol is secure. Notice in particular that the adversary can pick a Test session for which the adversary itself created all the messages it sent to the Test session (thus modelling a MitM attack). This is also true for the eCK model.

However, AKE models (including eCK) usually go beyond just MitM attacks, and also allow the adversary to obtain many of the secret values in the system too. This can include session keys derived by sessions other than the Test session itself, long-term keys held by the parties, and also the full internal randomness used by the sessions (the eCK model allows all three of these). However, once we start allowing the adversary these additional powers, certain unavoidable attacks start to become possible. It is this that the quote you refer to is about. In particular

$\mathcal A$ or $\mathcal B$ is an adversary-controlled party. This means in particular that $\mathcal B$ chooses or reveals both the long-term and ephemeral secret keys for the party and performs all communications and computations on behalf of the party.

deals with the following attack. Suppose the adversary picks the Test session to be at party $\mathcal B$ (communicating with a session at party $\mathcal A$). Now, using the powers granted to it in the eCK model, the adversary obtains the long-term key of party $\mathcal A$ as well as all the internal randomness used by the the running instance at $\mathcal A$. At this point the adversary has all the secret values that the honest session at $\mathcal A$ would use when communicating with $\mathcal B$, hence it can trivially impersonate $\mathcal A$ towards $\mathcal B$ allowing it to compute the same session key as the Test session (at $\mathcal B$). Thus it can trivially break the protocol. However, note that this attack is unavoidable given the powers the adversary is given. Thus, to make the eCK model meaningful, these trivial attacks need to be disallowed, and this what the restriction above does.

In summary, the eCK model allows MitM attacks, but since it also allows the adversary additional powers (such as obtaining certain secret values in the system), it must also impose some constraints on the adversary in order to account for the possibility of trivial attacks made possible by these powers.