[noise] IKpsk2 in Noise Explorer!

[Nadim Kobeissi]

Hello everyone,
I'm excited to be able to say that Noise Explorer finally contains a full
analysis of IKpsk2! This is the Noise Handshake Pattern used in WireGuard.

It took 21 days to run IKpsk2's ProVerif model.

The results are available here:
https://noiseexplorer.com/patterns/IKpsk2/

For comparison, IK's results are available here:
https://noiseexplorer.com/patterns/IK/

The intrepid among you will notice that upon first glance, IKpsk2 seems to
obtain security guarantees that are "weaker" than IK. For example, message
A in IK has an authentication grade of 1 and a confidentiality grade of 2,
whereas in IKpsk2, message A appears to have an authentication grade of 0
and a confidentiality grade of 0. This is misleading and I will explain why.

Whenever we test for static key compromise in non-PSK Noise Handshake
Patterns, the query looks something like this:
"event(RecvMsg(bob,alice,stagepack_a(sid_b),m)) ==>
event(SendMsg(alice,c_1211,stagepack_a(sid_a),m)) ||
event(LeakS(phase0,alice)) || event(LeakS(phase0,bob))."

..which translates to: "In this query, we test for sender authentication
and message integrity. If Bob receives a valid message from Alice, then
Alice must have sent that message to someone, or Alice had their static key
compromised before the session began, or Bob had their static key
compromised before the session began."

And whenever we test for static key compromise in PSK Noise Handshake
Patterns, the query looks something like this:
"event(RecvMsg(bob,alice,stagepack_a(sid_b),m)) ==>
event(SendMsg(alice,c_1342,stagepack_a(sid_a),m)) ||
(event(LeakS(phase0,alice)) && event(LeakPsk(phase0,alice,bob))) ||
(event(LeakS(phase0,bob)) && event(LeakPsk(phase0,alice,bob)))."

...which translates to: "In this query, we test for sender authentication
and message integrity. If Bob receives a valid message from Alice, then
Alice must have sent that message to someone, or Alice had their static key
******and PSK****** compromised before the session began, or Bob had their
static key ********and PSK********compromised before the session began."
(emphasis mine).

So therefore, notice that in PSK Noise Handshake Patterns, testing for
static key compromise across all security queries also comes conjoined with
a test for PSK compromise. The security query is modified to test whether
the compromise of the party's static key *and *PSK is necessary.

Since the PSK in IKpsk2 only appears at message B, its entailed effects or
security improvements occur only after that point. The updated security
queries are intended to reflect the PSK's before-and-after effect across
the entire Noise Handshake Pattern.

I hope that you find the parameters and queries for this analysis
reasonable. Of course, feedback is welcome.

Don't forget that 18 other PSK pattern analyses are also available:
https://noiseexplorer.com/patterns/ (type "psk" in the search bar.)

Best regards,

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/noise/attachments/20190207/4eff7198/attachment.html>