Skip to Main content Skip to Navigation

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.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Nadim Kobeissi <>
Submitted on : Sunday, December 9, 2018 - 12:12:28 PM
Last modification on : Tuesday, December 11, 2018 - 1:16:15 AM
Long-term archiving on: : Sunday, March 10, 2019 - 1:16:43 PM


Files produced by the author(s)


  • HAL Id : hal-01397439, version 3



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⟩



Record views


Files downloads