<p>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.</p>

<p>It's possible you might find the following paper of some relevance:</p>

<ul>
<li><a href="http://www.cs.bris.ac.uk/~bogdan/pdf/nsl.pdf" rel="nofollow">A Computational Analysis of the Needham-Schroeder-(Lowe) Protocol</a>.  Bogdan Warinschi.  Computer Security Foundations Workshop 2003.</li>
</ul>

<p>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.</p>

CC BY-SA 3.0
2013-03-02T01:52:48.363Z
2013-03-02T01:52:48.363Z
D.W.
<p>The <a href="http://www.math.upenn.edu/~bana/NSL.pdf" rel="nofollow">Needham-Schroeder-Lowe</a> protocol works as follows between the initiator I and responder R:</p>

<p>$I \longrightarrow R : \text{Enc}_{pk_R}(r_I, I)$</p>

<p>$R \longrightarrow I : \text{Enc}_{pk_I}(r_I, r_R, R)$</p>

<p>$I \longrightarrow R : \text{Enc}_{pk_R}(r_R)$</p>

<p>(I assume throughout that the encryption scheme is CCA-secure.)</p>

<p>Upon receiving their messages, both parties decrypt using the corresponding private key and finally output $r_I$ as their session key.</p>

<p>I understand <a href="http://www.math.upenn.edu/~bana/NSL.pdf" rel="nofollow">others have proven</a> that this protocol is SK-secure protocol, based on the <a href="http://eprint.iacr.org/2001/040" rel="nofollow">CK01</a> 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?</p>

CC BY-SA 3.0
2013-02-28T00:38:45.457Z
I recommend that you flag this to be moved over to [Crypto.SE](http://crypto.stackexchange.com).  Also, I recommend that you provide a link to the specification of the NSL protocol, add a link to the CK01 paper, and, provide a definition of SK-security.  Also, tell us what you've tried so far or how far you've gotten on your own, and why you think it "should be SK-secure".
D.W.
CC BY-SA 3.0
2013-02-28T15:47:08.297Z
@D.W.  NSL protocol has been shown to be secure using other techniques such as formal methods, e.g. see this(http://www.math.upenn.edu/~bana/NSL.pdf). It also achieves SK-security, so my question is that how can one use reduction to show it?
Brian
CC BY-SA 3.0
2013-03-02T01:46:14.720Z
This question would benefit from a lot of additional work, to try to be clearer.  I recommend you stick to standard notation/terminology.  The protocol is commonly known as Needham-Schroeder-Lowe (I've never heard of anyone call it NSL).  Normally we use $N_A$ for a nonce generated by $A$; you use $r_I$ but don't specify what that value is.  You claim this has been proven to be SK-secure but don't provide any citation for this; the paper you cited never makes that claim.  If you want a reduction, I suggest you specify what you want it reduced to (the CCA-security of the encryption scheme?).
D.W.
<cr.crypto-security><key-exchange>
A reduction proof of SK-security for the Needham-Schroeder-Lowe protocol
Brian
# A reduction proof of SK-security for the Needham-Schroeder-Lowe protocol

(Asked by: username_0 on 2013-02-27)

The [Needham-Schroeder-Lowe](http://www.math.upenn.edu/~bana/NSL.pdf) 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](http://www.math.upenn.edu/~bana/NSL.pdf) that this protocol is SK-secure protocol, based on the [CK01](http://eprint.iacr.org/2001/040) 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?

**Tags:** cr.crypto-security, key-exchange
> **Comments:**
> **username_1**: I recommend that you flag this to be moved over to [Crypto.SE](http://crypto.stackexchange.com).  Also, I recommend that you provide a link to the specification of the NSL protocol, add a link to the CK01 paper, and, provide a definition of SK-security.  Also, tell us what you've tried so far or how far you've gotten on your own, and why you think it "should be SK-secure".  
> **username_0**: @D.W.  NSL protocol has been shown to be secure using other techniques such as formal methods, e.g. see this(http://www.math.upenn.edu/~bana/NSL.pdf). It also achieves SK-security, so my question is that how can one use reduction to show it?  
> **username_1**: This question would benefit from a lot of additional work, to try to be clearer.  I recommend you stick to standard notation/terminology.  The protocol is commonly known as Needham-Schroeder-Lowe (I've never heard of anyone call it NSL).  Normally we use $N_A$ for a nonce generated by $A$; you use $r_I$ but don't specify what that value is.  You claim this has been proven to be SK-secure but don't provide any citation for this; the paper you cited never makes that claim.  If you want a reduction, I suggest you specify what you want it reduced to (the CCA-security of the encryption scheme?).  

---

## 1 answers

### Answer by username_1 on 2013-03-02. Score: 1

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](http://www.cs.bris.ac.uk/~bogdan/pdf/nsl.pdf). 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.


---

