Why not just use PresharedKey in Wireguard?
You can do that on top of a public/private keypair, too.
Rosenpass – formally verified post-quantum WireGuard
11–20 of 86 posts
Re: Rosenpass – formally verified post-quantum WireGuard
#12I'm too stupid to understand the crypto technicalities. Is this really a good solution? Or embrace, extend, extinguish targeted on Wireguard? The paper abstract mentions a "cookie"-like concept, and from websec I know that cookies are not always the optimal solution and historically cookie implementations had a lot of attack surface. EDIT: Seems to come from German Max-Planck Institute which is funded by German gover…
> EDIT: Seems to come from German Max-Planck Institute which is funded by German government.
On the Github repo it says:
"Supported by
Funded through NLNet with financial support for the European Commission's NGI Assure program."
On the website it says:
"Funded through NLnet with financial support from the European Commission's NGI Assure program."
Re: Rosenpass – formally verified post-quantum WireGuard
#13Does formal verification protect against buffer overflows? (it's a serious question)
They verified the protocol, not the actual implementation: https://github.com/rosenpass/rosenpass#security-analysis
This is still a pretty neat result! End-to-end proofs from high level protocol to low level implementation are mostly still a research topic.
Re: Rosenpass – formally verified post-quantum WireGuard
#14Why not just use PresharedKey in Wireguard?
That's what they're doing, generating a key using post-quantum crypto and using it as the PSK - from TFA: "The tool establishes a symmetric key and provides it to WireGuard. Since it supplies WireGuard with key through the PSK feature using Rosenpass+WireGuard is cryptographically no less secure than using WireGuard on its own ("hybrid security"). Rosenpass refreshes the symmetric key every two minutes."
Re: Rosenpass – formally verified post-quantum WireGuard
#15Does formal verification protect against buffer overflows? (it's a serious question)
The code signing project I worked on was formally verified. The whole time they were verifying it I found horrible bugs that needed fixing. One even made it past soft launch. So great job boys but this doesn’t help me.
Re: Rosenpass – formally verified post-quantum WireGuard
#16Does formal verification protect against buffer overflows? (it's a serious question)
They verified the protocol, not the actual implementation: https://github.com/rosenpass/rosenpass#security-analysis This is still a pretty neat result! End-to-end proofs from high level protocol to low level implementation are mostly still a research topic.
Related: Coq - https://coq.inria.fr/
And CompCert, a formally verified C compiler written in Coq: https://compcert.org/
(even then, there are parts which are not formally verified, mostly at the interfaces with the outside world)
Re: Rosenpass – formally verified post-quantum WireGuard
#17Does formal verification protect against buffer overflows? (it's a serious question)
The code signing project I worked on was formally verified. The whole time they were verifying it I found horrible bugs that needed fixing. One even made it past soft launch. So great job boys but this doesn’t help me.
What is a bug in the spec? Or in a part that was not formally verified?
Re: Rosenpass – formally verified post-quantum WireGuard
#18Does formal verification protect against buffer overflows? (it's a serious question)
I suppose if its implemented in a language that is formally proven to not allow buffer overflows.
Re: Rosenpass – formally verified post-quantum WireGuard
#19I'm too stupid to understand the crypto technicalities. Is this really a good solution? Or embrace, extend, extinguish targeted on Wireguard? The paper abstract mentions a "cookie"-like concept, and from websec I know that cookies are not always the optimal solution and historically cookie implementations had a lot of attack surface. EDIT: Seems to come from German Max-Planck Institute which is funded by German gover…
> EDIT: Seems to come from German Max-Planck Institute which is funded by German government. On the Github repo it says: "Supported by Funded through NLNet with financial support for the European Commission's NGI Assure program." On the website it says: "Funded through NLnet with financial support from the European Commission's NGI Assure program."
On the paper it says MPI
Re: Rosenpass – formally verified post-quantum WireGuard
#20Why not just use PresharedKey in Wireguard?
That doesn't solve the key management problem, it just defines it as out-of-scope, since you still need to exchange that preshared key outside Wireguard.