What is super interesting is that rosenpass logo is a rabbit, a duck, and a sinister looking boy sporting a cap all fighting over the same key .. https://raw.githubusercontent.com/rosenpass/rosenpass/papers...
Rosenpass – formally verified post-quantum WireGuard
71–80 of 86 posts
Re: Rosenpass – formally verified post-quantum WireGuard
#72Mullvad VPN has a PQC key exchange feature, they are even using two algorithms in parallel: McEliece and Kyber. https://github.com/mullvad/mullvadvpn-app/tree/main/talpid-t...
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 small code size. It's used by VPN services, but also by end-users creating their own tunnels.
Re: Rosenpass – formally verified post-quantum WireGuard
#73Does formal verification protect against buffer overflows? (it's a serious question)
Maybe not in general, but there is really interesting work happening in the area of verified protocols generating safe C code (memory safe, overflow safe, timing safe, etc). In particular Project Everest has a set of verified primitives underlying higher level protocols like TLS and more recently all Noise variants ( https://eprint.iacr.org/2022/607 ). As WireGuard is based on a Noise construction, it seems reasonabl…
I’ve seen some draft ideas for Noise patterns using Kyber on a slack I am on, but they’d be different since Kyber is a KEM rather than a Diffie-Hellman type construction. Noise is all built around DH.
You can use Kyber alongside Noise in a hybrid construction. Just mix it in with the PSK or something.
Re: Rosenpass – formally verified post-quantum WireGuard
#74Mullvad VPN has a PQC key exchange feature, they are even using two algorithms in parallel: McEliece and Kyber. https://github.com/mullvad/mullvadvpn-app/tree/main/talpid-t...
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…
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.
Re: Rosenpass – formally verified post-quantum WireGuard
#75Earlier quoted context omitted.
Rosenpass author here; nope, that is not correct. NIST has elected Kyber as one of the algorithms to standardize and we are using that. As other commenters mentioned (very good info there, thank you all!) the other algorithm we use – Classic McEliece – is one of the oldest algorithms and has been well studied. There is no known efficient attack against it.
Have you seen https://isd.mceliece.org/1347.html ? DJB agrees with you.
Re: Rosenpass – formally verified post-quantum WireGuard
#76Earlier 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.
If you're a fuddy-dud like me who uses the Vanilla WireGuard config files, I wrote a tool to upgrade your pre-quantum peer to a post-quantum one. https://github.com/d-z-m/pq-adapter-mullvad
Re: Rosenpass – formally verified post-quantum WireGuard
#77Earlier 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.
They maintain separate peers for Pre-quantum and Post-quantum so that connectivity isn't interrupted. Each Pre-quantum peer is implicitly paired with a corresponding Post-quantum peer. Negotiating the PSK happens over a grpc api they expose at `10.64.0.1:1337`. The spec is public, if you're curious: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t... If you're a fuddy-dud like me who uses the Vanilla Wire…
Re: Rosenpass – formally verified post-quantum WireGuard
#78Earlier 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.
They maintain separate peers for Pre-quantum and Post-quantum so that connectivity isn't interrupted. Each Pre-quantum peer is implicitly paired with a corresponding Post-quantum peer. Negotiating the PSK happens over a grpc api they expose at `10.64.0.1:1337`. The spec is public, if you're curious: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t... If you're a fuddy-dud like me who uses the Vanilla Wire…
You also don't need Go: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t...
Re: Rosenpass – formally verified post-quantum WireGuard
#79This available in tailscale?
Re: Rosenpass – formally verified post-quantum WireGuard
#80Earlier quoted context omitted.
They maintain separate peers for Pre-quantum and Post-quantum so that connectivity isn't interrupted. Each Pre-quantum peer is implicitly paired with a corresponding Post-quantum peer. Negotiating the PSK happens over a grpc api they expose at `10.64.0.1:1337`. The spec is public, if you're curious: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t... If you're a fuddy-dud like me who uses the Vanilla Wire…
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...
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).