[noise] IKpsk2 in Noise Explorer!

[Nadim Kobeissi]

Hello everyone,

Related news: Noise Explorer's compendium now also has formal verification
results IKpsk1!

https://noiseexplorer.com/patterns/IKpsk1/

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Thu, Feb 7, 2019 at 12:50 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> 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/20190505/c9dbd0c6/attachment.html>