E02-TS: Yes
Rationale
Lipp, Blanchet and Bhargavan (INRIA, EuroS&P 2019) publish a mechanised cryptographic analysis of WireGuard handshake and transport messages, with public CryptoVerif models. The selected Tailscale data plane uses this protocol; its pinned wireguard-go dependency identifies Noise_IKpsk2_25519_ChaChaPoly_BLAKE2s. This is independent analysis of a selected security-critical protocol mechanism, not merely of a cipher primitive. E02 accepts bounded mechanism coverage, as already applied to TLS, QUIC and BPSec compositions.
Assessment method
Published third-party protocol analysis mapped to a pinned selected dependency; no proof rerun
Source context
Lipp, Blanchet and Bhargavan, EuroS&P 2019; author-hosted models and Tailscale wireguard-go e61b6b78110b
Outstanding qualification
Protocol-model analysis, not an audit of the current Tailscale fork, managed coordination, DERP, identity-provider enrollment or Tailnet Lock. Model assumptions and compromise cases remain relevant; no post-quantum or secret-PSK guarantee is credited to the selected no-additional-PSK profile. The authors report a Curve25519-model correction in their longer version and provide corrected model artifacts; the conference PDF is retained as historical analysis, not treated as an unqualified current security proof. Proof scripts were not rerun. The authors are distinct from the selected implementation team; the paper acknowledges discussion with the WireGuard designer, not independent certification of the complete product.
Public sources
- https://bblanche.gitlabpages.inria.fr/cryptoverif/WireGuard/
- https://bblanche.gitlabpages.inria.fr/publications/LippBlanchetBhargavanEuroSP19.pdf
- https://tailscale.com/docs/concepts/tailscale-encryption
- https://raw.githubusercontent.com/tailscale/wireguard-go/e61b6b78110b/device/noise-protocol.go
Editorial evidence references
The following identifiers refer to research records not included in this public package; they are not public links.
- round596.html
- round596-sources.json