SoSySec seminar
Software and Systems Security
Inria - Rennes
May 12th, 2023, 11:00
In-person: Turing-Petri
Remotely with BBB:https://bbb.inria.fr/all-t0p-qjq-9em / Access code: 192737
----------------------------------------------------------------------
Sylvain Ruhault (ANSSI)
----------------------------------------------------------------------
======================================================================
A new symbolic analysis of WireGuard VPN
======================================================================
WireGuard is a new Virtual Private Network (VPN), recently integrated into the Linux Kernel and in OpenBSD. It proposes a different approach from other classical VPN such as IPsec or OpenVPN because it does not let users configure cryptographic algorithms but instead relies on a close set of preconfigured algorithms. The protocol inside WireGuard is a dedicated extension of IKpsk2 protocol from Noise Framework. WireGuard and IKpsk2 protocols have gained a lot of attraction from the academic community and different analyses have been proposed, in both the symbolic and the computational model, with or without computer-aided proof assistants. These analyses however consider different adversarial models or refer to incomplete versions of the protocols. Furthermore, when proof assistants are used, protocol models also differ. In this work, we propose a new, unified formal model of WireGuard protocol in the symbolic model. Our model is fully based on processes in the applied Pi-Calculus, the language used by the automatic cryptographic protocol verifier Sapic+. It allows us to automatically generate translations into ProVerif and Tamarin proof assistants. We consider a complete protocol execution, including cookie messages used for resistance against denial of service attacks. Furthermore, we model an adversary that can read or set static, ephemeral or pre-shared keys, read or set ECDH precomputations, control key distribution. Eventually, we present our results in a unified and interpretable way, allowing comparisons with previous analyses. This is joint work with Dhekra Mahmoud and Pascal Lafourcade.
----------------------------------------------------------------------
To follow the presentation remotely, please connect to the following URL with a modern web browser:
- URL:https://bbb.inria.fr/all-t0p-qjq-9em
- Access code: 192737
----------------------------------------------------------------------
Seminar taking place in person with mandatory registration at least 48h beforehand for *all* in-person participants by email to Nadia Derouault<nadia [*] derouault
inria [*] fr>. Participants non-affiliated with Inria or IRISA will be asked to present an ID at the reception desk of the IRISA building.
To receive the SoSySec announcements, please subscribe to the SoSySec mailing list:
https://sympa.inria.fr/sympa/subscribe/sosysec
All past and future SoSySec talks are listed at
https://seminaires-dga.inria.fr/en/seances-a-venir/
----------------------------------------------------------------------
Séminaire en présentiel ouvert à tous mais avec inscription obligatoire au moins 48h à l'avance pour *tous* les participants en présentiel auprès de Nadia Derouault<nadia [*] derouaultinria [*] fr>.
Les participants externes devront se présenter à l'accueil avec une pièce d'identité.
Vous pouvez vous abonner à nos annonces de séminaires :
https://sympa.inria.fr/sympa/subscribe/sosysec
et consulter la liste des exposés passés et à venir :
https://seminaires-dga.inria.fr/seances-a-venir/