Source-linked AI summary
Accountability in Certificate Transparency and Variants
Timo Treitz, Robert Künnemann
TL;DR
Certificate Transparency replaces a simple CA trust assumption with a distributed protocol whose accountability properties are difficult to characterize precisely. The paper models CT and its extensions in Tamarin, finding that plain CT requires an honest log, SCT Auditing can remove that assumption for audited certificates, and Gossiping cannot.
Problem
Existing CT analyses use simplified models or design-specific definitions, leaving unclear how CT’s CA, logger, monitor, and client checks establish accountability.
Method
The paper incrementally models vanilla PKI, CT, SCT Auditing, and Gossiping in the Dolev-Yao model using automated Tamarin accountability analysis.
Results
Plain CT provides accountable authenticity with trusted logs and monitors, while SCT Auditing can hold loggers and CAs accountable without trusting logs for audited certificates; Gossiping does not remove the log trust assumption.
Takeaways & Limitations
CT supplies accountability under explicit trust conditions, but stronger guarantees depend on audit coverage and introduce privacy or centralization trade-offs.
Takeaways & Limitations
The model does not cover certificate revocation, and SCT Auditing provides its strong guarantee only for randomly audited certificates from opted-in Chrome clients.
Abstract
from arXiv · showhide
Certificate Transparency (CT) aims to reduce the trust required in Certificate Authorities (CAs) within the TLS certificate ecosystem. It is supported by all major browsers. The protocol obliges all CAs to record the certificates they issue in a public log, which itself is monitored for compliance and consistency by third parties. Given this complex set of checks between the four roles-CA, loggers, monitor but also the end user's client-it is very hard to provide a precise account of how CT eliminates trust assumptions in exchange for complex infrastructure. Analyses both in the Dolev-Yao paradigm and the computational paradigm only regard a very simplified model and feature definitions adapted specifically to CAs, essentially capturing design features rather than the target property. The present paper posits accountability as the main goal of CT and presents a thorough analysis in the Dolev-Yao model. We start with the vanilla PKI and, step by step, move to CT, finally analyzing proposed extensions for SCT Auditing and Gossiping. We show that plain CT relies on an honest log, but provides accountability under this assumption. Furthermore, we show that the SCT Auditing extension can eliminate this assumption, while the Gossiping extension cannot.
1 Introduction
The paper treats accountability—identifying and attributing certificate misbehavior—as CT’s central goal and formally analyzes whether CT supplies sufficient evidence for it.
- Accountability is proposed as CT’s key property: misbehavior should be identified and correctly attributed to responsible parties.
- The paper applies automated Tamarin analysis in the Dolev-Yao model to CT, modeling CA, logger, and monitor corruption scenarios.
- The model formally checks that all responsible parties are blamed and no innocent party is blamed when authenticity is violated.
- The analysis proceeds incrementally from vanilla PKI to CT and then proposed SCT Auditing and Gossiping extensions.
2 Certificate Transparency Protocol
CT adds logs, monitors, and SCT-based evidence to the PKI, but its transparency remains vulnerable to logger misbehavior and depends on browser-specific policies and extensions.
- CT adds logs that maintain append-only Merkle trees and monitors that continuously inspect them for rogue certificates.
- An SCT promises that a certificate and its verification chain will be included in a log within the Maximum Merge Delay, typically up to 24 hours.
- CT does not prevent malicious CAs from issuing rogue certificates, but makes issuance transparent and detectable when logs do not collude with the CA.
- Known attacks and their detection.: Malicious logs can equivocate through partition attacks or omit certificates despite issuing SCTs, while inclusion checks can expose omission attacks but may reveal browsing interests.
- SCT Auditing.: SCT Auditing lets a dedicated monitor compare user-submitted SCTs against log inclusion, whereas browser implementations use constrained trusted-log and SCT policies.
3 Background
The paper models protocol execution and accountability with Tamarin’s multiset rewriting framework, using trace-based tests to identify parties responsible for property violations.
- 3.1.1 Multiset Rewriting (MSR).: Tamarin represents protocol states as multisets of facts and protocol behavior as rules that rewrite premises into conclusions while emitting actions.
- 3.1.1 Multiset Rewriting (MSR).: Executions are chains of rewrites, and traces record rule actions that support first-order security-property reasoning over terms and time points.
- 3.2 Accountability: Accountability requires CT to determine both whether a property was violated and which parties jointly caused the violation through protocol deviations.
- 3.2 Accountability: Tamarin tests use unbound party variables so matching traces identify blamed parties, including multiple parties when a violation requires collusion.
- 3.2 Accountability: The accountability decomposition checks sufficiency, verifiability, minimality, and uniqueness of blame assignments.
4 The Standard PKI
The standard PKI places trust in certificate authorities and can violate authenticity when a CA or root CA misbehaves. External validation enables accountability, but shifts trust to a validator that must be trusted and online.
- Accountability: External validation provides accountable authenticity by identifying the responsible intermediate or root CA, but requires a trusted validator that is always online.The validator distinguishes incorrect certificate fields and assigns blame through the certificate chain and documented intermediate CAs.
- Validation model: PKI validation relies on certificate chains, signature checks, and certificate validity periods before a browser accepts a chain.The model represents certificates as signed 7-tuples and checks signatures, trusted roots, and expiration.
- Security goal: The authenticity goal requires every browser-accepted certificate statement to match ground truth previously established for the CA and fields.The paper uses this lemma as a template for accountability properties in CT and its extensions.
- Security result: A corrupt signing CA or misbehaving root CA can construct a rogue certificate, refuting unconditional authenticity.Tamarin identifies both corruption scenarios; excluding them yields a refined authenticity result.
- Accountability: Accountability applies only to fields that were actually checked, creating an implicit liveness assumption for the checking party.The paper notes that accountability depends on an active party triggering the relevant check.
5 Certificate Transparency
Certificate Transparency distributes validation across logs and monitors using SCT commitments and proof-based log inspection. Plain CT provides accountable authenticity when logs are trusted, but dishonest loggers can hide rogue certificates and defeat accountability.
- CT infrastructure: CT certificates embed two SCTs from distinct logs, while monitors inspect logs and use inclusion and append-only proofs to detect rogue certificates.The model represents SCT issuance, log commitments, visibility after the maximum merge delay, and proof verification.
- Log modeling: The model encodes log operations and Merkle-tree proof properties axiomatically to support multiple ledgers, maximum merge delay, inclusion proofs, and append-only proofs.This avoids explicitly modeling Merkle trees, which the paper says does not scale as well.
- Accountable authenticity: A corrupt logger can hide a rogue certificate from an honest monitor, so plain CT may fail both CA accountability and verifiability.The counterexample shows that the monitor cannot produce a nonempty blame set when the relevant log entry is omitted.
- Accountable authenticity: Plain CT provides accountable authenticity against untrusted CAs only when both the monitor and logs are trusted.With trust only in the monitor, a corrupt logger can hide a certificate and prevent blame assignment.
- Transparency: Transparency fails for dishonest loggers because they can equivocate across different log views, while honest logs provide transparency only after the maximum merge delay.This motivates treating logger accountability as a separate problem.
6 SCT Auditing
SCT Auditing strengthens CT accountability by letting monitors validate logged certificates and hold dishonest loggers accountable, but it still relies on a trusted monitor with ground truth.
- SCT Auditing Mechanism: Clients can upload encountered SCTs and certificate chains to a monitor, enabling inclusion and authenticity checks against known ground truth.The mechanism is opt-in, so its guarantees apply to participating clients rather than universally.
- Accountable Authenticity: SCT Auditing provides accountable authenticity against untrusted loggers and CAs when the monitor is trusted.The monitor can identify misbehaving CAs and audit logger inclusion behavior.
- Limitations: Without trusting the monitor, a monitor can receive a rogue certificate and ignore it, defeating the audit.The model therefore identifies monitor behavior as an unresolved accountability dependency.
- Accountable Authenticity: SCT Auditing mitigates malicious loggers hiding entries, with detection probability 1 − (1 − p)^n when n rogue certificates reach clients auditing with probability p.This probabilistic guarantee applies per audited certificate.
- Accountable Transparency: SCT Auditing can hold loggers accountable for missing entries and provide accountable transparency, but the monitor remains trusted.The monitor obtains an external STH, performs inclusion checks, and blames a logger when the certificate is absent.
- Holding the Monitor Accountable With Receipts: Receipt-based auditing extends accountability to corrupted CAs, loggers, and monitors, but the authors do not present it as a finalized proposal.Clients can require signed monitor receipts and domain owners can use them to detect monitor misbehavior.
7 STH Gossiping
STH gossiping lets monitors compare log snapshots and detect equivocation, but it does not provide accountable authenticity against untrusted loggers because monitors lack the actual certificate context.
- Gossiping Mechanism: Gossiping clients share STHs with a monitor, which verifies append-only consistency and reuses CT authenticity checks on retrieved log entries.The model assumes clients have checked inclusion and that sufficiently many clients participate.
- Gossiping Mechanism: Gossiping prevents partition attacks on participating clients by requiring a logger to hide an entry from every gossiping client it contacts.Direct browser-to-user communication is considered impractical, so the analyzed design sends STHs to a monitor.
- Accountable Authenticity: A malicious logger can evade accountable authenticity by sending a valid certificate first and later presenting a refutable inclusion proof for a different snapshot.The monitor can blame the logger for the failed proof but cannot determine whether the CA caused an authenticity violation.
- Transparency: A logger can still break transparency to the monitor by refusing to disclose entries behind a client-verified STH and equivocating.The monitor can detect this when it additionally checks the append-only property.
- Transparency: STH gossiping achieves accountable transparency but not transparency when loggers and CAs are untrusted and the monitor is trusted.The monitor checks whether its latest snapshot is append-only relative to a client-gossiped STH.
8 Results
The formal results characterize when CT provides authenticity, transparency, and accountability, showing that transparency is essential unless a logger is trusted. SCT auditing strengthens guarantees for audited certificates, while other browser support remains limited.
- Results: All 192 rule-reachability lemmas were proved automatically, with total verification time below two hours for these sanity checks.The complete automated analysis across sanity, accountability, transparency, and helping lemmas took around five hours, with partial manual intervention for six lemmas.
- Results: A client accepting a certificate with two SCTs implies that both referenced loggers added entries unless one logger is corrupt.The corresponding authenticity lemmas also establish that two distinct loggers honestly issued SCTs when a CA asserts the certificate.
- Results: Transparency is essential for accountable authenticity unless the logger is trusted, and full certificates are needed to hold CAs accountable.SCTs can hold loggers accountable for omissions, while SCT auditing covers both CAs and loggers; STH gossiping cannot correctly blame CAs.
- Results: SCT auditing provides strong transparency and accountable authenticity only for certificates that are actually audited.Chrome audits only a randomized portion of certificates in practice, and other browsers do not implement SCT auditing or client-side inclusion proofs.
- Results: Current CT deployments still rely on trusted loggers because browsers require two SCTs from pools of seven or eight loggers.Under the stated browser parameters, at least six or seven loggers must be trusted or non-colluding.
9 Related Work
Prior CT analyses use manual cryptographic games or simplified automated models, while this work adopts a broader accountability notion and a more detailed protocol model. The comparison highlights improved coverage of protocol roles and Merkle-proof behavior.
- Related Work: Prior work modeled accountability through a complex, protocol-specific cryptographic game that is difficult to adapt beyond its original setting.That game encodes PKI-specific concepts and does not clearly establish accountability in a broader sense.
- Related Work: Earlier accountability definitions identify some responsible parties but do not ensure that every responsible party is blamed or that blamed parties truly caused the violation.The paper’s accountability definition is designed to ensure both soundness of blame and completeness of identifying causes.
- Related Work: The paper extends prior CT modeling with a broader, more realistic model covering dishonest intermediary and root CAs, loggers, monitors, and Merkle proofs.Earlier models simplified browser validation and monitoring or omitted inclusion and append-only proofs.
- Related Work: SCT auditing was previously modeled as identifying loggers responsible for missing transparency, whereas this paper analyzes it within a broader CT model.Earlier work characterized this property as audited transparency.
10 Conclusion
The paper concludes that CT shifts accountability from CAs toward loggers but still depends on logger trust in its ordinary form. SCT auditing removes that trust for audited certificates, whereas STH gossiping does not achieve accountable authenticity.
- 10 Conclusion: Plain CT can hold CAs accountable through logged certificates and chains, but corrupt loggers can hide evidence and preserve a trust dependency.An honest monitor knowing the ground truth can identify maliciously issued certificates when the relevant evidence remains visible.
- 10 Conclusion: SCT auditing removes the log from the trust assumption and can hold misbehaving loggers and CAs simultaneously accountable for audited certificates.In practice, auditing is randomized, requires Chrome opt-in, and shares certificates with one trusted Google monitor.
- 10 Conclusion: STH gossiping provides accountable transparency but not accountable authenticity because it can identify logger misbehavior without exposing CA signatures.It also adds inclusion-proof cost and was deprecated without implementation.
- 10 Conclusion: The model does not cover certificate revocation, although integrating revocation proofs into CT logs is considered future work.The paper describes postcertificates and similar log entries as possible approaches.
- 10 Conclusion: The analysis is defense-focused and specification-level, with no experiments conducted on living subjects.Its stated impact is clarifying CT guarantees and structural changes that may improve transparency and accountability, potentially with network overhead.
D.3 Log Data Structure
The log model represents each logger’s ledger through trace actions, visibility predicates, and controllable snapshots, capturing honest operation, corruption, proofs, and merge delays. It also distinguishes visible certificate entries from visible certificate chains.
- D.3 Log Data Structure: The model represents log additions and proof generation as trace actions, with restrictions enforcing ledger relations and permitting Merkle inclusion and append-only properties.Each operation carries an identifier for the specific log snapshot being represented, allowing malicious loggers to equivocate.
- D.3 Log Data Structure: Honest loggers accept pre-certificates with complete chains to known roots, issue SCTs, and add the pre-certificate and chain to the public log.The model’s SCT promise is computed over pre-certificate fields, so logger liability is limited to those fields rather than the complete chain.
- D.3 Log Data Structure: The log exposes append-only behavior, SCT inclusion, and entry validity as properties that participants can check.Entry validity requires a valid pre-certificate with a full chain ending in a trusted root.
- D.3 Log Data Structure: Corrupted loggers can create arbitrary forged log entries without possessing a valid pre-certificate chain.The model adds corruption rules that permit manipulation of log entries and forged SCTs.
- D.3 Log Data Structure: Visibility predicates model maximum merge delay by making scheduled additions visible only after a later time interval.The predicates separately track entry visibility, chain visibility, and the absence of a visible chain; inclusion alone does not guarantee chain validity or existence.
- D.3 Log Data Structure: Chain visibility lets monitors distinguish a visible pre-certificate from a visible certificate chain needed to identify the responsible CA.If a monitor verifies a found chain itself, the model guarantees discovery of a rogue certificate with a valid chain when such a chain exists in the log.
D.6 Fetching proofs and snapshots
The model abstracts log snapshots and proofs while structuring snapshot retrieval as a three-step exchange between fetchers and loggers. It uses secure, session-identified communication and explicitly limits adversarial replay of proofs.
- D.6 Fetching proofs and snapshots: Inclusion and append-only proofs are represented as abstract trace properties rather than computed cryptographic proofs.The model treats the proofs as symbolic variables and checks whether they would succeed for the log snapshot at the relevant time.
- D.6 Fetching proofs and snapshots: Snapshot fetching begins with a proof request, followed by the logger returning a current snapshot and the recipient checking the relevant property.The model distinguishes honest loggers from corrupted ones, which may return snapshots for maintained or forged logs.
- D.6 Fetching proofs and snapshots: Fresh session identifiers bind each proof run to its request and support temporal restrictions, such as requiring a request after receipt of an SCT.The connection is not persistent, so new requests receive different session identifiers.
- D.6 Fetching proofs and snapshots: The abstraction assumes secure proof handling and logger compliance when presenting snapshots, while malicious behavior is modeled separately.The logger-compliance assumption is relaxed for gossiping, where only the Signed Tree Head is shared rather than all underlying entries.
D.7 Inclusion Proof
The inclusion-proof model determines whether a certificate entry was visible in the logger’s supplied snapshot, while append-only checks compare stored snapshots for disappearing entries. The analysis also exposes accountability limits caused by proof replay and unobservable monitor behavior.
- D.7 Inclusion Proof: An inclusion proof succeeds when the queried entry is visible in the logger’s snapshot at the time that snapshot is handed out.A failed proof requires an earlier logger-presented view in which the entry was missing.
- D.7 Inclusion Proof: Proof requests, returned snapshots, and checks are linked by ordered trace events and session identifiers, allowing the model to distinguish valid from invalid proof outcomes.The formal restrictions require the logger’s view to precede the check and connect the relevant snapshot facts.
- D.7 Inclusion Proof: Append-only verification checks that entries visible in an older snapshot remain visible in a later snapshot, with one disappearing entry sufficient to witness a violation.The model stores retrieved snapshots and evaluates the property across them.
- D.7 Inclusion Proof: CT lacks a mechanism for a separate party to determine whether a monitor intentionally ignored a rogue certificate or never saw it.This prevents direct accountability for monitor misbehavior without additional evidence.
- D.7 Inclusion Proof: Monitor receipts address this gap by proving that a monitor saw a specific certificate chain, enabling tests that can blame corrupted monitors while preserving CA accountability.The receipt is a monitor signature over the received chain and monitor identifier, sent through a TLS channel.
E.1 Accountability Analysis
The accountability analysis extends monitor evidence with signed receipts and tests gossiping-based consistency checks. Receipts support accountable authenticity against corrupted monitors, whereas gossiping requires additional append-only checks to compare views.
- E.1 Accountability Analysis: A receipt proves to the logger or another holder that a monitor saw a specific log snapshot, supporting probabilistic monitor checking and cross-monitor validation.The receipt is issued by the monitor after receiving the audited certificate chain.
- E.1 Accountability Analysis: Signed monitor receipts enable tests that blame monitors which deliberately ignored rogue certificates, yielding accountable authenticity even with corrupted monitors.The construction combines receipt checks with earlier tests that can blame corrupted CAs.
- E.1 Accountability Analysis: The receipt approach assumes the domain owner can obtain the receipt, but routing it to the correct web server is not straightforward because that routing itself involves authenticity.The authors discuss clients forwarding receipts and domain owners acting as clients for probabilistic checks.
- E.1 Accountability Analysis: SCT Auditing assumes a powerful monitor that can access all certificates eventually seen by clients, limiting the direct applicability of self-run or independent monitors.The section notes that increasing domain-owner complexity may reduce the need for a distinct monitor, but the auditing model retains this access assumption.
- E.1 Accountability Analysis: In gossiping, only one of the relevant log views is shared, so a monitor must perform an append-only proof between the gossiped and locally fetched snapshots.The model relaxes the assumption that both snapshots were handed directly to the monitor.
- E.1 Accountability Analysis: The gossiping restrictions detect a violation when an entry visible in a gossiped snapshot is absent from the monitor’s later logger view.The formal rule records the two views and asserts the append-only violation between them.