  We introduce a logic for reasoning about contextual trust for web addresses,
provide a Kripke semantics for it, and prove its soundness under reasonable
assumptions about principals' policies.
  Self-Authenticating Traditional Addresses (SATAs) are valid DNS addresses or
URLs that are generally meaningful -- to both humans and web infrastructure --
and contain a commitment to a public key in the address itself. Trust in web
addresses is currently established via domain name registration, TLS
certificates, and other hierarchical elements of the internet infrastructure.
SATAs support such structural roots of trust but also complementary contextual
roots associated with descriptive properties. The existing structural roots
leave web connections open to a variety of well-documented and significant
hijack vulnerabilities. Contextual trust roots provide, among other things,
stronger resistance to such vulnerabilities.
  We also consider labeled SATAs, which include descriptive properties such as
that a SATA is an address for a news organization, a site belonging to a
particular government or company, a site with information about a certain
topic, etc. Our logic addresses both trust in the bound together identity of
the address and trust in the binding of labels to it. Our logic allows
reasoning about delegation of trust with respect to specified labels,
relationships between labels that provide more or less specific information,
and the interaction between these two aspects.
  In addition to soundness, we prove that if a principal trusts a particular
identity (possibly with label), then either this trust is initially assumed, or
there is a trust chain of delegations to this from initial trust assumptions.
We also present an algorithm that effectively derives all possible trust
statements from the set of initial trust assumptions and show it to be sound,
complete, and terminating.
