A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol

Autor: Karthikeyan Bhargavan, Benjamin Lipp, Bruno Blanchet

Publikováno v: 4th IEEE European Symposium on Security and Privacy
4th IEEE European Symposium on Security and Privacy, Jun 2019, Stockholm, Sweden. pp.231-246
[Research Report] RR-9269, Inria Paris. 2019, pp.49
2019 IEEE European Symposium on Security and Privacy (EuroS&P)
EuroS&P
[Research Report] RR-9269, Inria Paris. 2019, pp.50

WireGuard is a free and open source Virtual Private Network (VPN) that aims to replace IPsec and OpenVPN. It is based on a new cryptographic protocol derived from the Noise Protocol Framework. This paper presents the first mechanised cryptographic pr

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f49d39ec103b1f78fd4c66e001d7ecef
https://hal.inria.fr/hal-02396640/document

Composition Theorems for CryptoVerif and Application to TLS 1.3

Autor: Bruno Blanchet

Publikováno v: [Research Report] RR-9171, Inria Paris. 2018, pp.67
31st IEEE Computer Security Foundations Symposium (CSF'18)
31st IEEE Computer Security Foundations Symposium (CSF'18), Jul 2018, Oxford, United Kingdom. ⟨10.1109/CSF.2018.00009⟩
CSF

We present composition theorems for security protocols, to compose a key exchange protocol and a symmetric-key protocol that uses the exchanged key. Our results rely on the computational model of cryptography and are stated in the framework of the to

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::04e9a68ea969c147b670ce8a7b56eb95
https://hal.inria.fr/hal-01764527

Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate

Autor: Bhargavan, Karthikeyan, Blanchet, Bruno, Kobeissi, Nadim

Publikováno v: [Research Report] RR-9040, Inria Paris. 2017, pp.51

TLS 1.3 is the next version of the Transport Layer Security (TLS) protocol. Its clean-slate design is a reaction both to the increasing demand for low-latency HTTPS connections and to a series of recent high-profile attacks on TLS. The hope is that a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______212::4b557fa6901220e5d55b52fcb23cd3eb
https://hal.inria.fr/hal-01528752

Implémentations de protocoles cryptographiques prouvées dans le modèle calculatoire

Autor: Cadé, David

Publikováno v: Cryptography and Security [cs.CR]. Paris 7, 2013. English
Cryptography and Security [cs.CR]. Paris 7, 2013. English. ⟨NNT : ⟩

The goal of this work is to obtain implementations of security protocols proved in the computational model. We implemented a compiler that takes as input a specification of a protocol in the input language of the protocol verifier CryptoVerif and com

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::c0d43a0d7d1a98bf7b2ff79c137371c3
https://hal.inria.fr/tel-01112630

Modèles vérifiés et implémentations de référence pour le candidat standard TLS 1.3

Autor: Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet

Publikováno v: HAL
[Research Report] RR-9040, Inria Paris. 2017, pp.51
IEEE Symposium on Security and Privacy
2017 IEEE Symposium on Security and Privacy (SP)
38th IEEE Symposium on Security and Privacy
38th IEEE Symposium on Security and Privacy, May 2017, San Jose, United States. pp.483-502, ⟨10.1109/SP.2017.26⟩

TLS 1.3 is the next version of the Transport Layer Security (TLS) protocol. Its clean-slate design is a reaction both to the increasing demand for low-latency HTTPS connections and to a series of recent high-profile attacks on TLS. The hope is that a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b42cad5e1d54818341cd1c3edf1667c8
https://hal.inria.fr/hal-01528752