I recently came across a compelling story about the long-term impact of academic conferences—one that involves the Network and Distributed System Security (NDSS) Symposium.
I have been experimenting with the WireGuard Virtual Private Network (VPN) protocol for some time. For those not aware, it is a modern technology used to create VPNs that allow securing paths through untrusted networks. It is rapidly replacing older technologies because it is faster, leaner, and easier to audit, and as such is now used by millions of devices worldwide.
Serendipitously, its creator, Jason Donenfeld, was not long ago featured on the Security, Cryptography, Whatever podcast—which I frequently listen to and am a big fan of—during which he shared his experience presenting the protocol at NDSS in 2017.
After presenting his talk, Jason recollected meeting Kevin Milner, who taught him about a concept called “formal verification,” which later became a major factor in why WireGuard is considered so secure today.
Usually, when developers write software, they run “tests” to see if it works. Testing is like driving a car around the block to see if the brakes work. Formal verification is using complex mathematics to prove that it is impossible for the brakes to fail under any laws of physics. It provides a mathematical guarantee that the security protocol contains no logical flaws.
Below is the excerpt where Jason talks about that moment:
[01:03:54] Thomas Ptacek: Some of the flak that WireGuard got was from people that were really big into formal verification… there’s a notion that like, you know, any new major protocol… should be designed with formal methods and, you know, should be directly provable in some model that we already have. How compelling do you find that argument?
[01:04:18] Jason Donenfeld: I mean, I think it’s a compelling argument. It was used in context to say like NDSS never should have accepted the WireGuard paper because it didn’t come with a formal security proof… You know, that seems unreasonable because… for the most concrete reason, at NDSS I met a guy, Kevin Milner… He was like, “Hey that looks cool. Have you ever heard of formal verification? Have you ever used Tamarin?”
I said, “I have never used Tamarin.” And then we sat down at the conference and he showed me how to use Tamarin. And then a few months later I was hanging out with him up at Oxford and, you know, banging out the first proof for WireGuard. There you go. Had I not gone to NDSS in the first place, that never would have happened.
And since then, formal verification now has just become part of my general flow of doing things. I think it’s an important tool without a doubt.
Why This Matters
Jason and Kevin’s meeting wasn’t planned. It wasn’t a keynote. It was the kind of collision of minds that only occurs when brilliant people gather in the same room to discuss their work and think deeply.
To be Captain Obvious here: Because Jason came to NDSS, he learned how to mathematically prove his software was secure. This helped elevate WireGuard from a weekend project to a global standard for Internet security.
At the Internet Society, we invest in events like NDSS not just for the content presented on stage, but also for the lasting communities they create (such as our Fellowship Program and alumni), and for the conversations that result – whether at NDSS or later on.
Keeping these forums open, accessible, and vibrant requires resources. If your organization wants to support an environment where the next serendipitous security moment can occur, we are currently seeking sponsorship partners for our upcoming symposium.
Joseph Lorenzo Hall is a Distinguished Technologist at the Internet Society, where his work lies at the intersection of computer science, law, and policy. He leads programs focused on online trust and safety, as well as an open and trustworthy Internet, advocating for policy, technology, and commercial decisions that prioritize people’s safety, security, and privacy.
Photo by Wes Hardaker.