Live data from Hacker News

Rosenpass – formally verified post-quantum WireGuard

github.com

81–86 of 86 posts

Re: Rosenpass – formally verified post-quantum WireGuard

#81
post #80

Earlier quoted context omitted.

Nice. But I think you missed an update, Mullvad now also uses Kyber, your tool doesn't appear to. You also don't need Go: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t...

I'm intentionally not using Kyber, the key xor only happens if you elect to use both. It works just fine with McEliece only. > You also don't need Go You don't need any language in particular. That's the beauty of the .proto spec. Can generate some client(and server) code in whatever language you want(that protoc supports).

Do you have a reason to not use Kyber? The way it is combined should be sound.

Re: Rosenpass – formally verified post-quantum WireGuard

#82

> We are working on a cryptographic proof of security, but we already provide a symbolic analysis using proverif as part of the software package How can you prove this? There is still no mathematical proof that i.e discrete log is NP complete edit - I see it's a WIP but even the definition of secure seems difficult

Rosenpass author here; There is a confusion about terminology here I think. Mathematical proofs including cryptography proofs use models simplifying reality; i.e. the real practical system might still be susceptible to attacks despite a proof of security. For crypto primitives (classic mc eliece, curve25519, ed25519, RSA, etc etc) the standard for proofs is currently showing that they are as hard as some well studied…

Thank you for the informative comment!

Re: Rosenpass – formally verified post-quantum WireGuard

#83

Earlier quoted context omitted.

It's important to point out that these programs have two different objectives. The Mullvad client is designed to connect to a closed-source service, which is run by someone else. It supports a bunch of different plugins, including openvpn and WireGuard. So probably it could adopt rosenpass, at least with its WG plugin. WireGuard is designed for minimal protocol variability, high assurance implementations, and ultra s…

True. But they should have just forked either wireguard-go or boringtun to implement this functionality, and give up on the wg driver, the WG author seems like he doesn't care about PQC. Juggling multiple tooling is always a hassle. It's also not clear how the WG PSK change is coordinated, and whether that entails a brief loss of connectivity - packet loss, latency spike.

Rosenpass author here;

Mate, you could just read the code…or give it a try ;)

> the WG author seems like he doesn't care about PQC

This is plainly not true; WG supports post-quantum security with the use of the PSK mechanism as we do. PQ-crypto is high quality but it is also new and fairly inefficient; not a good thing to integrate into the kernel directly. Using the PSK mechanism is the best way to do this I know of at this point in time.

> It's also not clear how the WG PSK change is coordinated, and whether that entails a brief loss of connectivity - packet loss, latency spike.

WireGuard establishes a session with the existing PSK; we replace the PSK every two minutes but WireGuard keeps its established session around until it renegotiates a session.

Both WG and RP rekey their session every two minutes; there is no interruption.

Re: Rosenpass – formally verified post-quantum WireGuard

#84
post #80

Earlier quoted context omitted.

I'm intentionally not using Kyber, the key xor only happens if you elect to use both. It works just fine with McEliece only. > You also don't need Go You don't need any language in particular. That's the beauty of the .proto spec. Can generate some client(and server) code in whatever language you want(that protoc supports).

Do you have a reason to not use Kyber? The way it is combined should be sound.

Not in particular. Yes, the way they are combining them should be sound.

Re: Rosenpass – formally verified post-quantum WireGuard

#85
post #39

Earlier quoted context omitted.

You can add `#![forbid(unsafe_code)]` to your codebase to avoid any unsafe Rust, which should prevent buffer overflows. Obviously it may make writing a codebase somewhat harder.

Will that restriction also be applied transitively to all dependencies?

No, and in fact that would be impractical, because you can't do anything useful (e.g., any I/O whatsoever) without ultimately either calling into a non-Rust library or issuing system calls directly, both of which are unsafe.

Re: Rosenpass – formally verified post-quantum WireGuard

#86

Earlier quoted context omitted.

True. But they should have just forked either wireguard-go or boringtun to implement this functionality, and give up on the wg driver, the WG author seems like he doesn't care about PQC. Juggling multiple tooling is always a hassle. It's also not clear how the WG PSK change is coordinated, and whether that entails a brief loss of connectivity - packet loss, latency spike.

Rosenpass author here; Mate, you could just read the code…or give it a try ;) > the WG author seems like he doesn't care about PQC This is plainly not true; WG supports post-quantum security with the use of the PSK mechanism as we do. PQ-crypto is high quality but it is also new and fairly inefficient; not a good thing to integrate into the kernel directly. Using the PSK mechanism is the best way to do this I know of…

So is the rosenpass tunnel separate from the non PQC tunnel (the non PQC tunnel being used just for rosenpass)?

Because afaik the moment the PSK is changed all packets immediately start being encrypted by it.

If the change doesn't coincide on both the sender and receiver (within an instant), there will be dropped packets until both PSK's are the same again. Being separate from WG, I don't see how you can insert yourself into their state machine for better coordination.

Post reply on HN