Modal Logic for Distributed Trust

Niels Voorneveld; Peeter Laud

cs.LOMar 23, 2026

Modal Logic for Distributed Trust

Authors: Niels Voorneveld, Peeter Laud

Organizations: Cybernetica AS

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.

Figures & tables

Axiom	Name
$\vdash\mathcal{M}A\Rightarrow\mathcal{M}(A\Rightarrow B)\Rightarrow\mathcal{M}B$	Axiom K
If $\vdash A$ then $\vdash\mathcal{M}A$	Necessity
$\vdash\mathcal{B}_{a}A\Rightarrow\mathcal{B}_{a}\mathcal{B}_{a}A$	Self awareness
$\vdash\mathcal{I}_{a\scalebox{0.5}[0.75]{$ \leftarrow $}b}A\Rightarrow\mathcal{B}_{a}\mathcal{I}_{a\scalebox{0.5}[0.75]{$ \leftarrow $}b}A$	Recipient awareness
$\vdash\mathcal{I}_{a\scalebox{0.5}[0.75]{$ \leftarrow $}b}A\Rightarrow\mathcal{I}_{a\scalebox{0.5}[0.75]{$ \leftarrow $}b}\mathcal{B}_{b}A$	Intent of claim
If $a\sqsubseteq b$ then $\vdash\mathcal{B}_{a}A\Rightarrow\mathcal{B}_{b}A$	Belief inheritance

Figure 1: Axiom system.

\mathcal{M}

ranges over modalities,

a

b

over agents, and

A

B

over formulas.

\frac{}{\Gamma,A\vdash A}\qquad\frac{}{\Gamma\vdash\top}\qquad\frac{\Gamma\vdash\bot}{\Gamma\vdash A}\qquad\frac{\Gamma\vdash A\qquad\Gamma\vdash A\Rightarrow B}{\Gamma\vdash B}\qquad\frac{\Gamma,A\vdash B}{\Gamma\vdash A\Rightarrow B}\qquad\frac{\Gamma\vdash A\wedge B}{\Gamma\vdash A}\qquad\frac{\Gamma\vdash A\wedge B}{\Gamma\vdash B}

Figure 2: Intuitionistic Multi-Modal K Logic

Property	Name
$\vdash\widehat{\mathcal{M}}A\wedge\mathcal{M}A\Rightarrow A$	Validity definition
$\vdash A\Rightarrow\widehat{\mathcal{M}}A$	Validity unit
$\vdash\widehat{\mathcal{M}}A\wedge\widehat{\mathcal{M}}B\Rightarrow\widehat{\mathcal{M}}(A\wedge B)$	Merging validities
$\vdash\widehat{\mathcal{M}}\mathcal{N}A\wedge\widehat{\mathcal{N}}A\Rightarrow\widehat{\mathcal{M}\mathcal{N}}A$	Composition rule 1
$\vdash\mathcal{M}\widehat{\mathcal{N}}A\wedge\widehat{\mathcal{M}}A\Rightarrow\widehat{\mathcal{M}\mathcal{N}}A$	Composition rule 2
$\vdash\mathcal{M}\widehat{\mathcal{N}}A{\wedge}\widehat{\mathcal{M}}\widehat{\mathcal{N}}A{\wedge}\widehat{\mathcal{M}}\mathcal{N}A{\Rightarrow}\widehat{\mathcal{M}\mathcal{N}}A$	Composition rule 3

Figure 3: Validity properties (Derivable in the logic)

\frac{[\Delta]=\varepsilon}{\Gamma,x:A,\Delta\vdash\texttt{var}(x):A}\qquad\frac{}{\Gamma\vdash*:\top}\qquad\frac{\Gamma\vdash P:\bot}{\Gamma\vdash\texttt{abs}_{A}(P):A}\qquad\frac{\Gamma,\{\mathcal{M}\}\vdash P:A}{\Gamma\vdash\texttt{lock}_{\mathcal{M}}(P):\mathcal{M}A}

Figure 4: Fitch-style lambda calculus for our logic

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

\frac{}{\Gamma,t,\Delta\vdash t}(Var)\qquad\frac{\Gamma,A\vdash B}{\Gamma\vdash A\Rightarrow B}(ImpR)\qquad\frac{\Gamma,A\Rightarrow B\vdash A\qquad\Gamma,A\Rightarrow B,B\vdash D}{\Gamma,A\Rightarrow B\vdash D}(ImpL)

Appendix

Figure 5: Decidable Sequent Calculus

Multi-Agent Systems

Multi-Agent Systems studies how autonomous agents coordinate, compete, communicate, and learn in shared or interdependent tasks.

See all 677 papers

Trust-Gated Capability Control: Breaking the Trust-Vulnerability Paradox in Multi-Agent LLM Systems
Oct 4, 2026Mehedi Hasan Nipu, Chinmoy Mitra, Tarannum Ahmed Nowshin +1Trust in AI Multi-Agent System Security
Department of Electrical and Computer Engineering, North South University, Dhaka, Bangladesh · Department of Computer Science & Engineering Rajshahi University of Engineering & Technology Rajshahi, Bangladesh · Department of Computer Science and Engineering BRAC University,Dhaka, Bangladesh +1
Trust Between AI Agents: Measuring Formation, Breakage, and Recovery, with Implications for Governing Multi-Agent Systems
Jun 12, 2026Yujiao ChenAI Agent Evaluation Multi-Agent Systems
Massachusetts Institute of Technology Cambridge, MA 02139
Who Speaks, Who Authorizes, Who Acts? Understanding Trust Boundaries in Multi-Agent LLMs
Oct 16, 2026Junru Zhu, Xin Chen, Hang Lyu +6Multi-Agent LLM Systems AI Agent Security

Oct 4, 2026J/K move · Enter open · S save

Trust-Gated Capability Control: Breaking the Trust-Vulnerability Paradox in Multi-Agent LLM Systems

Mehedi Hasan Nipu, Chinmoy Mitra, Tarannum Ahmed Nowshin, Israt Moyeen Noumi

Department of Electrical and Computer Engineering, North South University, Dhaka, Bangladesh · Department of Computer Science & Engineering Rajshahi University of Engineering & Technology Rajshahi, Bangladesh · Department of Computer Science and Engineering BRAC University,Dhaka, Bangladesh+1

Trust in AI Multi-Agent System Security Multi-Agent LLM Systems Tool Access Control for LLM Agents Access Control

Open paper AskPDF arXiv

Layered trust models for multi-agent LLM systems remain largely conceptual: they name which dimensions of trust matter but not how layers combine, how their importance is set at runtime, or how trust should govern agent actions. This gap matters because higher inter-agent trust raises task success while also enlarging exposure to exploitation, a tension formalized as the Trust-Vulnerability Paradox. We make a five-layer trust stack operational through three contributions. First, a cross-layer synergy operator propagates prerequisite-layer deficits into de- pendent layers, feeding a generalized-mean composite trust that recovers the weakest-link rule as a limiting case, with provable bounds. Second, per-layer importance weights are grounded in observed failures via a no-regret online estimator that tracks which layer is currently most responsible for harm. Third, Trust- Gated Capability Control issues short-lived, revocable capability grants only when composite trust and the relevant prerequisite layers clear capability-specific thresholds. We prove this mechanism breaks the paradox: a stealthy compromise that inflates behavioral trust while degrading a prerequisite layer cannot escalate privilege, and give a closed-form, provably conservative trust fixed point with a bounded-latency revocation guarantee. A numerical study with a sleeper adversary confirms the predictions: composite-trust bounds hold across 20,000 random draws, the analytic fixed point matches simulation within 0.007, and a compromised prerequisite layer triggers automatic revocation within a few interactions.

Abstract

Multi-Agent Systems

Explore similar work

Trust-Gated Capability Control: Breaking the Trust-Vulnerability Paradox in Multi-Agent LLM Systems

Trust Between AI Agents: Measuring Formation, Breakage, and Recovery, with Implications for Governing Multi-Agent Systems

Who Speaks, Who Authorizes, Who Acts? Understanding Trust Boundaries in Multi-Agent LLMs