1. 3

  2. 3

    Here’s my post from the mailing list, on the paper:

    Two researchers – Ben Dowling and Kenny Paterson, who you might know from their work on Signal and TLS 1.3, among other research areas – have written up a by-hand game hopping proof in the computational model of the WireGuard protocol. The paper is worth a read; the findings are very interesting.

    One design goal of WireGuard is to simplify the state machine as much as possible, by keeping the handshake portion of the protocol as only two messages – there (message 1) and back (message 2) – so that if something goes wrong, the state machine can just start over at the beginning again, without having to take into account intermediate states. The original WireGuard paper [1] writes that after the initiator receives message 2 from the responder, the initiator must send the first transport data message to the responder, not the other way around, to act as a handshake confirmation message. By putting the confirmation message as part of the transport layer, it means that any transport message that arrives will suffice as confirmation, as opposed to relying on a special handshake-layer message, which could be dropped (we’re UDP remember), thereby complicating the state machine. This is a fairly nifty trick that allows us to write simpler and more reliable implementations, and it’s specified as part of how the Noise Protocol Framework [2] works.

    It turns out, however, that traditional computational security models, such as the eCK model used in this paper, were designed for a different era of protocols, where the handshake was one thing, and the transport was another, and different handshakes could be put together with different transports, in a nicely stackable fully modular way. Certainly IPsec-era protocols, for example, were interested in this kind of layer-separation – IKE is a good example. These computational security models simply don’t take into account what it means when a transport message is used as an essential part of ensuring the handshake security properties.

    Other protocols have had similar traits – TLS 1.2, for example – and researchers came up with a different security model called ACCE [3], in order to prove (or disprove!) things about them. But generally speaking, the go-to model for researchers interested in trying to do computational proofs is eCK.

    Thus, Dowling and Paterson tried to fit the verbatim protocol into this computational model, and were not able to, due to WireGuard’s reliance on the first transport message as part of its handshake properties (which we consider a feature, not a bug). Fortunately, the authors didn’t stop there. They then went on to modify their description of the WireGuard protocol to put that confirmation message essentially as part of the handshake layer, which would not be feasible for real WireGuard, but is a sufficiently interesting modification to prove things about. Finally, they showed that that modified construction is secure.

    I interpret this as further positive confirmation of WireGuard and the Noise Protocol Framework, as it is easy to argue that their modified WireGuard protocol – which fits into their security model – is “morally equivalent” to the real WireGuard protocol. I also look forward to advancements in the tools and models available to computational proof researchers.

    Enjoy the papers!