A reduction proof of SK-security for the Needham-Schroeder-Lowe protocol
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.