[noise] Noise Explorer

[Nadim Kobeissi]

Answers inline.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Apr 1, 2019, at 11:15 PM, Sebastian R. Verschoor <srverschoor at uwaterloo.ca> wrote:
> 
> Hi Nadim and Karthikeyan,
> 
> I am working on a proverif model with quite a few Diffie-Hellman operations and I am struggling with the efficiency of proverif (or even making it terminate), so I figured I would look at an example of a similar model. That brought me to your your paper [0] and the corresponding proverif models. So far it has been very instructive, so thank you for making them. However, quite a few questions did come up and I was hoping you could help me answer them.
> 
> 1. I noticed your decryption reduction only works when provided with the correct nonce and ad, so that these essentially act as keys to the encrypt function. Is there a reason for not including another reduction to get the plaintext with just the key and ciphertext?

I suppose not, actually. Well, decryption would fail without the nonce, but perhaps you are correct in that a more permissive reduction such as the one you suggest would be more appropriate. I wonder if Karthik agrees.

> 1a. (maybe related:) why is there a boolean parameter in aeadpack, always set to true?

This is the boolean that indicates whether decryption succeeded.

> 1b. (maybe also related:) why are the valid parameters there at all?

Because it is supposedly set to false if decryption fails, but that is a vestigial thing from a long time ago.

> 2. I notice you model X25519 private keys and public keys as the same type, while one is a scalar and the other a point on the elliptic curve. Is there a reason for not making this distinction (does it matter at all)?

It doesn’t matter in the symbolic model. It would matter in the computational model (i.e. CryptoVerif).

> 3. EncryptWithAd does not return the plaintext when k is empty. This means that sometimes an encrypted value is sent while plaintext should have been sent. I believe that this is always an encryption using the key "empty", the minnonce and a publicly known ad, so that an adversary can still recover the plaintext. I have only checked a few patterns so I'm not sure about this last statement. You have modelled the hasKey primitive, is there a reason you never call it?

Well, it encrypts with k = empty, which is a public value known to the attacker. So the end result is the same as sending plaintext. We model hasKey because it’s in the spec, but we don’t call it because doing so won’t change the model except to make it more expensive to run by adding another branching statement at the primitive level.

> 4. Using the example of Figure 5 from the paper: pattern IK. At the end of readmessage_a you validate that the received static key is the same as the one you retrieve through the private key_s function. That implies to me that you already have access to the public key, so why must it still be sent in the message? Or is this somehow an abstraction of public key validation, where you just assume that Bob somehow knows Alice's public key?

We do this in order to model our assumption that static keys always benefit from mutual out-of-band authentication in our models. We still send it over the wire anyway just so that we appropriately adhere to the Noise wire format and also so the attacker can see more realistic Noise wire messages over the network.

> 5. I am a bit confused by the sid in the main process. Session id's aren't present in the Noise protocol, so they must represent something else. I guess what confuses me is that the sessions with Charlie share the same sid... Could you maybe give a brief comment on the idea behind these sid’s?

This is explained in the paper:

"Our analysis of authentication grades comes with an important limitation: When Noise Explorer generates the authentication queries below, it uses two different values, sid_a and sid_b, to refer to the session ID as registered in the trigger events by Alice and Bob. This differs from, and is in fact less accurate than the queries described previously, which use the same session ID, sid, for both Alice and Bob. We are forced to adopt this approach due to performance limitations in our models during verification should we choose to use a single sid value for both Alice and Bob. However, we argue that since processes with differing sid values cause decryption operations that use shared secrets derived from ephemeral keys to fail, and therefore for those processes to halt, we still obtain essentially the same verification scenarios that these queries target.”

Not the nicest thing, I know, but unfortunately it was necessary to add this to our models.

> 6. I noticed that almost in none of the results proverif is able to prove that a query is false, it almost always says that a property cannot be proved. What concerns me a bit with those queries is that some of them include "sanity queries". For example the RecvEnd event should be triggered when the adversary does nothing, so it seems remarkable to me that this event cannot be proved. Should I worry that the model may be incorrect?

No, we indeed expect sanity queries to either be false or “cannot be proved”, which means that ProVerif cannot prove it as true and presents a reconstruction of an attack that contradicts the query. You see, this is because of ProVerif’s (very annoying) penchant for double negatives:

```
Starting query not event(RecvEnd(true))
goal reachable: begin(SendMsg(alice,charlie,stagepack_c(sid[!1 = @sid_30100814]),msg_c(alice,charlie,sid[!1 = @sid_30100814]))) && begin(SendMsg(alice,charlie,stagepack_a(sid[!1 = @sid_30100814]),msg_a(alice,charlie,sid[!1 = @sid_30100814]))) -> end(RecvEnd(true))

[…kilobytes of illegible nonsense later…]

So event RecvEnd(true) may be executed at {246}.
end(RecvEnd(true)).
RESULT not event(RecvEnd(true)) cannot be proved.
```

> 7. Using the example of Figure 9 from the paper: pattern IK. Message D can only be sent after (the first) message C has been sent, while in Noise either party should be able to send transport messages after completion of the handshake.

If you look at the models, you’ll see that we’re executing unbounded executions of transport messages in parallel, so I don’t think we are indeed waiting for message C to be sent first (maybe I’m missing something):

```
 !(
    get statestore(=me, =them, =sid, statepack_c(hs, cs1, cs2)) in
    let hs = handshakestatesetcs(hs, cs1) in
    in(pub, message_c:bitstring);
    let (hs:handshakestate, plaintext_c:bitstring, valid:bool) = readMessage_c(me, them, hs, message_c, sid) in
    event RecvMsg(me, them, stagepack_c(sid), plaintext_c);
    insert statestore(me, them, sid, statepack_d(hs, handshakestategetcs(hs), cs2));
    0
  ) | !(
    get statestore(=me, =them, =sid, statepack_d(hs, cs1, cs2)) in
    let hs = handshakestatesetcs(hs, cs2) in
    let (hs:handshakestate, message_d:bitstring) = writeMessage_d(me, them, hs, msg_d(me, them, sid), sid) in
    event SendMsg(me, them, stagepack_d(sid), msg_d(me, them, sid));
    (* Final message, do not pack state *)
    out(pub, message_d)
  )
```

> 7a. The protocol participants enter the state where they can send transport messages while they still hold onto their handshakestate. It was my understanding that after split is called at the end of the handshake, the participants only hold onto the sending- and receiving-cipherstate.

I don’t know whether we can meaningfully model the “deletion” of values in ProVerif especially in the context of unbounded parallel executions being modeled symbolically.

> 
> If your still reading this, thanks! I realize this is a lot of questions, but I hope to hear from you.

Thank you for the great questions!

> 
> Thanks in advance,
> Sebastian
> 
> Ps. if you think it is helpful feel free to continue this conversation on the noise mailing list.

Good idea, I will do so.

> 
> [0]: https://eprint.iacr.org/2018/766/20181202:150953
> 
> On Fri, 24 Aug 2018 at 04:28, Trevor Perrin <trevp at trevp.net> wrote:
> On Tue, Aug 21, 2018 at 9:08 AM, Nadim Kobeissi <nadim at symbolic.software> wrote:
> > Hello everyone,
> > A Noise Explorer paper now exists:
> > https://eprint.iacr.org/2018/766
> 
> 
> Very nice, few bits of feedback:
> 
> 
> Section 2: The example of pre-messages isn't great: "could be used in
> secure messaging protocols, where prior knowledge of an ephemeral...".
> It's not clear what "secure messaging" means in this context, and we
> mostly use pre-messages with static keys, not ephemeral keys, except
> for the fallback case.
> 
> Better examples would probably be "one-shot" protocols like public-key
> encryption to a static key, or 0-RTT handshakes where the static key
> was cached or was looked up via some directory.
> 
> 
> Section 2: The validity rules listed here omit a crucial validity rule
> which has been in the spec for a long time.  (The paper then
> re-invents that rule as a proposal in Section 5.2, so I'll say more
> about that below).
> 
> 
> Section 2: The footnote 2 isn't correct as of revision 34.  It's not
> clear whether this paper intends to reference revision 33 or 34, it
> seems to switch back and forth.
> 
> 
> Section 2.3: We renamed the security-property grades to "initiator"
> and "responder in revision 34, in response to discussions with Noise
> Explorer team.
> 
> 
> Section 2.3: the properties introduced in your new "authentication"
> grades 3 and 4 are already covered by the existing "responder" (or
> "confidentiality" grades), which is why I think these are redundant
> and shouldn't be introduced.
> 
> 
> Section 2.4:  The deferred patterns only defer DH operations, not "the
> communication of public keys".
> 
> Figure 7:  Surprised me a bit that the WireGuard pattern (IKpsk2) isn't listed.
> 
> Section 5.2:  This section claims to "discover a novel forgery attack
> within certain Noise handshake patterns".  However the example is an
> invalid Noise handshake pattern, so this isn't an attack against
> Noise.  Also, I wouldn't call this a novel discovery, since we had
> anticipated it and had a rule to prevent it.
> 
> In revision 33, the validity rule that disallows this pattern was
> unambiguous, if terse:
> 
> "After performing a DH between a remote public key and any local private
> key that is not the ephemeral private key, the local party must not call
> ENCRYPT() unless it has also performed a DH between the ephemeral
> private key and the remote public key."
> 
> This rule was intended to prevent the scenario you describe:  the
> victim using a DH output like ss without randomizing it via an
> ephemeral-static DH with your partner's static.
> 
> Anyways, the paper proposes that a "A Noise Handshake Pattern
> validation rule could be introduced to disallow the usage of ss in a
> handshake unless it is accompanied by se of es in the same handshake
> pattern."
> 
> This rule existed!  The paper goes on to talk about a "lack of clarity
> in the then-current revision", and that "As a result of our report,
> revision 34 of the Noise Protocol Framework specification included the
> following more stringent pattern validity rule. [...]  These new
> validity rules [...]".
> 
> I disagree with that history: The validity rule didn't change.
> However, since your team had seemingly missed and then mis-read the
> existing rule, and since it lacked a good rationale, I added more
> descriptive text, and spelled it out specifically for static keys (I
> had written it more generally initially, to allow for different types
> of keys in the future, like semi-static or something).
> 
> Aside from that, I quite like the paper, it could use some polish and
> proofreading, but I look forward to the final version!
> 
> Trevor
> _______________________________________________
> Noise mailing list
> Noise at moderncrypto.org
> https://moderncrypto.org/mailman/listinfo/noise