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.

翻译：我们引入了一种用于推理网络地址的上下文信任的逻辑，为其提供了克里普克语义，并在关于主体策略的合理假设下证明了其可靠性。自我认证传统地址（SATAs）是有效的DNS地址或URL，它们通常对人类和网络基础设施都具有意义，并且在地址本身中包含对公钥的承诺。目前，网络地址的信任是通过域名注册、TLS证书以及互联网基础设施的其他层级元素建立的。SATA支持此类结构性信任根源，同时也支持与描述性属性相关的补充性上下文信任根源。现有的结构性信任根源使网络连接容易受到多种有据可查且影响重大的劫持漏洞的影响。上下文信任根源则提供了更强的抵御此类漏洞的能力。我们还考虑了带标签的SATA，这些标签包含描述性属性，例如某个SATA是新闻机构的地址、属于特定政府或公司的网站、提供特定主题信息的网站等。我们的逻辑既涉及对地址绑定身份的信任，也涉及对标签绑定于该地址的信任。该逻辑允许推理关于指定标签的信任委托、提供更多或更少具体信息的标签之间的关系，以及这两个方面之间的相互作用。除了可靠性之外，我们还证明：如果某个主体信任特定的身份（可能带有标签），那么要么这种信任是初始假设的，要么存在一条从初始信任假设出发到该信任的委托信任链。我们还提出了一种算法，能够有效地从初始信任假设集合中推导出所有可能的信任陈述，并证明该算法是可靠、完备且可终止的。