Formal Modeling and Verification for Domain Validation and ACME

Abstract : Web traffic encryption has shifted from applying only to highly sensitive websites (such as banks) to a majority of all Web requests. Until recently, one of the main limiting factors for enabling HTTPS is the requirement to obtain a valid certificate from a trusted certification authority, a tedious process that typically involves fees and ad-hoc key generation, certificate request and domain validation procedures. To remove this barrier of entry, the Internet Security Research Group created Let's Encrypt, a new non-profit certificate authority which uses a new protocol called Automatic Certificate Management Environment (ACME) to automate certificate management at all levels (request, validation , issuance, renewal, and revocation) between clients (website operators) and servers (certificate authority nodes). Let's Encrypt's success is measured by its issuance of over 12 million free certificates since its launch in April 2016. In this paper, we survey the existing process for issuing domain-validated certificates in major certification authorities to build a security model of domain-validated certificate issuance. We then model the ACME protocol in the applied pi-calculus and verify its stated security goals against our threat model of domain validation. We compare the effective security of different domain validation methods and show that ACME can be secure under a stronger threat model than that of traditional CAs. We also uncover weaknesses in some flows of ACME 1.0 and propose verified improvements that have been adopted in the latest protocol draft submitted to the IETF.
Type de document :
Rapport
[Research Report] INRIA Paris; Microsoft Research Cambridge. 2016
Liste complète des métadonnées

https://hal.inria.fr/hal-01397439
Contributeur : Nadim Kobeissi <>
Soumis le : dimanche 9 décembre 2018 - 12:12:28
Dernière modification le : mardi 11 décembre 2018 - 01:16:15
Document(s) archivé(s) le : dimanche 10 mars 2019 - 13:16:43

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01397439, version 3

Collections

Citation

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Nadim Kobeissi. Formal Modeling and Verification for Domain Validation and ACME. [Research Report] INRIA Paris; Microsoft Research Cambridge. 2016. 〈hal-01397439v3〉

Partager

Métriques

Consultations de la notice

53

Téléchargements de fichiers

82