An In-Depth Symbolic Security Analysis of the ACME Standard

Karthikeyan Bhargavan; Abhishek Bichhawat; Quoc Huy Do; Pedram Hosseyni; Ralf Kuesters; Guido Schmitz; Tim Wuertele

Paper 2021/1457

An In-Depth Symbolic Security Analysis of the ACME Standard

Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Kuesters, Guido Schmitz, and Tim Wuertele

Abstract

he 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 DY* , which in turn is based on the F* 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.

Note: Additional information (such as our ACME model and the DY* framework) is available at https://reprosec.org

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Published elsewhere. Minor revision. CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security Proceedings
DOI: 10.1145/3460120.3484588
Keywords: applications digital signatures implementation public-key cryptography certificates
Contact author(s): karthikeyan bhargavan @ inria fr
abhishek b @ iitgn ac in
quoc-huy do @ sec uni-stuttgart de
pedram hosseyni @ sec uni-stuttgart de
ralf kuesters @ sec uni-stuttgart de
guido schmitz @ sec uni-stuttgart de
tim wuertele @ sec uni-stuttgart de
History: 2021-11-06: received
Short URL: https://ia.cr/2021/1457
License: CC BY

BibTeX

@misc{cryptoeprint:2021/1457,
      author = {Karthikeyan Bhargavan and Abhishek Bichhawat and Quoc Huy Do and Pedram Hosseyni and Ralf Kuesters and Guido Schmitz and Tim Wuertele},
      title = {An In-Depth Symbolic Security Analysis of the {ACME} Standard},
      howpublished = {Cryptology {ePrint} Archive, Paper 2021/1457},
      year = {2021},
      doi = {10.1145/3460120.3484588},
      url = {https://eprint.iacr.org/2021/1457}
}