Threshold Trust Logic

Distributed processes, such as multi-party computations and collaborative product pipelines, require many entities. To formulate formal guarantees of such processes involves the gathering and evaluation of claims of the entities involved. We consider a formal logic in which modalities are used to mark the channel in which such claims are made, specifying their source and target. Formally, we see each channel as some domain of knowledge, containing both literal claims and their consequences. We can combine such channels to express whether claims were made independently by different channels, or collaboratively by pooling claims from different channels. Together, this allows us to formulate more complex combinations we call threshold channels. We can use this logic to find out which sources need to be trusted, and which targets will have received sufficient claims, in order to prove a particular guarantee. The paper is split into two parts. First, we formulate and investigate the formal properties of a modal logic expressing threshold channels. Second, we consider how to apply this to reasoning about threshold claims for distributed processes.