The Needham-Schroeder-Lowe protocol works as follows between the initiator I and responder R:
$I \longrightarrow R : \text{Enc}_{pk_R}(r_I, I)$
$R \longrightarrow I : \text{Enc}_{pk_I}(r_I, r_R, R)$
$I \longrightarrow R : \text{Enc}_{pk_R}(r_R)$
(I assume throughout that the encryption scheme is CCA-secure.)
Upon receiving their messages, both parties decrypt using the corresponding private key and finally output $r_I$ as their session key.
I understand others have proven that this protocol is SK-secure protocol, based on the CK01 model for SK-security. (As a reminder, the protocol is secure in this model if no adversary can distinguish, with probability strictly greater than $1/2$, between the output $r_I$ of the protocol and a random bit.) Security was proven using formal methods. My question: is there a proof of this using an explicit reduction?