An In-Depth Symbolic Security Analysis of the ACME Standard
| Autor: | Quoc Huy Do, Guido Schmitz, Abhishek Bichhawat, Karthikeyan Bhargavan, Pedram Hosseyni, Tim Würtele, Ralf Küsters |
|---|---|
| Přispěvatelé: | Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Indian Institute of Technology [Gandhinagar] ( IIT Gandhinagar ), Universität Stuttgart [Stuttgart] |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Security analysis
business.industry Computer science Public key infrastructure Cryptography Cryptographic protocol Internet security Computer security computer.software_genre [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Server Key (cryptography) business Protocol (object-oriented programming) computer ComputingMilieux_MISCELLANEOUS |
| Zdroj: | CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2601-2617, ⟨10.1145/3460120.3484588⟩ CCS |
| Popis: | 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 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|