A Formal Model for ACME: Analyzing Domain Validation over Insecure Channels

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 :
[Research Report] INRIA Paris; Microsoft Research Cambridge. 2016
Liste complète des métadonnées

Contributeur : Nadim Kobeissi <>
Soumis le : mercredi 16 novembre 2016 - 11:08:06
Dernière modification le : vendredi 18 novembre 2016 - 01:10:35
Document(s) archivé(s) le : lundi 27 mars 2017 - 09:24:14


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01397439, version 2



Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Nadim Kobeissi. A Formal Model for ACME: Analyzing Domain Validation over Insecure Channels. [Research Report] INRIA Paris; Microsoft Research Cambridge. 2016. <hal-01397439v2>



Consultations de
la notice


Téléchargements du document