# Proof of a key agreement protocol based on bilinear pairings

I'm currently trying to understand a proof of a protocol of the paper of Liqun Chen and Caroline Kudla entitled "Identity Based Authenticated Key Agreement Protocols from Pairings". You can find a copy here.

In particular, it is a key agreement protocol which makes use of the bilinear maps. The protocol is the one described in the page 6 of the paper. The protocol is not very complex. It considers two users Alice, and Bob. Both choose at random their ephemeral private keys $a,b\in \mathbb{Z}_n^*$. Then both interchange the ephemeral keys $W_A=aQ_A$ and $W_B=bQ_B$ where $Q_A=H(ID_A)$ and $Q_B=H(ID_B)$. Then the established key can be computed by using a bilinear map as $K_{AB}=\hat{e}(S_A, W_A+aQ_B)$ and $K_{BA}=\hat{e}(W_A+bQ_A, S_B)$, where $S_A=sQ_A$ and $S_B=sQ_B$ (generated by the KGC).

The protocol is proven secure under the Bellare and Rogaway model. However there is a particular step that I don not understand which is associated with Theorem 1 of the paper. In particular, when they say (at top page 7):

Now call $A_k$ the event that $H_2$ has been queried on $\hat{e}(Q_I, Q_J)^{s(i + j)}$ by $E$ or some oracle other than $\Pi_{IJ}^n$ or $\Pi_{J,I}^t$. Then

Following, they say:

$Pr[E\text{ succeeds}] = Pr[E\text{ succeeds}|A_k]Pr[A_k] + Pr[E\text{ succeeds}|Ā_k]Pr[Ā_k]$.

Are they considering the case $Pr[E\text{ success} \cap A_k]$ and $Pr[E\text{ success} \cap Ā_k]$ for the first and second part of the previous expression?

Later, they assume $Pr[E\text{ succeeds}|Ā_k] = \frac{1}{2}$ which I understand. However, later they consider:

$\frac{1}{2}+ η(k) ≤ Pr[E\text{ succeeds}|A_k]Pr[A_k] + \frac{1}{2}$

and say "Thus $Pr[A_k] ≥ η(k)$". How they conclude this last expression from the previous one? I can understand that:

$η(k) ≤ Pr[E\text{ succeeds}|A_k]Pr[A_k]$

however... I can't see how they deduce $Pr[A_k] ≥ η(k)$ from the last expression.

I guess that it is something related with probabilities, but I suppose that I'm missing something...

however... I can't see how they deduce $Pr[A_k] ≥ η(k)$ from the last expression.
They use the upper bound $Pr[E\text{ succeeds}|A_k]Pr[A_k]\leq Pr[A_k]$, which follows from the fact that $Pr[E\text{ succeeds}|A_k]\leq 1$.