Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Modal Logic for Distributed Trust

Niels Voorneveld, Peeter Laud

Abstract

We propose a method for reasoning about trust in multi-agent systems, specifying a language for describing communication protocols and making trust assumptions and derivations. This is given an interpretation in a modal logic for describing the beliefs and communications of agents in a network. We define how information in the network can be shared via forwarding, and how trust between agents can be generalized to trust across networks. We give specifications for the modal logic which can be readily adapted into a lambda calculus of proofs. We show that by nesting modalities, we can describe chains of communication between agents, and establish suitable notions of trust for such chains. We see how this can be applied to trust models in public key infrastructures, as well as other interaction protocols in distributed systems.

Modal Logic for Distributed Trust

Abstract

We propose a method for reasoning about trust in multi-agent systems, specifying a language for describing communication protocols and making trust assumptions and derivations. This is given an interpretation in a modal logic for describing the beliefs and communications of agents in a network. We define how information in the network can be shared via forwarding, and how trust between agents can be generalized to trust across networks. We give specifications for the modal logic which can be readily adapted into a lambda calculus of proofs. We show that by nesting modalities, we can describe chains of communication between agents, and establish suitable notions of trust for such chains. We see how this can be applied to trust models in public key infrastructures, as well as other interaction protocols in distributed systems.
Paper Structure (44 sections, 31 theorems, 32 equations, 5 figures)

This paper contains 44 sections, 31 theorems, 32 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Constructive Modal Logic
  3. Distributed Trust and Decentralized Identity
  4. Misplaced Trust in Certificate Authorities
  5. Related Work
  6. Comparison to Authorization and Access Logics
  7. Contributions and Paper Outline
  8. Related papers:
  9. Modal Reasoning
  10. Optional hierarchy of agents
  11. Logical Foundation
  12. Decidability
  13. Chains of Communications
  14. Trust
  15. Indirect trust
  16. ...and 29 more sections

Key Result

Lemma 1

For any $\mathsf{Ax}$, the logics $\mathcal{L}_{\mathsf{Ax}}$ and $\mathcal{L}_{\widehat{\mathsf{Ax}}}$ are equivalent.

Figures (5)

  • Figure 1: Axiom system. $\mathcal{M}$ ranges over modalities, $a$, $b$ over agents, and $A$, $B$ over formulas.
  • Figure 2: Intuitionistic Multi-Modal K Logic
  • Figure 3: Validity properties (Derivable in the logic)
  • Figure 4: Fitch-style lambda calculus for our logic
  • Figure 5: Decidable Sequent Calculus

Theorems & Definitions (70)

  • Definition 1
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Example 1: A global view
  • Example 2: Trust and Responsiveness
  • Example 3: Communicating Trust
  • Example 4: Trusted Authority
  • Lemma 3
  • ...and 60 more