A reduction proof of SK-security for the Needham-Schroeder-Lowe protocol 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?
I am not an expert on this subject, but it looks to me like the question makes some assumptions that may or may not be valid.  The question claims that the Needham-Schroeder-Lowe protocol is SK-secure.  However, I don't know whether there is any known proof that Needham-Schroeder-Lowe is SK-secure.  The paper that was cited in the question does not appear to claim that it is SK-secure.  You might want to start by first checking whether there's a known proof of its SK-security.

It's possible you might find the following paper of some relevance:


A Computational Analysis of the Needham-Schroeder-(Lowe) Protocol.  Bogdan Warinschi.  Computer Security Foundations Workshop 2003.


It gives a computational, reduction-oriented proof of security for the Needham-Schroeder-Lowe protocol, assuming that the encryption algorithm is CCA-secure.  However, I don't know what notion of security for key exchange algorithms this paper uses; I don't know if it proves SK-security, or something else.