Home > Research > Publications & Outputs > An In-Depth Symbolic Security Analysis of the A...


Text available via DOI:

View graph of relations

An In-Depth Symbolic Security Analysis of the ACME Standard

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

  • Karthikeyan Bhargavan
  • Abhishek Bichhawat
  • Quoc Huy Do
  • Pedram Hosseyni
  • Ralf Küsters
  • Guido Schmitz
  • Tim Würtele
Publication date13/11/2021
Host publicationCCS 2021 - Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security
Place of PublicationNew York
Number of pages17
ISBN (electronic)9781450384544
<mark>Original language</mark>English


The ACME certificate issuance and management protocol, standardized as IETF RFC 8555, is an essential element of the web public key infrastructure (PKI). It has been used by Let's Encrypt and other certification authorities to issue over a billion certificates, and a majority of HTTPS connections are now secured with certificates issued through ACME. Despite its importance, however, the security of ACME has not been studied at the same level of depth as other protocol standards like TLS 1.3 or OAuth. Prior formal analyses of ACME only considered the cryptographic core of early draft versions of ACME, ignoring many security-critical low-level details that play a major role in the 100 page RFC, such as recursive data structures, long-running sessions with asynchronous sub-protocols, and the issuance for certificates that cover multiple domains. We present the first in-depth formal security analysis of the ACME standard. Our model of ACME is executable and comprehensive, with a level of detail that lets our ACME client interoperate with other ACME servers. We prove the security of this model using a recent symbolic protocol analysis framework called DYg, which in turn is based on the Fg programming language. Our analysis accounts for all prior attacks on ACME in the literature, including both cryptographic attacks and low-level attacks on stateful protocol execution. To analyze ACME, we extend DYĝ with authenticated channels, key substitution attacks, and a concrete execution framework, which are of independent interest. Our security analysis of ACME totaling over 16,000 lines of code is one of the largest proof developments for a cryptographic protocol standard in the literature, and it serves to provide formal security assurances for a crucial component of web security.