[1]TU Berlin, Institute of Mathematics, Straße des 17. Juni 136, 10623 Berlin, Germany<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>[2]SatoshiPay GmbH, Mühlenstr. 8a, 14167 Berlin, Germany<EMAIL_ADDRESS>
We give an introduction to federated Byzantine agreement systems (FBAS) with many examples ranging from small “academic” cases to the current Stellar network. We then analyze the main concepts from a mathematical and an algorithmic point of view. Based on work of Lachowski <cit.> we derive algorithms for quorum enumeration, checking quorum intersection, and computing the intact nodes with respect to a given set of ill-behaved (Byzantine) nodes. We also show that from the viewpoint of the intactness probability of nodes, which we introduce in this paper, a hierarchical setup of nodes
is inferior to an arrangement that we call a symmetric simple FBAS. All algorithms described in this paper are implemented in the Python package Stellar Observatory[<https://github.com/andrenarchy/stellar-observatory>], which is also used in some of the computed examples.

§ INTRODUCTION

The main idea of blockchain technology is to maintain a distributed ledger in a decentralized way. This means that the ledger is replicated among a set of different parties or nodes, and no central entity has the authority on the content of the ledger <cit.>.
Transactions included in the ledger are recorded in blocks which point to previous blocks, thus forming a chain of blocks.
Nodes need to reach consensus (see, e.g., <cit.> or <cit.>) on the next block in order to be included in the chain despite facing arbitrary (Byzantine) failures of some nodes such as going offline or proposing an invalid block.
Consequently, every blockchain system requires an underlying consensus model, which ideally is based on a thorough mathematical formalization and analysis.

In this paper we study a consensus model introduced by Mazières in 2016 <cit.>, the federated Byzantine agreement system (FBAS), which is used in the Stellar[<https://www.stellar.org>] Consensus Protocol (SCP). The main practical advantages of the SCP in comparison with other consensus mechanisms like proof-of-work or proof-of-stake with the longest chain rule, or classical Byzantine agreement are discussed in detail in <cit.> and in <cit.>.

The nodes of an FBAS conceptually form a network, where the links between the nodes are established by trust decisions that are made by each node individually, and hence in a decentralized way. A subset of nodes that a given node “trusts” is called a quorum slice, and each node may have several such slices. A quorum of the FBAS is a set of elements which contains at least one quorum slice for each of its members, and hence may be interpreted as a subset of nodes that “trusts itself”. In order to avoid that contradictory statements are ratified, the quorums need to be pairwise intersecting. The quorum intersection property and several other concepts in the context of the FBAS lead to challenging mathematical and computational problems which so far have not been fully addressed in the literature. Our goal in this paper is contribute to the overall understanding of FBAS by giving a thorough mathematical introduction to the main ideas and concepts, in particular the quorum intersection problem and the intactness of nodes. We will also treat these problems in detail from an algorithmic point of view.

The paper is organized as follows: In Section <ref> we give the FBAS definition of Mazières and illustrate it with several examples. We then introduce and analyze the trust graph of an FBAS and derive a mathematical description of the current Stellar network. In Section <ref> we show that the quorum intersection decision problem is NP-complete. A similar result was recently shown by Lachowski <cit.>, but here we show NP-completeness even when we restrict the decision problem to the class of simple FBAS (see Definition <ref>). We then discuss algorithms for quorum enumeration and checking quorum intersection. The main ideas of these algorithms also appeared in the work of Lachowski <cit.>, and some have been implemented in Stellar Core[<https://github.com/stellar/stellar-core>], the “backbone” of the Stellar network. Based on these previous works, we give an in-depth treatment of both algorithms.

In Section <ref> we analyze the intactness of nodes, characterize the intact nodes in symmetric simple FBAS, and compare the original intactness definition of Mazières with newer definitions given in <cit.>. In Section <ref> we treat intactness algorithmically, and based on results from Section <ref>, we derive an algorithm for computing the intact nodes when a set of ill-behaved (Byzantine) nodes is given. The time complexity of this algorithm is (only) twice as long as determining quorum intersection. Finally, in Section <ref> we look at intactness from a probabilistic point of view, and we study the probability that a node is intact in different scenarios of ill-behaved nodes.

§ FEDERATED BYZANTINE AGREEMENT SYSTEMS

In this section we first review the basic definition and give some simple examples of federated Byzantine agreement systems, then discuss their relationship to certain graphs, and finally derive a mathematical description of the current Stellar network.

§.§ Basic definitions and examples

We start with the following definition, originally given by Mazières <cit.>.

A federated Byzantine agreement system (FBAS) is a pair $(V,S)$ consisting of a finite set of nodes $V$ and a quorum function $S:V\to {\mathcal P}({\mathcal P}(V)) \setminus \{\emptyset\}$, where for each $v\in V$ and $s\in S(v)$ we require that $v\in s$. Each set $s\in S(v)$ is called a quorum slice of the node $v$.

A nonempty set of nodes $Q\subseteq V$ is called a quorum in $(V,S)$ if for each $v\in Q$ there exists a quorum slice $s\in S(v)$ with $s\subseteq Q$.

Note that we require that $S(v)\not=\emptyset$ for every node $v$. Therefore $Q=V$ is a quorum in $(V,S)$, so that each FBAS has at least one quorum. Also note that if $Q_1,Q_2$ are quorums, then $Q_1\cup Q_2$ is a quorum as well.

In a more recent paper on Stellar as a global payment network, the authors define a quorum to be “a non-empty set of nodes encompassing at least one quorum slice of each non-faulty member” <cit.>. In contrast to Definition <ref>, this definition of quorums includes the individual behavior of the nodes (which is unknown a priori and uncontrollable). In this paper we will focus on the FBAS as originally defined by Mazìeres, and thus consider the individual node behavior only later, when defining the concept of intactness (see Definition <ref>). A comparison of the original and the new concepts is given in Section <ref>. We stress that in the analysis of consensus mechanisms it is very important to pay great attention to details. Already Lamport, Shostak and Pease in their classical paper on the Byzantine generals problem from 1982 “strongly advise the reader to be very suspicious of ... nonrigorous reasoning” and write that they “know of no area in computer science or mathematics in which informal reasoning is more likely to lead to errors than in the study of this type of algorithm” <cit.>.

A quorum slice $s\in S(v)$ is interpreted as a subset of the nodes that the node $v$ “trusts”. The set $S(v)$ should be chosen so that $v$ will agree with any statement that is unanimously agreed upon by any of the slices. A quorum $Q$ of the FBAS again is a subset of the nodes, where for each element $v\in Q$ at least one of its quorum slices (i.e., at least one subset of “trusted” nodes) is completely contained in $Q$ as well. Thus, a quorum is a set of nodes that “trusts itself”. In practice quorums are not known a priori but discovered by the nodes when exchanging messages. Each node sends its quorum slices with every message. A receiving node considers a message to satisfy a quorum when the set of the sending nodes contains a quorum slice of each of its elements.

In a nutshell (see <cit.> for details), a quorum $Q$ ratifies a statement if every node $v\in Q$ asserts that this statement is true. Consensus means that two contradicting statements should not be ratified at the same time. Thus, the quorums of the FBAS should pairwise intersect, which naturally leads to the following concept introduced by Mazières <cit.>.

An FBAS $(V,S)$ has quorum intersection if any two of its quorums have a nonempty intersection.

Note that quorum intersection is not guaranteed without further assumptions. Moreover, the decision problem whether quorum intersection holds is NP-complete; see Section <ref> below for details. As described in <cit.>,
within Stellar Core the quorum intersection property of the underlying FBAS is regularly checked with an algorithm based on an idea of Lachowski <cit.>, which we will analyze in detail in Sections <ref> and <ref>.

If $Q_1,\dots,Q_m$ are the quorums of an FBAS $(V,S)$ with quorum intersection, then $(V, \{Q_1,\dots,Q_m\})$ is a (classical) quorum system. Such systems have been studied since the late 1970s in the context of distributed computing; see, e.g., the monograph <cit.> for an overview. The quorum system $(V,\{Q_1,\dots,Q_m\})$ therefore may be analyzed using the concepts introduced in this area, including load, capacity, and availability; see, e.g., <cit.>. A detailed analysis of the relationship between FBAS and classical Byzantine quorum systems was recently given in <cit.>.

Let us give a few examples of federated Byzantine agreement systems.

Let $V=\{1,\dots,n\}$ for some $n\geq 2$.

(1) Let $S(i)=\{\{i\}\}$ for $i=1,\dots,n$. Then every nonempty subset $Q\subseteq V$ is a quorum, since for every node $i$ its only quorum slice is given by $\{i\}$, and we trivially have $\{i\}\subseteq Q$. Clearly, $(V,S)$ does not have quorum intersection.

(2) Let $S(i)=\{V\}$ for $i=1,\dots,n$. Now $Q=V$ is the only quorum and $(V,S)$ has quorum intersection.

Consider $V=\{1,\dots,n\}$ for some $n\geq 2$ and $S(i)=\{\{i,j\}\mid j=1,\dots,n,\,j\neq i\}$ for $i=1,\dots,n$. Let $U\subseteq V$ be any subset containing at least two nodes. If we take any two nodes from $U$, say $\ell$ and $m$ with $\ell\neq m$, then $\{\ell,m\}\in S(\ell)$ and $\{\ell,m\}\in S(m)$, which shows that $U$ is a quorum. If $n\geq 4$, then $(V,S)$ does not have quorum intersection, since, e.g., $\{1,2\}$ and $\{3,4\}$ are quorums.

[Byzantine agreement]
This example shows that classical Byzantine agreement can be modeled as a special FBAS.

Let $V=\{1,\dots,n\}$ for some $n=3m+1$, where $m\in\N$, and suppose that for $i=1,\dots,n$, each quorum slice $s\in S(i)$ contains at least $2m+1$ nodes (including $i$). Then any quorum of the FBAS $(V,S)$ must consist of at least $2m+1$ nodes, and since there are exactly $3m+1$ nodes, any two quorums must intersect in at least $m+1$ nodes. If $m$ nodes in the intersection become Byzantine, i.e., behave arbitrarily, then there still is at least one non-Byzantine node in each intersection, which guarantees that the quorums cannot ratify contradictory statements. And, as shown in a classical paper of Lamport, Shostak, and Pease, “no solution with fewer than $3m+1$ generals can cope with $m$ traitors” <cit.>; also cf. Theorem <ref> below.

Consider $V=\{1,\dots,7\}$ and $S$ with

\begin{align*}
S(i)&=\{\{1,2,3,7\}\},\; i=1,2,3,\qquad S(i)=\{\{4,5,6,7\}\},\;i=4,5,6\;,
\end{align*}

and $S(7)=\{\{7\}\}$. This FBAS $(V,S)$ has exactly four quorums,

\begin{align*}
\{1,2,3,7\},\quad\{4,5,6,7\},\quad\{7\},\quad V,
\end{align*}

and it has quorum intersection. Note that node $7$ is contained in every quorum, and that the minimal intersection of two quorums consists only of this node.

Suppose that the FBAS is built by 4 organizations $A,B,C,D$, which have 3 nodes each, i.e., $V=A\cup B\cup C\cup D$ with

\begin{align*}
\end{align*}

Suppose that the quorum slices of each node $x_i$, $i=1,2,3$, are all sets consisting of the three nodes of its own organization $X$, and exactly one node from another organization, i.e.,

$$S(x_i)=\{X\cup \{y\}\mid y\in V\setminus X\}.$$

Then each node has 9 quorum slices containing 4 nodes each, and $(V,S)$ does not have quorum intersection, since $A\cup B$ and $C\cup D$ are quorums.

[hierarchical quorum slices]
Suppose that the FBAS is built by 6 organizations, $V=A\cup B\cup C\cup D\cup E\cup F$ with

\begin{align*}
\end{align*}

and suppose that the quorum slices are built in a hierarchical way: We form all possible subsets of $V$ by first choosing 5 of the 6 sets $A,B,C,D,E,F$, and then in each of the 5 chosen sets we choose either 2 of the 3 nodes in case of the sets $A,B,C,D,E$, or 3 of the 5 nodes in case of set $F$. Thus, each of these subsets contains either 10 or 11 nodes, depending on whether on the “root level” of the hierarchy the set $F$ is chosen or not. In total there are 4293 such subsets, and we denote the union of all these sets by $\underline{S}$.

We define the quorum function by

$$S(v)=\{U\in \underline{S}\mid v\in U\},\quad v\in V,$$

then each node in the sets $A,B,C,D,E$ has 2322 quorum slices, and each node in the set $F$ has 2430 quorum slices. This results in 37888 quorums and we have quorum intersection, with the minimal size of an intersection given by 4 nodes.

As shown by the examples above, the definition of the FBAS allows quite intricate systems of quorum slices and resulting quorums. We will now introduce special FBAS classes that are of some practical relevance and can be analyzed more easily than the general case. The idea of these classes is that the quorum slices of each node are given by all possible subsets of a fixed cardinality that can be drawn from a certain fixed subset of the nodes.

An FBAS $(V,S)$ is called simple when there exist functions $q: V \rightarrow {\mathcal P}(V)$ and $n: V\rightarrow \N$, such that for each node $v\in V$ we have $v\in q(v)$, $1\leq n(v)\leq |q(v)|$, and

$$S(v)=\{U\subseteq q(v)\mid v\in U\;\mbox{and}\;|U| = n(v)\}.$$

We denote a simple FBAS by $(V, q, n)$. A simple FBAS is called symmetric when for all $v\in V$ we have $q(v)=V$ and $n(v)=k$ for some fixed $k$, where $1\leq k\leq |V|$, and we denote such an FBAS by $(V,k)$.

Note that Example <ref>(1) is a simple FBAS with $q(v_i)=\{v_i\}$ and $n(v_i)=1$, Example <ref>(2) is a symmetric simple FBAS with $k=n$, and Example <ref> is a symmetric simple FBAS with $k=2$.

Let $(V,k)$ be a symmetric simple FBAS. Then the set of all quorums is given by $\{Q\subseteq V\,\mid\,|Q|\geq k\}$, and the FBAS has quorum intersection if and only if $k>|V|/2$.

It is easy to see that $\{Q\subseteq V\,\mid\,|Q|\geq k\}$ is the set of all quorums, since
for each node $v\in V$ its quorum slices are given by all subsets of $V$ containing exactly $k$ elements (including $v$ itself). If $k\leq |V|/2$, then there exist two disjoint quorums. On the other hand, if $k>|V|/2$, then the pigeonhole principle implies that the quorums are pairwise intersecting.

§.§ The trust graph

It is tempting to think of and to visualize the network of relationships that is represented by an FBAS as a conventional directed graph, where the vertices are given by the elements of $V$, and an edge between $v_i$ and $v_j$ exists when $v_j$ is contained in a quorum slice of $v_i$. While in general there is no one-to-one correspondence between directed graphs and FBAS, the representation of an FBAS by a directed graph is a useful tool for their analysis because it describes the network of trust.

The trust graph of the FBAS $(V,S)$ is the directed graph $G=(V,E)$, where for every $u,v\in V$ we have $(u,v)\in E$ if
$v\in s$ for some $s\in S(u)$.

For every $u,v\in V$ we say that $v$ is reachable from $u$ if there is a path from $u$ to $v$ in $G$. We say that a set $U\subseteq V$ is strongly connected in $G$ if for every $u,v\in U$ the node $u$ is reachable from $v$. Furthermore, we say that a nonempty set $C\subseteq V$ is a strongly connected component (abbreviated SCC) of $G$ if it is strongly connected and no proper superset of $C$ is strongly connected.

Note that due to the last condition, whenever $C$ is an SCC and there is a node $v\in V$ such that every node in $C$ is reachable from $v$, and $v$ is reachable from every node in $C$, then $v\in C$. The following result follows directly from the transitivity of the reachability relation.

If $C$ and $D$ are SCCs, then the following hold:

* $C=D$ or $C\cap D=\emptyset$.

* Let $c\in C$ and $d\in D$ be such that $d$ is reachable from $c$. Then every node in $D$ is reachable from every node in $C$.

The first statement of Lemma <ref> implies that the set of SCCs form a partition of $V$ into disjoint nonempty subsets. The second statement implies that the following notion of reachability of SCCs is well-defined and is a partial order on SCCs.

Let $C$ and $D$ be SCCs. We say that $D$ is reachable from $C$ if there are $c\in C$ and $d\in D$ such that $d$ is reachable from $c$. We say that an SCC is maximal if no other SCC is reachable from it. We say that an SCC is the greatest SCC if it is reachable from every other SCC.

[Continuation of Example <ref>]
The strongly connected components of the FBAS of Example <ref> are $\{1,2,3\}$, $\{4,5,6\}$ and $\{7\}$; see Figure <ref>, which also shows how the reachability relation carries over to the SCCs. Note that the SCC $\{7\}$ is the only maximal SCC and also the greatest SCC.

level distance = 1.25cm,
edge_style/.style=draw=orange, line width=2, ultra thick,
bi_dir_e/.style=edge from parent/.style=<->,>=stealth',draw]

[node] (7) 7;
[circle, draw=black, fit=(7), dashed] (q3) ;

[node, below right= 6mm and 19mm of q3] (2) 2
child[bi_dir_e] node [node] (1) 1
child[bi_dir_e] node [node] (3) 3;
[<->,>=stealth'] (1) – (3);

[node, below left= 6mm and 19mm of q3] (5) 5
child[bi_dir_e] node [node] (4) 4
child[bi_dir_e] node [node] (6) 6;
[<->,>=stealth'] (4) – (6);

[circle, draw=black, fit=(1) (2) (3), dashed, below right=6mm and 10mm of q3] (q2) ;
[circle, draw=black, fit=(4) (5) (6), dashed, below left=6mm and 10mm of q3] (q1) ;
[->,>=stealth'] (q1) – (q3);
[->,>=stealth'] (q2) – (q3);

The strongly connected components of the FBAS from Example <ref>.

The following result follows from the finiteness of the set $V$.

There is at least one maximal SCC. If there is only one maximal SCC, then it is the greatest SCC. The greatest SCC is also maximal.

Let us now introduce a generalization of maximal SCCs.

A set $Z\subseteq V$ is called a trust cluster of $(V,S)$ if it is closed under reachability in $G$, i.e., if for every $u\in Z$ and $v\in V$ reachable from $u$, also $v\in Z$.

A set $Z\subseteq V$ is a trust cluster if and only if it is the union of strongly connected components that are closed under reachability. In particular, every maximal SCC is a trust cluster.

If a node $v$ is in a trust cluster, then the cluster contains every node that $v$ trusts transitively. Moreover, we have the following basic properties.

Let $Z$ be a trust cluster of $(V,S)$.

* $(Z, S|_Z)$ is a well-defined FBAS, where $S|_Z$ is the restriction of $S$ to $Z$.

* Every quorum of $(Z, S|_Z)$ is also a quorum of $(V,S)$.

* $Z$ is a quorum of $(V,S)$.

(1) Let $v\in Z$. Then every quorum slice of $v$ is contained in $Z$, i.e., $S(v)\subseteq \mathcal P(Z)$ or, equivalently, $S(v)\in \mathcal P(\mathcal P(Z))$.

(2) Follows from the equality $S|_Z(v)=S(v)$ for every $v\in Z$.

(3) By (2) and the fact that $Z$ is a quorum of $(Z, S|_Z)$.

Note that Lemma <ref> also applies if $Z$ is a maximal or the greatest SCC because of Lemma <ref>.

§.§ The Stellar network

Stellar Core

uses hierarchical quorum slices, but the construction is more sophisticated than in Example <ref>. In order to describe this construction we need the following definition, which is based on a rooted tree.

A quorum slice definition $d=(t,N,C)$ consists of a threshold $t\in\mathbb{N}$, a set of nodes $N$, and a set of children definitions $C$, which satisfy the following conditions:

* Each child $c\in C$ is a quorum slice definition and the recursively induced graph is a rooted tree with root $d$ and a finite number of vertices.

* For two vertices $(t_1,N_1,C_1)\neq(t_2,N_2,C_2)$ of the induced tree, the nodes do not intersect, i.e., $N_1\cap N_2=\emptyset$.

* $0\leq t \leq |N| + |C|$.

For describing how a quorum slice definition is translated to quorum slices we need the following definitions.

For a finite set $M$ and an integer $k\leq |M|$ we define the $k$-subsets of $M$ by $\mathcal{P}_k(M)=\{N\subseteq M\mid |N|=k\}\subseteq \mathcal P(M)$.

For sets of sets $M_1,\ldots,M_k$ we define their product set union by

\begin{align*}
\cup_\times(M_1,\ldots,M_k)
&=\{m_1\cup\cdots\cup m_k\mid (m_1,\ldots,m_k)\in M_1\times\ldots\times M_k\}\\
&\subseteq \mathcal P\left( \bigcup (M_1\cup \cdots \cup M_k)\right).
\end{align*}

Let $d=(t,N,C)$ be a quorum slice definition with threshold $t$, nodes $N=\{n_1,\ldots,n_l\}$, and children definitions $C=\{c_1,\ldots,c_m\}$. The quorum slices $s(d)$ are generated recursively with the following set of $l+m$ quorum slices sets

by considering all $t$-subsets of $B_{N,C}$ and reducing them to a single set of quorum slices with the product set union:

$$s(d)=\bigcup \{\cup_\times (M_1,\ldots,M_t) \mid \{M_1,\ldots M_t\}\in \mathcal{P}_t(B_{N,C})\}.$$

Note that the above recursion is well-defined and finite because the tree has by definition a finite number of vertices and thus leaf vertices, i.e., where the set of children definitions is empty.

In Stellar Core a quorum slice definition is transformed with respect to the node it is running so that the node itself is always contained in the generated quorum slices. For a formal description we also need the following definition.

Let $d=(t,N,C)$ be a quorum slice definition and let $v$ be a node. The quorum slice definition with $v$ removed is defined by

$$ R_v(d)=
\begin{cases}
(t-1,N\setminus \{v\},C),&\text{if $v\in N$},\\
(t,N,\{R_v(c)\mid c\in C\}),&\text{otherwise}.
\end{cases}

A Stellar Core instance running on node $v$ that is given a quorum slice definition $d$ actually uses the quorum slice definition $(2,\{v\},\{R_v(d)\})$.

[Stellar network]
The current Stellar network
consists of 20 nodes in its greatest SCC (see Definition <ref>), which are run by 6 organizations[Network transitive quorumset taken from <https://stellarbeat.io> on Nov. 7, 2019.].
The nodes are $V=A\cup B\cup C\cup D\cup E\cup F$ with

\begin{align*}
\end{align*}

The base quorum slice definition is

Thus, all quorum slices need to cover 5 organizations, and within each organization two nodes must be present (except for $F$, which requires three nodes to be present). The quorum slices of $v\in V$ are given by

where $d_v=(2,\{v\},\{R_v(d)\})$ is the transformed quorum slice definition with $v$ moved to the top level.

The nodes in $V\setminus F$ have 3132 quorum slices and the nodes in $F$ have 2673 quorum slices.

A computation in Stellar Observatory shows that the FBAS $(V,S)$ has 114688 quorums, and it has quorum intersection with the minimal size of an intersection given by 4 nodes.

§ ALGORITHMIC TREATMENT OF QUORUMS

In this section we will first show that the quorum intersection decision problem is NP-complete, and we will then discuss algorithms for enumerating the quorums of a given FBAS and for deciding whether an FBAS has quorum intersection.

§.§ Checking quorum intersection is NP-complete

Lachowski <cit.> showed that the problem of deciding whether a given FBAS $(V,S)$ has two disjoint quorums (Disjoint Quorums Problem) is NP-complete. His proof relies on a polynomial-time reduction from the NP-complete Set Splitting Problem <cit.> to the Disjoint Quorums Problem. Given an instance of the Set Splitting Problem (a family $F$ of subsets of a given set $S$), his reduction builds an instance of the Disjoint Quorums Problem such that it is only possible to partition the set $S$ into subsets $S_1, S_2$ in a way that all elements of $F$ are split by this partition, if and only if there are disjoint quorums in the constructed FBAS.

Here we will show that the decision problem is NP-complete even if we restrict it to the class of simple FBAS; see Definition <ref>. In order to fix the terminology, we say that an FBAS $(V,S)$ has quorum split if there exist two disjoint quorums, and we let $\textsc{SimpleQuorumSplit}$ be the problem to decide whether a given simple FBAS does have quorum split.

SimpleQuorumSplit is NP-complete.

SimpleQuorumSplit is obviously in NP because it can be checked in polynomial time whether a set is a quorum (see Lemma <ref> below) and, therefore, whether two witness sets are indeed disjoint quorums.

It remains to show that SimpleQuorumSplit is NP hard. We provide a polynomial-time reduction of the 3-SAT <cit.> problem to SimpleQuorumSplit.
Consider an instance $\varphi = (l_1^1\vee l_1^2\vee l_1^3)\wedge \cdots \wedge (l_m^1\vee l_m^2\vee l_m^3)$ of 3-SAT, where the literals
$l_i^j$ are either variables or negated variables taken from the set $x_1, \ldots, x_r$ of variables. We construct a simple FBAS $(V, q, n)$ that has quorum split if and only if $\varphi$ is satisfiable. Let

\begin{align}
V &=\{\star\}\cup\{a_k, x_k, \neg x_k\mid 1\leq k\leq r\}\cup\{b_i, c_i^1, c_i^2, c_i^3\mid 1\leq i\leq m\},\nonumber\\
q(\star) &=\{\star\}\cup \{b_i\mid 1\leq i\leq m\}\;\mbox{and $n(\star)=m + 1$,}\label{proof:quorumsplit-np-def-star}\\
q(a_k) &=\{a_k,x_k,\neg x_k\}\;\mbox{and $n(a_k)=2$ for $1\leq k\leq r$},\label{proof:quorumsplit-np-def-ak}\\
q(l) &=\bigl\{l, a_{(k\bmod r)+1}\bigr\}\cup\bigl\{c_i^j\mid l_i^j = l, 1\leq i\leq m, 1\leq j\leq 3\bigr\}\; \mbox{and}\label{proof:quorumsplit-np-def-ql}\\
n(l)& =|q(l)|\;\mbox{for $1\leq k\leq r$ and $l\in\{x_k, \neg x_k\}$},\\
q(b_i) &=\{b_i, c_i^1, c_i^2, c_i^3\}\;\mbox{and $n(b_i)=2$ for
$1\leq i\leq m$,}\label{proof:quorumsplit-np-def-qb}\\
q(c_i^j) &=\{c_i^j, \star, a_1\}\; \mbox{and $n(c_i^j)=2$ for $1\leq i\leq m$
and $1\leq j\leq 3$.}\label{proof:quorumsplit-np-def-qc}
\end{align}

Obviously, $(V,q,n)$ is a valid simple FBAS and can be constructed in time polynomial in the size of $\varphi$. It remains to show that $(V, q, n)$ has quorum split if and only if $\varphi$ is satisfiable.

“$\Leftarrow$”: Suppose that $\varphi$ is satisfiable and let $\alpha:\{x_1, \ldots, x_r\}\rightarrow \{\mathit{true}, \mathit{false}\}$ be a variable assignment that satisfies $\varphi$.

\begin{align*}
L=\{x_k\mid \alpha(x_k)=\mathit{false},\; 1\leq k\leq r\}\cup\{\neg x_k\mid \alpha(x_k)=\mathit{true},\; 1\leq k\leq r\}
\end{align*}

be the literals that are false under $\alpha$. Consider the two sets

\begin{align*}
Q_1 &=\{a_k\mid 1\leq k\leq r\}\cup L\cup\{c_i^j\mid l_i^j\in L, 1\leq i\leq m, 1\leq j\leq 3\},\\
Q_2 &=\{\star\}\cup \{b_i\mid 1\leq i\leq m\}\cup\{c_i^j\mid l_i^j\not\in L, 1\leq i\leq m, 1\leq j\leq 3\}.
\end{align*}

Clearly, $Q_1$ and $Q_2$ are disjoint. Moreover, $Q_1$ and $Q_2$ are quorums of $(V,q,n)$ because for every $1\leq i\leq m, 1\leq j\leq 3$ and $1\leq k\leq r$ we have:

* $x_k\in L$ or $\neg x_k\in L$, and hence by (<ref>) either $\{a_k, x_k\}$ or $\{a_k, \neg x_k\}$ is a quorum slice of $a_k$ contained in $Q_1$,

* $q(l)\subseteq Q_1$ for every $l\in L$ by (<ref>), and therefore every quorum slice of $l$ is contained in $Q_1$,

* if $l_i^j\in L$, then $\{c_i^j, a_1\}$ is a quorum slice of $c_i^j$ contained in $Q_1$ by (<ref>),

* $\{\star, b_1, \ldots, b_m\}$ is a quorum slice of $\star$ contained in $Q_2$ by (<ref>),

* since $\alpha$ is a satisfying variable assignment for $\varphi$, there is a $1\leq j\leq 3$ such that $l_i^j\not\in L$; then $\{b_i, c_i^j\}$ is a quorum slice of $b_i$ contained in $Q_2$ by (<ref>),

* if $l_i^j\not\in L$, then $\{c_i^j, \star\}$ is a quorum slice of $c_i^j$ contained in $Q_2$ by (<ref>).

“$\Rightarrow$”: Let $Q_1$ and $Q_2$ be disjoint quorums in $(V, q, n)$. We construct a satisfying variable assignment $\alpha$ for $\varphi$.
First note that for every quorum $Q$ we have $\star\in Q$ or $a_1\in Q$, which follows from this list of observations:

* if $a_k\in Q$, then $x_k\in Q$ or $\neg x_k\in Q$ by (<ref>),

* if $x_k\in Q$ or $\neg x_k \in Q$, then $a_{(k\bmod r)+1}\in Q$ by (<ref>),

* if $b_i\in Q$, then $c_i^1\in Q$, $c_i^2\in Q$ or $c_i^3\in Q$ by (<ref>),

* if $c_i^j\in Q$, then $\star \in Q$ or $a_1\in Q$ by (<ref>).

Since $Q_1$ and $Q_2$ are disjoint, we assume without loss of generality that $a_1\in Q_1$ and $\star\in Q_2$. We immediately have $\{b_1, \ldots, b_m\}\subseteq Q_2$ due to (<ref>), and from the list of
observations above we derive that $\{a_1, \ldots, a_r\}\subseteq Q_1$ and that, for every $1\leq k\leq r$, there is an $l_k \in \{x_k, \neg x_k\} \cap Q_1$.

Now set $\alpha(x_k)=\mathit{true}$ if $l_k=\neg x_k$, and set $\alpha(x_k)=\mathit{false}$ if $l_k=x_k$. In order to show that $\alpha$ satisfies $\varphi$, it
suffices to show that for every $1\leq i\leq m$, there is a $1\leq j\leq 3$ such that $l_i^j$ is $\mathit{true}$ under $\alpha$. Since $Q_2$ is a quorum and $b_i\in Q_2$,
there is a $1\leq j\leq 3$ such that $c_i^j\in Q_2$ by (<ref>). We show that $l_i^j$ is $\mathit{true}$ under $\alpha$. Observe that $l_i^j\not\in Q_1$,
otherwise we would have $c_i^j\in Q_1$ as $Q_1$ is a quorum and due to (<ref>), contradicting $c_i^j\in Q_2$. There is a $1\leq k\leq r$ with $l_i^j=x_k$ or $l_i^j=\neg x_k$.
Then, $l_i^j\not=l_k$ as $l_k\in Q_1$, i.e., $l_k=\neg x_k$ if $l_i^j=x_k$, and $l_k=x_k$ if $l_i^j=\neg x_k$. By the definition of $\alpha$, $l_i^j$ is $\mathit{true}$ under $\alpha$.

In the following two subsections we will discuss algorithms for
enumerating the quorums of a given FBAS and for deciding whether
an FBAS has quorum intersection. These algorithms are based on the work of Lachowski <cit.>. Lachowski describes them only on a conceptual level which gives room for interpretation when implementing both algorithms. For this purpose we base our discussion additionally on the current implementation in Stellar Core[<https://github.com/stellar/stellar-core/blob/b30a7023e6b51843ac2d3763d04ef7f0ad56ad73/src/herder/QuorumIntersectionCheckerImpl.h>]. We remark that the original implementation of the quorum intersection algorithm in Stellar Core was erroneous[<https://github.com/stellar/stellar-core/issues/2267>]. The misinterpretation of Lachowski's account might be partially due to the fact that he merely gave a sketch of these algorithms. For these reasons our main purpose here is to give an in-depth and precise treatment of both algorithms.

§.§ Quorum enumeration

In order to describe the computational cost of the algorithms, we need to define a measure for the size of the input. For the purposes of this definition we distinguish between simple and general FBAS.

The slice size $\Vert v\Vert$ of a node $v$ is defined as

* $\Vert v\Vert = \sum\nolimits_{s\in S(v)}|s|$,
for a general FBAS $(V,S)$, and

* $\Vert v\Vert = |q(v)|$, for a simple FBAS $(V, q, n)$.

The size of an FBAS $F=(V,S)$ or $F=(V,q,n)$, respectively, is defined as $\Vert F\Vert =|V| + \sum_{v\in V}\Vert v\Vert$.

The most fundamental operation for all algorithms discussed in this section is to decide whether a given node has a quorum slice contained in a given subset of $V$, see function containsSlice in Figure <ref>.

Given $U\subseteq V$ and $v\in U$ the function containsSlice decides in time $O(\Vert v\Vert)$ whether $v$ has a quorum slice contained in $U$.

Figure <ref> defines the function containsSlice for general as well as for simple FBAS. The correctness of the former version is obvious. For the correctness of the latter version note that $U$ contains a slice of $v$ if and only if there are $n(v)$ nodes in $q(v)$ that are also in $U$ if and only if $q(v) \cap U$ has at least $n(v)$ elements.

The complexity follows from the fact that $s\subseteq U$ can be decided in time $O(|s|)$ and that $U\cap q(v)$ can be computed in time $O(|q(v)|)$.

2lcontainsSlice (for general FBAS)
2lInput: FBAS $(V, S)$; $U\subseteq V$; $v\in U$

2lOutput: whether $v$ has a quorum slice contained in $U$

1   for $s$ in $S(v)$

2       if $s\subseteq U$ return $\mathit{true}$

3   return $\mathit{false}$

2lcontainsSlice (for simple FBAS)
2lInput: simple FBAS $(V, q, n)$; $U\subseteq V$; $v\in U$

2lOutput: whether $v$ has a quorum slice contained in $U$

1   return $|U\cap q(v)|\geq n(v)$

Algorithm for the function containsSlice for both general and simple FBAS.

In the sequel we will not distinguish between general and simple FBAS anymore. To this end we will refer to any FBAS simply using the variable $F$. We can now use the function containsSlice to build more interesting algorithms, see Figure <ref>.

Given a nonempty set $U\subseteq V$ the function isQuorum decides in time $O(\Vert F\Vert)$ whether $U$ is a quorum of the FBAS $F$.

The correctness of isQuorum follows immediately from the definition of quorums. It requires time $O(\sum_{v\in U}\Vert v\Vert)\leq O(\Vert F\Vert)$ due to Lemma <ref>.

2lInput: FBAS $F$ with set of nodes $V$; $U\subseteq V$ nonempty

2lOutput: whether $U$ is a quorum in $F$

1   for $v$ in $U$

2       if not $\textsc{containsSlice}(F, U, v)$ return $\mathit{false}$

3   return $\mathit{true}$

2lInput: FBAS $F$ with set of nodes $V$; $U\subseteq V$, $W\subseteq U$ ($\emptyset$ by default)

2lOutput: greatest quorum $Q$ with $W\subseteq Q\subseteq U$ if it exists, $\emptyset$ otherwise

1   $U_1\leftarrow U$, $i\leftarrow 1$

2   repeat

3       $U_{i+1}\leftarrow\emptyset$

4       for $v$ in $U_i$

5           if $\textsc{containsSlice}(F, U_i, v)$

6               $U_{i+1}\leftarrow U_{i+1}\cup\{v\}$

7           else

8               if $v \in W$ return $\emptyset$

9       if $U_{i+1}=U_{i}$ or $U_{i+1}=\emptyset$ return $U_{i+1}$

10       $i\leftarrow i+1$

Algorithm for isQuorum and greatestQuorum.

Clearly the union of two quorums is again a quorum. Thus, if a set $U\subseteq V$ contains at least one quorum, then the union of all quorums contained in $U$ is again a quorum. This quorum is the greatest with respect to the subset relation among all quorums contained in $U$. The following lemma states that the greatest quorum contained in a set of nodes can be computed efficiently via the function greatestQuorum, see Figure <ref>. This function is slightly more general: given two sets $U\subseteq V$ and $W\subseteq U$ it determines the greatest quorum $Q$ with $W\subseteq Q\subseteq U$. Note that we specify this last argument $W$ to be the empty set by default whenever we do not provide it explicitly when calling greatestQuorum in other algorithms defined in the remainder of this paper.

Given sets $U\subseteq V$ and $W\subseteq U$ the function greatestQuorum decides whether there is a quorum $Q$ with $W\subseteq Q\subseteq U$ and, if so, computes the greatest such quorum in time $O(|V|\cdot \Vert F\Vert)$.

Observe that the $i$-th iteration of the loop in lines 2–10 constructs the set $U_{i+1}$. The construction is performed in lines 3–8. Whenever we refer to one of the sets $U_{i+1}$ in this proof, we refer to its final value that it attains after its construction.

First observe that $U_{i+1}\subseteq U_i$ for every $i$ by construction of $U_{i+1}$. Hence the loop in lines 2–10 will terminate in line 9 after at most $|U|\leq |V|$ iterations. By Lemma <ref> each iteration takes time $O(\sum_{v\in U_i}\Vert v\Vert + |U_i|)\leq O(\Vert F\Vert)$. This proves the time complexity of greatestQuorum.

The set returned by greatestQuorum is either empty or a quorum contained in $U$ because the condition $U_{i+1}=U_i$ on line 9 is equivalent to the condition that $\textsc{containsSlice}(F, U_i, v)$ returns $\mathit{true}$ for every $v\in U_i$ – compare with the function isQuorum. Furthermore, if the algorithm does not return the empty set in line 8, then it is easy to show by induction that $W$ is contained in every constructed $U_i$: (i) it is obvious for $U_1$ and (ii) for every $U_{i+1}$ and $v\in W$ the element $v$ is added to $U_{i+1}$ in line 6. We conclude that if the algorithm does not return the empty set, then it returns a quorum contained in $U$ that contains $W$.
Conversely, whenever $U$ does not contain a quorum that contains $W$, then greatestQuorum returns the empty set as expected.

Finally, let us consider the case that $U$ contains a quorum that contains $W$. Given an arbitrary quorum $Q$ with $W\subseteq Q\subseteq U$ we will show by induction that $Q\subseteq U_i$ for every constructed $U_i$ and that the algorithm does not return in line 8. This implies that greatestQuorum returns a quorum that is a superset of $Q$; since $Q$ is arbitrary, greatestQuorum returns even the greatest quorum in $U$ that contains $W$. Now let us carry out the inductive proof. Trivially, $Q\subseteq U_1=U$. Let $i$ with $Q\subseteq U_i$. For every $v\in Q$ there is a quorum slice of $v$ contained in $Q$ and therefore also in $U_i$ – hence, $v\in U_{i+1}$. We conclude $Q\subseteq U_{i+1}$.

Let us now consider an algorithm for enumerating all quorums of an FBAS. Note that every such algorithm has worst-case time complexity of at least $O(2^{|V|})$ because there can be exponentially many quorums. In fact, there are FBAS such that every nonempty subset of $V$ is a quorum; see Example <ref>.

We will show that quorums can be enumerated with polynomial-time delay using the function enumerateQuorums in Figure <ref>. This result is originally due to Lachowski <cit.>, but the algorithm we present here uses a more efficient approach than the one described in his proof  of <cit.>.

The function enumerateQuorums enumerates all quorums of an FBAS with time delay $O(|V|^2\cdot\Vert F\Vert)$.

It suffices to show that for every $U\subseteq V$ and $R\subseteq V\setminus U$, the function call $\textsc{traverseQuorums}(F, U, R)$ enumerates all quorums $Q$ of $F$ such that $U\subseteq Q\subseteq U\cup R$ with time delay $O(|V|^2\cdot\Vert F\Vert)$.

First let us prove the correctness of the algorithm by strong induction on $|R|$. Let $U\subseteq V$ and $R\subseteq V\setminus U$ and suppose that the correctness of traverseQuorums holds for every $U'$ and $R'$ disjoint from $U'$ with $|R'|< |R|$.

Consider the case that the function call returns early in line 2 and therefore does not enumerate any quorums. Then $Q=\emptyset$; by Lemma <ref> this implies that $U\cup R$ does not contain any quorums that are supersets of $U$ and therefore there are no quorums to enumerate – the function behaves correctly.

Now consider the case that the algorithm does not return early in line 2. Then $Q$ is a quorum with $U\subseteq Q\subseteq U\cup R$ and line 3 will correctly output this quorum. All remaining quorums $Q'$ with $U\subseteq Q'\subseteq U\cup R$ will be proper subsets of $Q$ as $Q$ is the greatest quorum contained in $U\cup R$. Therefore, in order to enumerate all remaining quorums it is sufficient to consider candidates in the set $\{Q'\mid U\subseteq Q'\subset Q\}$. Suppose that the set $Q\setminus U$ has $n$ elements and that they are enumerated in the order $v_1, \ldots, v_n$ in the loop in lines 5 to 7. Observe that we can decompose the set $\{Q'\mid U\subseteq Q'\subset Q\}$ disjointly as follows:

\begin{align}
\{Q'\mid U\subseteq Q'\subset Q\} &= \big\{Q'\mid U\subseteq Q'\subseteq Q\setminus\{v_1\}\big\}\nonumber\\
&\phantom{=\ }\mbox{}\cup \big\{Q'\mid U\cup\{v_1\}\subseteq Q'\subseteq Q\setminus\{v_2\}\big\}\nonumber\\
&\phantom{=\ }\mbox{}\cup \cdots\cup\big\{Q'\mid U\cup\{v_1, \ldots, v_{n-1}\}\subseteq Q'\subseteq Q\setminus\{v_n\}\big\}\nonumber\\
&=\bigcup\nolimits_{i=1}^n\big\{Q'\mid U\cup\{v_1, \ldots, v_{i-1}\}\subseteq Q'\subseteq Q\setminus\{v_i\}\big\}.\label{eq:proof-enum-quorums}
\end{align}

The $i$-th component of this union stands for all sets $Q'$ that contain the nodes $v_1, \ldots, v_{i-1}$, but not the node $v_i$. Thus, (<ref>) is a disjoint union. Let $W_i$ be the value of $W$ at the beginning of the $i$-th iteration of the loop in lines 5 to 7. Clearly, $W_i=\{v_{i}, \ldots, v_n\}$. Then the above decomposition can be written as

\begin{align}
\{Q'\mid U\subseteq Q'\subset Q\} &= \bigcup\nolimits_{i=1}^n\big\{Q'\mid Q\setminus W_i\subseteq Q'\subseteq Q\setminus\{v_i\}\big\}.\label{eq:proof-enum-quorums2}
\end{align}

Together with the induction hypothesis this proves the correctness of the algorithm because the $i$-th call to traverseQuorums in line 6 will enumerate the quorums in the $i$-the component of the right-hand side of (<ref>).

For the proof of the time complexity note that every call to the function traverseQuorums will either return early or output its first quorum after time $O(|V|\cdot \Vert F\Vert)$ by Lemma <ref>. If it outputs a quorum, then it will make at most $|V|$ subsequent recursive calls to traverseQuorums. Therefore the call to traverseQuorums will either quit without outputting any other quorums, or it will output the next quorum after at most $O(|V|^2\cdot \Vert F\Vert)$ steps.

2lInput: FBAS $F$ with set of nodes $V$

2lOutput: enumerate all quorums of $F$

1   $\textsc{traverseQuorums}(F, \emptyset, V)$

2lInput: FBAS $F$ with set of nodes $V$; $U\subseteq V$; $R\subseteq V\setminus U$

2lOutput: enumerate all quorums $Q$ of $F$ with $U\subseteq Q\subseteq U\cup R$

1   $Q\leftarrow\textsc{greatestQuorum}(F, U\cup R, U)$

2   if $Q=\emptyset$ return

3   output $Q$

4   $W\leftarrow Q\setminus U$

5   for $v$ in $Q\setminus U$

6       $\textsc{traverseQuorums}(F, Q\setminus W, W\setminus\{v\})$

7       $W\leftarrow W\setminus\{v\}$

Algorithm for enumerateQuorums.

In this experiment we study the computation time of the enumerateQuorums algorithm (see Figure <ref>) implemented in Stellar Observatory in comparison with the number of quorums of a sequence of FBAS that are constructed similarly to the current maximal SCC of the Stellar network; see Example <ref>. We consider $n$ organizations $A_1,\ldots,A_n$ with $3$ nodes each, and define an FBAS $(V,S)$

by $V=A_1\cup\cdots\cup A_n$, so that $|V|=3n$, and quorum slices
where $d_v=(2,\{v\},\{R_v(d)\})$ and
$d=(t,\emptyset,\{(2,A_1,\emptyset),\ldots,(2,A_n,\emptyset)\})$ for a $t\in\N$.
Essentially, $t$ organizations are required on the root level and then $2$ nodes are required within each organization. Analogous to the Stellar network (cf. Example <ref>), we transform the quorum slice definition for each node $v\in V$ to $d_v$ by moving $v$ to the root level and removing it from its original position with $R_v$; see Definition <ref>.

We consider the root level thresholds $t=n-1$ and $t=\lfloor\frac{2}{3}n\rfloor+1$. In both cases the number of quorums as well as the computation time of the enumerateQuorums algorithm grow exponentially with $n$; see the dashed line (<ref>)
and the solid line (<ref>) in Figure <ref>, respectively. The code for reproducing the results is available on GitHub[<https://github.com/andrenarchy/stellar-experiments>].

Root threshold $n-1$

Root threshold $\lfloor\frac{2}{3}n\rfloor+1$

Computation time of enumerateQuorums in seconds (<ref>) and number of quorums (<ref>)
for the FBAS described in Example <ref> consisting of $n$ organizations with $3$ nodes each. Note that the y-axes are scaled logarithmically.

§.§ Quorum intersection

We have shown in Section <ref> that the problem to decide whether a given FBAS has quorum intersection is NP-complete. The brute-force approach to solve this problem is to first enumerate all quorums (see the previous section), and then to compare all pairs of quorums. This method has complexity $2^{O(|V|)}$ as the number of quorums can be exponential in the number of nodes.

In this section we will discuss an algorithm to decide quorum intersection that still has exponential time complexity but that is drastically more efficient than the brute-force approach. This algorithm is due to Lachowski <cit.> and is based on the following key ideas:

* Preprocessing the given FBAS can considerably reduce its size before enumerating the quorums.

* Instead of enumerating all quorums it is sufficient to enumerate only minimal quorums up to a certain size.

§.§.§ Strongly connected components

In this section we will make use of the trust graph as defined in Definition <ref>. In the following lemma we use the notation $S|_C$, which is the restriction of $S$ to $C$; see Lemma <ref>.

* If $(V, S)$ has quorum intersection, then the greatest SCC of its trust graph exists.

* Let $Q\subseteq V$ be a quorum of $(V,S)$. Then there is an SCC $D$ such that $D\cap Q$ is a quorum of $(V,S)$.

* If $C$ is the greatest SCC and no other SCC contains a quorum of $(V,S)$, then $(C, S|_C)$ has quorum intersection if and only if $(V,S)$ has quorum intersection.

(1) If there are distinct maximal SCC, then there are disjoint quorums due to Lemma <ref>(3). Hence, there is only one maximal SCC and it is even the greatest SCC by Lemma <ref>.

(2) Let $\mathcal D$ be the set of all SCCs that intersect $Q$. Then $\mathcal D$ is nonempty as $Q$ is nonempty. There is at least one SCC $D\in\mathcal D$ such that no other SCC in $\mathcal D$ is reachable from $D$. We show that $D\cap Q$ is a quorum of $(V,S)$. Let $v\in D\cap Q$. Then there is a slice $s\in S(v)$ with $s\subseteq Q$. Suppose that $s\not\subseteq D$ and let $u\in s\setminus D$. Thus, $u$ is in an SCC $D'$ different from $D$. Clearly, $D'\in \mathcal D$ because $u\in s\subseteq Q$. It follows that $D'$ is reachable from $D$, contrary to the construction of $D$. Thus, our assumption $s\not\subseteq D$ was wrong. Since $s\subseteq D\cap Q$, the set $D\cap Q$ is a quorum of $(V,S)$.

(3) “$\Rightarrow$”: Suppose that $(V,S)$ has disjoint quorums $Q_1$ and $Q_2$. Because of (2), there are SCCs $D_1$ and $D_2$ such that $D_1\cap Q_1$ and $D_2\cap Q_2$ are quorums of $(V,S)$. Then $D_1=D_2=C$ by assumption. The definition of $(C, S|_C)$ immediately implies that $C\cap Q_1$ and $C\cap Q_2$ are not just quorums of $(V,S)$ but also of $(C, S|_C)$. Therefore $(C, S|_C)$ does not have quorum intersection.

“$\Leftarrow$”: If $Q_1$ and $Q_2$ are disjoint quorums of $(C, S|_C)$, then they are also disjoint quorums of $(V,S)$ by Lemma <ref>(2).

Using the results of Lemma <ref> we can preprocess the FBAS and reduce its size before running the actual algorithm to decide quorum intersection. To this end we determine the strongly connected components of the trust graph using, e.g., Tarjan's algorithm <cit.>. If there is no greatest SCC, then Lemma <ref>(1) implies that there are disjoint quorums. Next, we can check whether any of the SCCs different from the greatest SCC $C$ contain a quorum by using the function greatestQuorum; see Lemma <ref>. If this is the case, then there are disjoint quorums because the greatest SCC is itself a quorum by Lemma <ref>(3). Otherwise, Lemma <ref>(3) allows to reduce the quorum intersection decision to the FBAS $(C, S|_C)$.

§.§.§ Minimal quorums

Instead of enumerating all quorums of $(V,S)$ and comparing them pairwise, we can instead enumerate all minimal quorums $Q$ up to size $|V|/2$ and check whether $V\setminus Q$ contains a quorum; see the function quorumIntersection in Figure <ref>. For now assume that $\textsc{traverseMinQuorums}(F, \emptyset, V)$ enumerates all minimal quorums up to size $|V|/2$; we will prove its correctness in Lemma <ref>.

The function quorumIntersection decides whether $F$ has quorum intersection and returns a pair of disjoint quorums if it does not.

Suppose that quorumIntersection returns a pair $(Q,Q')$. Thus $Q$ is a minimal quorum and $Q'=\textsc{greatestQuorum}(F, V\setminus Q)\not=\emptyset$. Then by Lemma <ref>, $Q'$ is a quorum which is obviously disjoint from $Q$. Hence, $(V,S)$ does not have quorum intersection.

Now suppose that $(V,S)$ does not have quorum intersection. We will prove that quorumIntersection does not return $\mathit{true}$ but two disjoint quorums instead. There are two disjoint quorums $Q_1$ and $Q_2$. Without loss of generality, $|Q_1|\leq |Q_2|$, which implies $|Q_1|\leq |V|/2$. There is a minimal quorum $Q$ in $Q_1$, possibly $Q_1$ itself. Clearly, $Q$ will be one of the quorums enumerated by $\textsc{traverseMinQuorums}(F, \emptyset, V)$ in line 1. Since $Q_2$ is a quorum contained in $V\setminus Q$, the set $Q'$ computed in line 2 will not be empty and therefore quorumIntersection will not return $\mathit{true}$.

2lInput: FBAS $F$ with set of nodes $V$

2lOutput: $\mathit{true}$ if $F$ has quorum intersection; otherwise two disjoint quorums

1   for $Q$ in $\textsc{traverseMinQuorums}(F, \emptyset, V)$

2       $Q'\leftarrow\textsc{greatestQuorum}(F, V\setminus Q)$

3       if $Q'\not=\emptyset$ return $(Q,Q')$

4   return $\mathit{true}$

2lInput: FBAS $F$ with set of nodes $V$; $U\subseteq V$; $R\subseteq V\setminus U$

2lOutput: enumerate all minimal quorums $Q$ of $F$ with

2lOutput: $U\subseteq Q\subseteq U\cup R$ and $|Q|\leq |V|/2$

1   if $|U|>|V|/2$ return

2   $Q=\textsc{greatestQuorum}(F, U)$

3   if $Q\not=\emptyset$

4       if $U=Q$ and not $\textsc{containsProperSubQuorum}(F, U)$

5           output $U$

6   else

7       if $R\not=\emptyset$ and $\textsc{greatestQuorum}(F, U\cup R, U)\not=\emptyset$

8           $v\leftarrow \text{pick from $R$}$

9           $\textsc{traverseMinQuorums}(F, U, R\setminus\{v\})$

10           $\textsc{traverseMinQuorums}(F, U\cup\{v\}, R\setminus\{v\})$

2lInput: FBAS $F$ with set of nodes $V$; $U\subseteq V$

2lOutput: whether there is a quorum $Q\subsetneq U$

1   for $v$ in $U$

2       if $\textsc{greatestQuorum}(F, U\setminus \{v\})\not=\emptyset$ return $\mathit{true}$

3   return $\mathit{false}$

Algorithm for quorumIntersection.

Now let us prove the correctness of traverseMinQuorums; see Figure <ref>. We remark that line 8 of traverseMinQuorums nondeterministically picks an element from $R$. In practice we would use some heuristics to decide what element to pick next in order to minimize the run-time. These details shall not concern us in the present paper.

Given two sets $U\subseteq V$ and $R\subseteq V\setminus U$, the function invocation $\textsc{traverseMinQuorums}(F, U, R)$ enumerates every minimal quorum $Q$ of $F$ such that $U\subseteq Q\subseteq U\cup R$ and $|Q|\leq |V|/2$. Furthermore, every such quorum is enumerated exactly once.

We give a proof by induction over $|R|$. Before we proceed to the proof of the induction base and induction step, we will look at two special cases first.

First consider the case $|U|>|V|/2$. Then there are no sets $Q$ with $U\subseteq Q\subseteq U\cup R$ and $|Q|\leq |V|/2$. Moreover, traverseMinQuorums returns early in line 1 and, thus, does not enumerate any sets; i.e., the function behaves correctly.

Next suppose that $|U|\leq |V|/2$ and that $U$ contains a quorum. In this case the function call will branch into line 4 because $Q$ is nonempty by Lemma <ref>. Observe that the function containsProperSubQuorum defined in Figure <ref> correctly decides whether a set $U$ of nodes contains a proper subset that is a quorum. We conclude that the function traverseMinQuorums will output $U$ in line 5 if and only if $U$ itself is a quorum (i.e., $U=Q$) and it is a minimal quorum. This is obviously correct behavior. The call to traverseMinQuorums will then finish and not enumerate any other quorum. This is also correct because there cannot be any other minimal quorum $Q$ with $U\subseteq Q$.

Let us now proceed to the actual inductive proof. It is sufficient to consider the case that $|U|\leq |V|/2$ and that $U$ does not contain a quorum – the latter condition implies that $U$ itself is not a quorum. This case also implies that traverseMinQuorums branches into line 7.

For the base case $|R| = 0$ we have $R=\emptyset$ and traverseMinQuorums will not branch into line 8, i.e., it does not enumerate any sets. This is correct behavior as the only set $Q$ satisfying $U\subseteq Q\subseteq U\cup R$ is $Q=U$ and it is not a quorum.

For the induction step let $|R|>0$. Then $R\not=\emptyset$. We distinguish two cases. If $\textsc{greatestQuorum}(F, U\cup R, U)=\emptyset$, then (i) there is no quorum $Q$ with $U\subseteq Q\subseteq U\cup R$ by Lemma <ref> and (ii) traverseMinQuorums does not branch into line 8 and does not enumerate any quorums; hence traverseMinQuorums behaves correctly. If $\textsc{greatestQuorum}(F, U\cup R, U)\not=\emptyset$, then traverseMinQuorums branches into line 8, picks a node $v$ from $R$ and makes two recursive calls to traverseMinQuorums. By induction, the first call enumerates all minimal quorums $Q$ with $U\subseteq Q\subseteq U\cup R$ that do not contain $v$ and the second call all those minimal quorums that do contain $v$.

In this experiment we study the computation time of the quorumIntersection algorithm (see Figure <ref>) implemented in Stellar Observatory for the same sequence of FBAS as in Example <ref>. All FBAS of this form with $n>2$ have quorum intersection, and the computation time of the quorumIntersection algorithm grows exponentially; see Figure <ref>.

Root threshold $n-1$

Root threshold $\lfloor\frac{2}{3}n\rfloor+1$

Computation time of quorumIntersection in seconds
for the FBAS described in Example <ref> consisting of $n$ organizations with $3$ nodes each. Note that the y-axes are scaled logarithmically.

§ INTACTNESS

A node $v\in V$ can be either well-behaved or ill-behaved[Alternative terms used in this context, which mean the same as ill-behaved, are faulty (see, e.g., <cit.>) and Byzantine (see, e.g. <cit.>).].
This is a local property, which is independent of the quorum function $S$, and which other nodes cannot control. An important question is whether ill-behaved nodes can negatively impact other (well-behaved) nodes. If this happens, these other nodes are befouled by the ill-behaved nodes. This intuitive idea will be made precise in Definitions <ref>, <ref> and <ref> below,
which correspond to the original development of Mazières <cit.>:

Let $(V,S)$ be an FBAS and let $D\subseteq V$. The FBAS without $D$ is defined by
$(V,S)^D=(V\setminus D,S^D)$, where

$$S^D(v)=\{s\setminus D\mid s\in S(v)\}~\text{for all}~v\in V\setminus D.$$

Thus, forming $(V,S)^D$ amounts to deleting the nodes in $D$ from $V$ and from all quorum slices. The next result of Mazières will be useful in our discussion below.

Let $Q\subseteq V$ be a quorum in $(V,S)$ and let $D\subseteq V$. If $Q\setminus D\not=\emptyset$, then $Q\setminus D$ is a quorum in $(V,S)^D$.

The following two corollaries are an immediate consequence of  Definition <ref>. The second one is a consequence of Lemma <ref>(2).

Let $D\subseteq V$ and $E\subseteq V\setminus D$. Then $((V,S)^D)^E=(V,S)^{D\cup E}$.

Let $Z$ be a trust cluster of $(V,S)$. Then $(V,S)^{V\setminus Z}=(Z, S|_Z)$ and every quorum of $(V,S)^{V\setminus Z}$ is also a quorum of $(V,S)$.

The following notion of dispensible sets (DSets) is an important stepping stone for the definition of intactness.

Let $(V,S)$ be an FBAS. A set $D\subseteq V$ is a dispensible set or DSet, when

* $(V,S)^D$ has quorum intersection, and

* either $V\setminus D$ is a quorum in $(V,S)$ or $D=V$.

By this definition, $D=V$ is always a DSet, since $(V,S)^V=(\emptyset,S^D)$ with $S^D:\emptyset\rightarrow \{\{\emptyset\}\}$, consistently with Definition <ref>, and this FBAS trivially has quorum intersection. Whenever an FBAS $(V,S)$ has quorum intersection, $D=\emptyset$ is a DSet. An extreme case arises when $S(v)=\{V\}$ for all $v\in V$, since then $\emptyset$ and $V$ are the only DSets.

Consider the FBAS $(V,S)$ from Example <ref>. Since this FBAS has quorum intersection, $\emptyset$ and $V$ are DSets. For every DSet $D\neq \emptyset$ it is necessary that $V\setminus D$ is a quorum in $(V,S)$. The only candidates are $\{1,2,3\}$, $\{4,5,6\}$, and $V\setminus\{7\}$. For each of these sets we see that the corresponding FBAS $(V,S)^D$ indeed has quorum intersection, and hence the DSets of $(V,S)$ are given by

$$\emptyset, \quad\{1,2,3\},\quad \{4,5,6\},\quad
V\setminus\{7\},\quad V.$$

We can now formalize the intuitive idea described at the beginning of this section.

Let $B\subseteq V$ be the set of ill-behaved nodes in the FBAS $(V,S)$. A node $v$ is called $B$-intact when there exists a single DSet $D$ which contains all ill-behaved nodes but not $v$, i.e., $B\subseteq D\subseteq V\setminus\{v\}$. If $B$ is obvious from the context, then we just say that $v$ is intact instead of $B$-intact. If $v$ is not intact, it is called befouled.

Note that if a node $v$ is intact, then the definition immediately implies that it is well-behaved. Conversely, if $v$ is ill-behaved, then it is befouled. The interesting object of study are the well-behaved nodes that are befouled.

We have shown in Theorem <ref> that the problem SimpleQuorumSplit is NP-complete. Since the problem to decide whether a given set $D\subseteq V$ is a DSet involves the problem to decide whether $(V,S)^D$ has quorum intersection, the DSet decision problem is computationally at least as hard. We will deal with the algorithmic treatment of intactness in Section <ref> below.

§.§ Intact nodes in symmetric simple FBAS

While the computation of quorums and DSets in general is computationally challenging, the quorums of a symmetric simple FBAS can be completely characterized, see Lemma <ref>. The following result shows that a simple characterization also exists for DSets of symmetric simple FBAS.

Let $(V,k)$ be a symmetric simple FBAS, and let $D\subseteq V$. Then the set of all quorums of $(V,k)^D$ is given by $\bigl\{Q\subseteq V\setminus D\,\mid\,|Q|\geq \max\{1,k-|D|\}\bigr\}$.
Moreover, $(V,k)^D$ has quorum intersection if and only if $\max\{1,k-|D|\}>(|V|-|D|)/2$.

If $Q\subseteq V\setminus D$ is any set with $|Q|<\max\{1,k-|D|\}$ then either $Q$ is empty and hence not a quorum, or $1\leq |Q|<k-|D|$. Let $v\in Q$, and let $s$ be any quorum slice of $v$ in $(V,k)$. From $|s|=k$ we obtain $|s\setminus D|\geq |s|-|D|=k-|D|>|Q|$, which shows that $s\setminus D$ is not contained in $Q$, and hence $Q$ cannot be a quorum.

Now let $Q\subseteq V\setminus D$ with $|Q|\geq \max\{1,k-|D|\}$; then $Q$ is nonempty. Consider a node $v\in Q$.

(i) If $|D|>k-1$, then there exist distinct $d_1,\dots,d_{k-1}\in D$. Then $\{v\}\cup \{d_1,\dots,d_{k-1}\}$ is a quorum slice of $v$ in $(V,k)$ and, thus, $\{v\}$ is a quorum slice of $v$ in $(V,k)^D$ that is contained in $Q$.

(ii) If $|D|\leq k-1$, then $|Q|\geq k-|D|$ implies that there exist distinct elements $q_1,\dots,q_{k-|D|-1}\in Q\setminus\{v\}$. Then $\{v\}\cup\{q_1,\dots,q_{k-|D|-1}\}\cup D$
is a quorum slice of $v$ in $(V,k)$, and thus $\{v\}\cup\{q_1,\dots,q_{k-|D|-1}\}$ is a quorum slice of $v$ in $(V,k)^D$ that is contained in $Q$.

This concludes the proof that $Q$ is a quorum of $(V,k)^D$. The statement that $(V,k)^D$ has quorum intersection if and only if $\max\{1,k-|D|\}>(|V|-|D|)/2$ can be proved similarly to Lemma <ref>.

We remark that deleting nodes from a symmetric simple FBAS according to Definition <ref> does not preserve the property to be symmetric and simple. To show this consider the example symmetric simple FBAS $(V,k)$ with $V=\{a,b,c\}$ and $k=2$. Let $D=\{c\}$. Then the quorum slices of $a$ in $(V,k)$ are $\{a,b\}$ and $\{a,c\}$ and the quorum slices of $a$ in $(V,k)^D$ are $\{a, b\}$ and $\{a\}$. These last two quorum slices have different sizes so that we can conclude that $(V,k)^D$ is not simple and therefore not symmetric.

Using the Lemmas <ref> and <ref> we now characterize the DSets of a simple symmetric FBAS.

Let $(V,k)$ be a symmetric simple FBAS. A set $D\subseteq V$ is a DSet if and only if one of the following holds:

* $D=V$, or

* $k=1$ and $|D|=|V|-1$, or

* $|D|\leq\min\{|V|-k,\,2k-|V|-1\}$.

By definition, $D$ is a DSet if and only if

* $D=V$ or

* $\max\{1,k-|D|\}>(|V|-|D|)/2$, i.e., $(V,k)^D$ has quorum intersection (cf. Lemma <ref>) and
$|V|-|D|\geq k$, i.e., $V\setminus D$ is a quorum in $(V,k)$ (cf. Lemma <ref>).

The equivalence is now shown by the following implications:

“(ii) $\Rightarrow$ (1), (2) or (3)”: If $\max\{1,k-|D|\}>(|V|-|D|)/2$, then either (a) $1>(|V|-|D|)/2$, or (b) $k-|D|>(|V|-|D|)/2$. In case (a) we have either $V=D$ and hence statement (1), or $|V|-|D|=1$, which together with $|V|-|D|\geq k$ yields (2). In case (b) we have $|D|<2k-|V|$, which together with $|D|\leq |V|-k$ yields (3).

“(2) or (3) $\Rightarrow$ (ii)”:  Clearly, (2) implies (ii). Moreover, (3) yields $|D|\leq |V|-k$ and hence $|V|-|D|\geq k$, as well as $|D|\leq 2k-|V|-1$ or equivalently $k-|D|>(|V|-|D|)/2$, so that we again obtain (ii).

Lemma <ref> shows that if $(V,k)$ is a symmetric simple FBAS with $1<k=|V|$ or $1<k\leq (|V|+1)/2$, then $(V,k)$ has only the trivial DSets $D=V$ and possibly $D=\emptyset$.

We say that an FBAS $(V,S)$ is resilient against $m\geq 0$ ill-behaved nodes if no well-behaved node becomes befouled whenever there are at most $m$ ill-behaved nodes. We now ask about the minimum size of $V$ such that for a suitable $k$ there is a symmetric simple FBAS $(V,k)$ that is resilient against $m$ ill-behaved nodes. We only want to consider FBAS that have quorum intersection and therefore we require $k>|V|/2$ by Lemma <ref>. In particular, $k>1$ if we exclude trivial FBAS.

We know that a node $v$ is intact when all ill-behaved nodes (at most $m$) are contained in a single DSet that does not contain $v$. By Lemma <ref>, the relevant DSets of $(V,k)$ are given by all sets $D\subseteq V\setminus\{v\}$ which satisfy $m\leq |D|\leq \min\{|V|-k, 2k-|V|-1\}$, and hence $|V|$ and $k$ must satisfy $m\leq \min\{|V|-k, 2k-|V|-1\}$. Maximizing the right hand side over $k$ by equating the two expressions yields $k=2|V|/3+1/3$, and then $m\leq |V|-k$ leads to $|V|\geq 3m+1$. Thus, the minimum number of nodes is $|V|=3m+1$, and the corresponding constant is $k=2(3m+1)/3+1/3=2m+1$.

We thus have shown the following result, which is consistent with traditional Byzantine fault tolerance; see, e.g., <cit.>, <cit.>, and Example <ref> above.

The minimum number of nodes of a symmetric simple FBAS $(V,k)$ that is resilient against (at most) $m$ ill-behaved nodes is $3m+1$, and this FBAS has constant $k=2m+1$.

§.§ Comparison of intactness definitions

In the recent publications <cit.>, quorums and intactness are defined differently from <cit.>, and in this subsection we will compare both variants. Let us first give an intuition for the main differences:

* In the definitions of <cit.>, which we adopted in this paper, the main notions are introduced in the following order: First, FBAS, quorums, quorum intersection, and DSets are defined without any reference to ill-behaved nodes. Then one postulates a set of ill-behaved nodes and introduces the concept of an intact node, which depends on the set of ill-behaved nodes.

* In <cit.>, the set of intact nodes is directly “baked into” an FBAS, i.e., in these papers FBAS are richer structures that already define their intact nodes. Then quorums and quorum intersection directly incorporate the set of intact nodes into their definition. Finally, the notion of intact sets is introduced.

The advantage of the first paradigm is that FBAS can be viewed as structures agnostic to the set of ill-behaved nodes (which is usually unknown in practice). An advantage of the second paradigm is its simplicity – it does not require definitions of DSets or FBAS of the form $(V,S)^D$.

In order to mathematically compare the two paradigms, we need the following definition.

Let $(V,S)$ be an FBAS and $B\subseteq V$. A $B$-quorum is a nonempty set $Q\subseteq V$ such that for every $v\in Q\setminus B$ there is a quorum slice $s\in S(v)$ with $s\subseteq Q$. A subset $U\subseteq V\setminus B$ is called a $B$-intact set if

* $U$ is a $B$-quorum or $U=\emptyset$,

* for all $B$-quorums $Q$, $Q'$ that intersect $U$, also $Q\cap Q'$ intersects $U$.

Note that in Definition <ref> we have defined $B$-intact nodes, whereas Definition <ref> introduces $B$-intact sets (as in <cit.> and <cit.>).
Intuitively, we expect that a node is $B$-intact if and only if it is contained in a $B$-intact set. We will show that this is actually not the case, and that the former property is strictly stronger than the latter.

For the following discussion we fix a set $B\subseteq V$, the set of ill-behaved nodes.

If a node $v$ is $B$-intact, then it is contained in a $B$-intact set.

Let us first prove the following auxiliary statement:

* Let $D\subseteq V$ contain $B$ and let $Q$ be a $B$-quorum with $Q\not\subseteq D$. Then $Q\setminus D$ is a quorum in $(V,S)^D$.

Obviously, $Q\setminus D$ is nonempty. Let $v\in Q\setminus D$. Then in particular $v\not\in B$. Hence, there is an $s\in S(v)$ with $s\subseteq Q$ and, therefore, $s\setminus D\subseteq Q\setminus D$. We conclude that $Q\setminus D$ is a quorum in $(V,S)^D$. This concludes the proof of Statement (A).

Now let us proceed with the proof of this lemma. Let $v$ be $B$-intact. Then there is DSet $D$ containing $B$ but not $v$. Let $U=V\setminus D$. We will show that $U$ is a $B$-intact set. Clearly, $U$ is a quorum because $U$ is nonempty and due to the definition of $D$. Then $U$ is also a $B$-quorum. Let $Q,Q'$ be $B$-quorums that intersect $U$. By Statement (A), $Q\setminus D$ and $Q'\setminus D$ are quorums in $(V, S)^D$. Since $D$ is a DSet we obtain that $\emptyset\not=(Q\setminus D)\cap (Q'\setminus D)=(Q\cap Q')\setminus D$, i.e., $Q\cap Q'$ intersect $U$.

The following example shows that the converse of Lemma <ref> does not hold in general, i.e., we cannot conclude that every member of a $B$-intact set is $B$-intact itself.

Let $V=\{a,b,c,d\}$,

\begin{align*}
S(d)&=\{\{b,d\}, \{c,d\}\},
\end{align*}

and let $B=\{a\}$. Then there are two quorums, $\{c,d\}$ and $\{a,b,c,d\}$, and four $B$-quorums, $\{a\}$, $\{a,c,d\}$, $\{c,d\}$ and $\{a,b,c,d\}$, so that $\{c,d\}$ is a $B$-intact set.

On the other hand, the only DSet that contains $B$ is $V$ itself, and hence
no node in $V$ is $B$-intact. (Observe that $\{a,b\}$ is not a DSet as $(V, S)^{\{a,b\}}$ has the quorums $\{c\}$ and $\{d\}$ and therefore has no quorum intersection.)

We will now introduce an FBAS property under which the converse of  Lemma <ref> is guaranteed to hold.

We say that $(V, S)$ has the $B$-subslice property if for every $v\in V\setminus B$, $s_v\in S(v)$ and $u\in s_v\setminus B$ there is some $s_u\in S(u)$ with $s_u\subseteq s_v$.

We remark that the $B$-subslice property reminds of the main property of Personal Byzantine Quorum Systems <cit.>. It is easy to see that the $B$-subslice property holds for symmetric simple FBAS for every set $B$. Moreover, this property holds for many example FBAS presented in this paper such as Examples <ref>, <ref>, <ref> and <ref>. More interestingly, it is easy to show that also the greatest SCC of the Stellar network (see Example <ref>) has the $B$-subslice property for every set $B$ of ill-behaved nodes.

Let $(V,S)$ have the $B$-subslice property and let $v\in V$. Then the following statements are equivalent:

* $v$ is $B$-intact.

* $v$ is contained in a $B$-intact set.

The direction (1) $\Rightarrow$ (2) follows from Lemma <ref>.

Let us now prove the direction (2) $\Rightarrow$ (1) and suppose that $v$ is contained in a $B$-intact set $U$. It suffices to show that $D=V\setminus U$ is a DSet because $v\in U$ and $U\cap B=\emptyset$. By the last property, if $U$ is a $B$-quorum, then it is also a quorum. Hence, the only non-trivial property that we need to show is that $(V,S)^D$ has quorum intersection. Let $Q, Q'$ be quorums in $(V,S)^D$. We will show that there are $B$-quorums $P$, $P'$ with $P\setminus D= Q$ and $P'\setminus D=Q'$. We only prove that there is such a set $P$; the proof for the existence of $P'$ follows by symmetry.

For every $v\in Q$ there is a slice $s_v\in S(v)$ such that $s_v\setminus D\subseteq Q$. Let $P=\bigcup_{v\in Q}s_v$. We will show that (i) $P$ is a $B$-quorum and that (ii) $P\setminus D=Q$.

(i) Let $u\in P\setminus B$. Then there is some $v\in Q$ with $u\in s_v$. Since $v\in Q\subseteq V\setminus D$, we have $v \not\in B$ and $u\not\in B$. Then there is some $s_u\in S(u)$ with $s_u\subseteq s_v\subseteq P$ by the $B$-subslice property.

(ii) $P\setminus D = \bigcup_{v\in Q}s_v\setminus D=Q$ because $v\in s_v\setminus D\subseteq Q$ for every $v\in Q$.

This concludes the proof for the existence of $P$ and $P'$. Since $Q$ and $Q'$ are contained in $U$ and nonempty, the sets $P$ and $P'$ intersect $U$. Thus, also $P\cap P'$ intersects $U$ because $U$ is a $B$-intact set. Thus, $\emptyset\not=(P\cap P')\cap U=(P\cap P')\setminus D=(P\setminus D)\cap (P'\setminus D)=Q\cap Q'$. We conclude that $(V,S)^D$ has quorum intersection.

§ ALGORITHMIC TREATMENT OF INTACTNESS

Let us now study the problem to algorithmically determine the set of $B$-intact nodes given a set $B$ of ill-behaved nodes. We point out that in a real-life situation one does usually not know the set $B$ and would not be able to apply such an algorithm. However, it is useful for analyzing a given FBAS and to simulate certain failure and attack scenarios.

The techniques we use in this section are based on methods and algorithms developed in Section <ref>. Throughout this section we will assume that we only consider FBAS $(V,S)$ that have quorum intersection.

§.§ Strongly connected components

In this section we revisit the trust graph of the FBAS and show how it affects the intactness of nodes in an FBAS. We will see that analyzing the structure of the SCCs of the trust graph allows us to prune major parts of the FBAS when determining intactness of nodes.

Let us first present two rather technical properties about trust clusters and DSets. The first one ensures that every DSet still behaves like a DSet within a trust cluster. The second one states that every DSet within a trust cluster can be extended to a DSet for the whole FBAS.

Let $Z$ be a trust cluster of $(V,S)$ and let $D$ be a DSet of $(V,S)$. Then $D\cap Z$ is a DSet of $(Z, S|_Z)$.

By Corollary <ref> $(Z, S|_Z)=(V, S)^{V\setminus Z}$. Thus, we need to show that

* $((V, S)^{V\setminus Z})^{D\cap Z}$ has quorum intersection.

* $Z\setminus (D\cap Z)$ is a quorum in $(V, S)^{V\setminus Z}$ or $D\cap Z=Z$.

(1) The equality $(V\setminus Z)\cup(D\cap Z)=D\cup((V\setminus D)\setminus (Z\setminus D))$ and Corollary <ref> imply $((V, S)^{V\setminus Z})^{D\cap Z}=((V, S)^D)^{(V\setminus D)\setminus (Z\setminus D)}$. Let us refer to this FBAS as $F'$. It is straightforward to show that $Z\setminus D$ is a trust cluster of $(V, S)^D$. Then Corollary <ref> implies that every quorum of $F'$ is also a quorum of $(V,S)^D$. Thus, $F'$ has quorum intersection because $(V,S)^D$ does have quorum intersection.

(2) We will show the equivalent statement that $Z\setminus D$ is a quorum in $(V, S)^{V\setminus Z}$ or $Z\subseteq D$. Since $D$ is a DSet we have either that $V\setminus D$ is a quorum in $(V,S)$ or that $D=V$. We are done in the latter case as it implies $Z\subseteq D$. Consider the former case and suppose that $Z\not\subseteq D$. We will show that $Z\setminus D$ is a quorum in $(V, S)^{V\setminus Z}$. From $Z\not\subseteq D$ we obtain $(V\setminus D)\setminus (V\setminus Z)\not=\emptyset$. Then Lemma <ref> yields that $(V\setminus D)\setminus (V\setminus Z)=Z\setminus D$ is a quorum in $(V,S)^{V\setminus Z}$.

Let $Z$ be a trust cluster of $(V,S)$ and let $D$ be a DSet of $(Z, S|_Z)$. Then $D\cup (V\setminus Z)$ is a DSet of $(V, S)$.

Our assumption is equivalent to the statement that $D$ is a DSet of $(V, S)^{V\setminus Z}$ due to Corollary <ref>. We need to show that

* $(V, S)^{D\cup (V\setminus Z)}$ has quorum intersection.

* $V\setminus (D\cup (V\setminus Z))$ is a quorum in $(V, S)$ or $D\cup (V\setminus Z)=V$.

Statement (1) follows from Corollary <ref> and the fact that $((V,S)^{V\setminus Z})^D$ has quorum intersection, which is a consequence of our assumption. Next let us prove Statement (2). We have that $Z\setminus D$ is a quorum in $(V, S)^{V\setminus Z}$ or $D=Z$. In the former case Corollary <ref> yields that $V\setminus (D\cup (V\setminus Z))=Z\setminus D$ is a quorum in $(V,S)$. The latter case clearly implies $D\cup (V\setminus Z)=V$.

We can now combine the previous two lemmas to the following result.

Let $Z$ be a trust cluster, $v\in Z$ and $B\subseteq V$.
The node $v$ is $B$-intact in $(V,S)$ if and only if $v$ is $(B\cap Z)$-intact in $(Z,S|_Z)$.

“$\Rightarrow$”: Let $v$ be $B$-intact in $(V,S)$. Then there is a DSet $D$ of $(V,S)$ with $B\subseteq D\subseteq V\setminus\{v\}$. Lemma <ref> yields that $D\cap Z$ is a DSet of $(Z, S|_Z)$. Clearly, $B\cap Z\subseteq D\cap Z\subseteq Z\setminus\{v\}$, which proves that $v$ is $(B\cap Z)$-intact in $(Z,S|_Z)$.

“$\Leftarrow$”: Let $v$ be $(B\cap Z)$-intact in $(Z,S|_Z)$. Then there is a DSet $D$ of $(Z, S|_Z)$ with $B\cap Z\subseteq D\subseteq Z\setminus \{v\}$. Lemma <ref> implies that $D\cup(V\setminus Z)$ is a DSet of $(V,S)$. Note that $B\subseteq(B\cap Z)\cup(V\setminus Z)\subseteq D\cup(V\setminus Z)\subseteq (Z\setminus \{v\})\cup(V\setminus Z)=V\setminus\{v\}$ and therefore, $v$ is $B$-intact in $(V,S)$.

The following corollary uses Lemma <ref>.

Let $C$ be the greatest SCC and $B\subseteq V$. Let $I$ be the set of $B$-intact nodes of $(V,S)$. Then $I\cap C$ is the set of $(B\cap C)$-intact nodes of $(C,S|_C)$.

There are two ways to interpret the previous theorem and corollary. First, whether nodes inside a trust cluster are intact or befouled merely depends on the ill-behaved nodes inside the trust cluster. The ill-behaved nodes outside the trust cluster have no influence on this. Second, if we are only interested to know what nodes inside a specific trust cluster $Z$ are intact, we can apply the algorithm that we present below to the smaller FBAS $(Z, S|_Z)$ instead. This is particularly meaningful when one is only interested in determining what nodes in the greatest SCC are intact. It also shows that the nodes in the greatest SCC have the highest importance in an FBAS – they can influence the intactness of all other nodes but their own intactness cannot be influenced by nodes outside the SCC.

§.§ The intactness algorithm

The algorithm to compute the set of $B$-intact nodes is shown in Figure <ref>. Before we are going to prove its correctness, we want to point out that in a naive implementation of the expression $\textsc{quorumIntersection}(F^{V\setminus Q})$ on line 4 one would need to construct $F^{V\setminus Q}$ first. This can be challenging as usually $F^{V\setminus Q}$ is not a simple FBAS even if $F$ is a simple FBAS; see the remark after Lemma <ref>. Then the construction of $F^{V\setminus Q}$ would lead to an exponential blowup; cf. our concept of size of general and simple FBAS in Definition <ref>.

There is a better approach that avoids that problem. We can redefine the function $\textsc{quorumIntersection}$ to accept an additional parameter $D$, so that the function call $\textsc{quorumIntersection}(F, D)$ determines whether $F^D$ has quorum intersection. This can be achieved by redefining the functions traverseMinQuorums, greatestQuorum and containSlice, too, and equip them with an additional parameter $D$ in a similar fashion. Then the parameter $D$ is forwarded from quorumIntersection to greatestQuorum to containsSlice and every reference to $V$ in these algorithms is replaced by $V\setminus D$. Additionally we need to change the logic of the function containsSlice: replace line 2 for the general FBAS version with

if $s\setminus D\subseteq U$ return $\mathit{true}$

and replace line 1 for the simple FBAS version with

return $|(U\cup D)\cap q(v)|\geq n(v)$

While the change to the general FBAS version is obvious, the change to the simple FBAS version requires some argument.

Let $F=(V, q, n)$ be a simple FBAS, let $D, U\subseteq V$ and $v\in U\setminus D$. Then $v$ has a quorum slice in $F^D$ contained in $U$ if and only if $|(U\cup D)\cap q(v)|\geq n(v)$.

First we expand the simple FBAS $(V, q, n)$ into its general form $(V, S)$, i.e., $S(v)=\{W\subseteq q(v)\mid v\in W, |W|=n(v)\}$. Next we construct $F^D=(V\setminus D, S^D)$ with

\begin{align*}
S^D(v)&=\{s\setminus D\mid s\in S(v)\}
=\{W\setminus D\mid W\subseteq q(v), v\in W, |W|=n(v)\}.
\end{align*}

Then the following statements are equivalent: (i) $v$ has a quorum slice in $F^D$ contained in $U$, and (ii) there is a set $W\subseteq q(v)$ with $v\in W$, $|W|=n(v)$ and $W\setminus D\subseteq U$. It remains to prove that the latter statement is equivalent to  (iii) $|(U\cup D)\cap q(v)|\geq n(v)$. For the direction (ii) $\Rightarrow$ (iii) we get $W\subseteq U\cup D$ and therefore $W\subseteq (U\cup D)\cap q(v)$. Hence, $n(v)=|W|\leq |(U\cup D)\cap q(v)|$. For the direction (iii) $\Rightarrow$ (ii) we have $v\in (U\cup D)\cap q(v)$, and therefore there is a subset $W\subseteq (U\cup D)\cap q(v)$ with $|W|=n(v)$ and $v\in W$. This set $W$ clearly satisfies (ii).

2lInput: FBAS $F$ having quorum intersection with set of nodes $V$; $B\subseteq V$

2lOutput: the set of all $B$-intact nodes

1   $U_1\rightarrow V\setminus B$, $i\leftarrow 1$

2   repeat

3       $Q\leftarrow \textsc{greatestQuorum}(F, U_i)$

4       $\mathrm{result} \leftarrow \textsc{quorumIntersection}(F^{V\setminus Q})$

5       if $\mathrm{result}=\mathit{true}$

6           return $Q$

7       else

8           $(Q_1, Q_2)\leftarrow \mathrm{result}$

9           $W_1\leftarrow \textsc{greatestQuorum}(F, Q\setminus Q_1)$

10           $W_2\leftarrow \textsc{greatestQuorum}(F, Q\setminus Q_2)$

11           if $W_1=\emptyset$

12               $U_{i+1}\leftarrow W_2$

13           else if $W_2=\emptyset$

14               $U_{i+1}\leftarrow W_1$

15           else

16               $U_{i+1}\leftarrow W_1\cap W_2$

17       $i\leftarrow i+1$

Algorithm for determining $B$-intact nodes given a set $B$ of nodes. The functions greatestQuorum and quorumIntersection are defined in Section <ref>.

Let us now prove the correctness of the algorithm intactNodes in Figure <ref>. First we state an auxiliary lemma.

Consider the $i$-th iteration of the loop of intactNodes and the sets $Q$ and $U_{i+1}$ constructed in that iteration. Suppose that there is a DSet $D$ with $V\setminus D\subseteq U_i$. Then $V\setminus D\subseteq Q$ and if the iteration branches into line 8, also $V\setminus D\subseteq U_{i+1}$.

This statement is trivial if $D=V$. So let us assume that $D\not=V$; then $V\setminus D$ is a quorum because $D$ is a DSet. Line 3 yields that $Q$ is a quorum with $V\setminus D\subseteq Q$.

Now suppose that the iteration branches into line 8. Let $Q_1$, $Q_2$, $W_1$ and $W_2$ be the values of the respective variables in iteration $i$. Let $a\in\{1,2\}$. We will show that

* if $Q_a\subseteq D$, then $V\setminus D\subseteq W_a$,

* if $Q_a\not\subseteq D$, then $Q_a\setminus D$ is a quorum in $F^D$ and $W_a=\emptyset$,

* $Q_1\subseteq D$ or $Q_2\subseteq D$.

For the proof of the first claim we have that $V\setminus D$ is a quorum contained in $Q\setminus Q_a$, and hence $V\setminus D\subseteq W_a$.

For the proof of the second claim observe that $Q_a\setminus D\not=\emptyset$. In particular, $Q_a\setminus (D\cap Q)\not=\emptyset$.
Together with Lemma <ref> applied to $F^{V\setminus Q}$ and the fact that $Q_a$ is a quorum of $F^{V\setminus Q}$, we obtain that $Q_a\setminus (D\cap Q)$ is a quorum in $(F^{V\setminus Q})^{D\cap Q}$. Clearly, $Q_a\setminus (D\cap Q)=Q_a\setminus D$ because $Q_a\subseteq Q$ by construction in line 4. Furthermore, $(F^{V\setminus Q})^{D\cap Q}=F^D$ by Corollary <ref> and because $(V\setminus Q)\cup(D\cap Q)=D$ due to $V\setminus D\subseteq Q$. We conclude that $Q_a\setminus D$ is a quorum in $F^D$.

For the second claim it remains to show that $W_a=\emptyset$. We assume that $W_a$ is nonempty and derive a contradiction. Then $W_a$ is a quorum by construction and it intersects $V\setminus D$ because we assumed that $F$ has quorum intersection; equivalently, $W_a\setminus D\not=\emptyset$. By Lemma <ref> applied to $F$ we obtain that $W_a\setminus D$ is a quorum in $F^D$. The fact that $D$ is a DSet implies that $F^D$ has quorum intersection and, therefore, $Q_a\setminus D$ and $W_a\setminus D$ intersect. This is a contradiction to $W_a\subseteq Q\setminus Q_a$, which follows from the construction of $W_a$.

For the proof of the third claim assume that $Q_1\not\subseteq D$ and that $Q_2\not\subseteq D$. We will derive a contradiction. By the second claim, $Q_1\setminus D$ and $Q_2\setminus D$ are quorums in $F^D$. They intersect because $D$ is a DSet and, thus, $F^D$ has quorum intersection. This
contradicts that $Q_1$ and $Q_2$ are disjoint by construction.

Now we can employ our three claims to prove the lemma. By the third claim $Q_1\subseteq D$ or $Q_2\subseteq D$. Due to symmetry we will just consider the case that $Q_1\subseteq D$. Then $V\setminus D\subseteq W_1$ by the first claim and, hence, $W_1\not=\emptyset$ because we assumed $D\not=V$. Therefore the algorithm will not branch into line 12. If $Q_2\not\subseteq D$, then by the second claim the algorithm will branch into line 14 and we have $V\setminus D\subseteq W_1=U_{i+1}$. If $Q_2\subseteq D$, then again $\emptyset\not=V\setminus D\subseteq W_2$ and the algorithm will branch into line 16 and we obtain $V\setminus D\subseteq W_1\cap W_2=U_{i+1}$.

Given a set $B$ the function intactNodes returns the set of all $B$-intact nodes.

First we show that the function terminates by proving that the sequence $U_1, U_2, \ldots$ is strictly decreasing, i.e., $U_{i+1}\subsetneq U_i$ for every $i$ as long as the loop does not terminate in line 6. Clearly, (i) $Q\subseteq U_i$ (line 3), (ii) $Q_1\not=\emptyset\not=Q_2$ as they are quorums, and (iii) $W_1\subseteq Q\setminus Q_1$, $W_2\subseteq Q\setminus Q_2$. These statements together imply $W_1\subsetneq U_i$ and $W_2\subsetneq U_i$. Then $U_{i+1}\subsetneq U_i$ because $U_{i+1}\subseteq W_1$ or $U_{i+1}\subseteq W_2$.

Next observe that when intactNodes terminates and returns a set $Q$ in line 6, then $V\setminus Q$ is a DSet because $F^{V\setminus Q}$ has quorum intersetion (line 4) and because $Q$ is a quorum or empty (line 3). Moreover, $V\setminus Q$ contains $B$ because $U_1, U_2, \ldots$ is a decreasing sequence and $U_1\cap B=\emptyset$ by construction and therefore also $Q\cap B=\emptyset$.

Let $D$ be a DSet that contains $B$. Then $V\setminus D\subseteq U_1$. From Lemma <ref> it follows through a simple inductive proof that the result $Q$ returned by the function intactNodes satisfies $V\setminus D\subseteq Q$ or, equivalently, $V\setminus Q\subseteq D$.

We have shown above that $V\setminus Q$ is a DSet containing $B$. Hence, it is the smallest DSet that contains $B$. Thus, $Q$ is the set of all $B$-intact nodes.

Let us analyze the time complexity of the function intactNodes. In every iteration of the loop the call to quorumIntersection dominates the time complexity of the other three calls to greatestQuorum. In fact the former function has exponential time complexity, say, $c\cdot 2^n$ for some constant $c$, where $n$ is the number of nodes of the argument FBAS. The number $n$ for the call $\textsc{quorumIntersection}(F^{V\setminus Q})$ is $|Q|$, which is at most $|V|-i+1$ in the $i$-th iteration because $Q\subseteq U_i$ and the $U_i$ are a strictly decreasing sequence.

Since there are at most $|V|+1$ iterations of the loop, we obtain that the time complexity of intactNodes is roughly

\begin{align*}
\sum\nolimits_{n=0}^{|V|}c\cdot 2^n\leq c\cdot 2^{|V|+1}\;,
\end{align*}

twice as long as determining $\textsc{quorumIntersection}(V)$.

§ PROBABILISTIC INTACTNESS

Let $(V, S)$ be an FBAS with quorum intersection. In this section we will study the probability that a node $v\in V$ is intact. We will treat the set $B$ of ill-behaved nodes as unknown and describe it as a random variable $\mathbb B$. Let $p$ be its probability distribution, i.e., $p(B)=\mathrm P(\mathbb B=B)$. Observe that $p:\mathcal P(V)\rightarrow [0,1]$ with $\sum_{B\subseteq V}p(B) =1$. Then for every $v\in V$ we have

\begin{align}
\mathrm {P}(\text{$v$ is intact})&=\sum_{B\subseteq V}\,\mathrm P(\text{$v$ is intact}\mid \mathbb B = B)\cdot\mathrm P(\mathbb B = B)
=\sum_{\substack{B\subseteq V\\ \text{$v$ is $B$-intact}}} \mathrm P(\mathbb B = B)\nonumber\\
&=\sum_{\substack{B\subseteq V\\ \text{$\exists$ DSet $D$: $B\subseteq D\subseteq V\setminus\{v\}$}}} p(B)\;.\label{eq:def-prob-intactness}
\end{align}

It is particularly interesting to consider the probability of a node to be intact given that it is well-behaved. This is described by the following conditional probability:

\begin{align}
&\mathrm {P}(\text{$v$ is intact}\mid \text{$v$ is well-behaved})\nonumber\\
&=\frac{\mathrm {P}(\text{$v$ is intact})}{\mathrm {P}(\text{$v$ is well-behaved})}\tag{because intact implies well-behaved}\nonumber\\
&=\frac{\mathrm {P}(\text{$v$ is intact})}{\sum_{B\subseteq V}\mathrm P(\text{$v$ is well-behaved}\mid \mathbb B = B)\cdot \mathrm P(\mathbb B=B)}=\frac{\mathrm {P}(\text{$v$ is intact})}{\sum_{B\subseteq V\setminus\{v\}} p(B)}\;.\label{eq:def-conditional-prob-intactness}
\end{align}

Let us illustrate the probabilistic intactness for some examples.

Consider the symmetric simple FBAS $(V,k)$ with $V=\{a,b,c,d\}$ and $k=3$. Lemma <ref> yields that the DSets are $\emptyset$, $V$, and all one-element subsets of $V$. Thus,

\begin{align}
\mathrm P(\text{$a$ is intact}) = p(\emptyset) + p(\{b\}) + p(\{c\}) + p(\{d\})\;,\label{eq:prob_intact1_basis1}
\end{align}

and similarly for the nodes $b$, $c$ and $d$.

Consider the FBAS from Example <ref>. As stated already in Example <ref>, the DSets are
$\emptyset$, $\{1,2,3\}$, $\{4,5,6\}$, $V\setminus\{7\}$ and $V$. Thus,

\begin{align*}
\mathrm {P}(\text{$v$ is intact})&=
\begin{cases}
\sum_{B\subseteq \{4,5,6\}}p(B),&\text{if $v\in\{1,2,3\}$},\\
\sum_{B\subseteq \{1,2,3\}}p(B),&\text{if $v\in\{4,5,6\}$},\\
\sum_{B\subseteq V\setminus\{7\}}p(B),&\text{if $v=7$}.
\end{cases}
\end{align*}

In particular, $\mathrm {P}(\text{$7$ is intact}\mid \text{$7$ is well-behaved}) = 1$ by equation (<ref>), i.e., node $7$ will not become befouled if it is well-behaved, independent from the actual probability distribution $p$. Note that this property holds for every FBAS that has a well-behaved node $v$ and a DSet that comprises all nodes except $v$. Another way to show that $\mathrm {P}(\text{$7$ is intact}\mid \text{$7$ is well-behaved})=1$ is by using the fact that $C=\{7\}$ is the greatest SCC (see Figure <ref>): Clearly, $C$ is the set of $\emptyset$-intact nodes of $(C, S|_C)$ and then Corollary <ref> implies that $7$ is intact whenever it is well-behaved.

Suppose that the FBAS is built by 4 organizations that each operate 3 nodes. We let $V=A\cup B\cup C\cup D$ with $A=\{a_1, a_2, a_3\}$ and likewise for the other organizations. We let $\mathcal O=\{A, B, C, D\}$ be the set of organizations. Similar to Example <ref>, we suppose that the quorum slices are built by first choosing 3 of the 4 organizations, and then choosing 2 nodes within each chosen organization. Formally, let

\begin{align*}
T&=\bigcup\nolimits_{\{O_1,O_2,O_3\}\in \mathcal P_3(\mathcal O)}\bigl\{M_1\cup M_2\cup M_3\mid M_i\in \mathcal P_2(O_i)\bigr\},
\end{align*}

with $\mathcal P_k(M)$ as in Definition <ref>. Now we define $S(v)=\{U\in T\mid v\in U\}$ for all $v\in V$.
The resulting set of quorums is obtained by picking 3 or 4 organizations, and then picking 2 or 3 nodes from each chosen organization. The FBAS has quorum intersection and it is easy to check that the corresponding DSets are given by $\emptyset$, $V$, each singleton set, and each set comprising a complete single organization.

Let us determine $\mathrm {P}(\text{$a_1$ is intact})$. The set of all $B\subseteq V$ such that there is a DSet $D$ with $B\subseteq D\subseteq V\setminus\{a_1\}$ is given by

\begin{align}
\bigl\{\emptyset, \{a_2\}, \{a_3\}\bigr\}\cup\mbox{}\bigcup\nolimits_{O\in \{B,C,D\}}\mathcal P(O)\setminus\{\emptyset\}.\label{eq:example_prob_intact_groups1}
\end{align}

Observe that all unions in (<ref>) are disjoint and hence

\begin{align}
\mathrm {P}(\text{$a_1$ is intact}) = p(\emptyset) + p(\{a_2\}) + p(\{a_3\}) + \sum_{O\in \{B,C,D\}}\ \sum_{\emptyset\not=O'\subseteq O}p (O').\label{eq:example_prob_intact_groups2}
\end{align}

Similar expressions can be derived for the other nodes in $V$ by symmetry.

Let us now discuss some interesting special cases for the distribution $p$.

§.§ At most one ill-behaved node

If at most one node can be ill-behaved, i.e, $p(B)=0$ for $|B|>1$, we have

\begin{align*}
\mathrm {P}(\text{$v$ is intact})&=p(\emptyset)+\sum\nolimits_{u\in U_v} p(\{u\})=1-\sum\nolimits_{u\in V\setminus U_v} p(\{u\}),
\end{align*}

where $U_v$ is the union of all DSets that do not contain $v$. Note that our assumption that $(V,S)$ has quorum intersection implies that $\emptyset$ is a DSet. Furthermore,

\begin{align}
\mathrm {P}(\text{$v$ is intact}\mid \text{$v$ is well-behaved})
&=\frac{p(\emptyset)+\sum_{u\in U_v} p(\{u\})}{p(\emptyset)+\sum_{u\in V\setminus\{v\}} p(\{u\})}\nonumber\\
&=\frac{p(\emptyset)+\sum_{u\in U_v} p(\{u\})}{1-p(\{v\})}\;.\label{eq:cond-prob-intactness-one-maximal}
\end{align}

[continuation of Example <ref>]
Suppose that

\begin{align*}
\end{align*}

By (<ref>), $\mathrm {P}(\text{$a$ is intact})=0.8$. Likewise, $\mathrm {P}(\text{$b$ is intact})=\mathrm {P}(\text{$c$ is intact})=0.9$ and $\mathrm {P}(\text{$d$ is intact})=1$. With (<ref>) we conclude furthermore that the conditional probability of each node to be intact given that it is well-behaved is $1$ because $U_v=V\setminus\{v\}$ for each node $v$.

Note that the latter property carries over to a large class of symmetric simple FBAS $(V,k)$: If $|V|-1\geq k\geq |V|/2 +1$, then Lemma <ref> implies that every one-element subset of $V$ is a DSet. We thus get $U_v=V\setminus \{v\}$ for every $v\in V$ and consequently $\mathrm {P}(\text{$v$ is intact}\mid \text{$v$ is well-behaved})=1$.

[continuation of Example <ref>]
Since the DSets are $\emptyset$, $\{1,2,3\}$, $\{4,5,6\}$, $V\setminus\{7\}$, and $V$, we obtain

\begin{align*}
\end{align*}

From this we conclude that

\begin{align*}
\mathrm {P}(\text{$v$ is intact})=
\begin{cases}
p(\emptyset)+p(\{4\})+p(\{5\})+p(\{6\})\;,&\text{if $v\in\{1,2,3\}$},\\
p(\emptyset)+p(\{1\})+p(\{2\})+p(\{3\})\;,&\text{if $v\in\{4,5,6\}$},\\
1-p(\{7\})\;,&\text{if $v=7$}.
\end{cases}
\end{align*}

§.§ Independent failures

Let us suppose that ill-behavior only occurs due to random and non-coordinated failures of nodes. We can model this case by assuming that the events of distinct nodes to be ill-behaved are independent, and that a single node $v$ becomes ill-behaved with probability $p_v$. Thus, for every $B\subseteq V$ we have

\begin{align*}
p(B)=\prod_{u\in B}p_u\cdot\prod_{u\in V\setminus B}(1-p_u)\;,
\end{align*}

and therefore

\begin{align*}
\mathrm {P}(\text{$v$ is intact})&=\sum_{\substack{B\subseteq V\\ \text{$\exists$ DSet $D$: $B\subseteq D\subseteq V\setminus\{v\}$}}} \prod_{u\in B}p_u\cdot\prod_{u\in V\setminus B}(1-p_u)\;.
\end{align*}

Note that
$$\sum_{B\subseteq V\setminus\{v\}}p(B)=\sum_{B\subseteq V\setminus\{v\}}\prod_{u\in B}p_u\cdot\prod_{u\in V\setminus B}(1-p_u)=1-p_v,$$

which is easy to show by induction. Then (<ref>) yields

\begin{align*}
\mathrm {P}(\text{$v$ is intact}\mid \text{$v$ is well-behaved})&=\frac{\mathrm {P}(\text{$v$ is intact})}{1-p_v}\;.
\end{align*}

[continuation of Example <ref>]
Suppose that

\begin{align*}
\end{align*}

then by (<ref>),

\begin{align*}
\mathrm {P}(\text{$a$ is intact})=0.8\cdot 0.9^2 + 0.8\cdot 0.1\cdot 0.9 + 0.8\cdot 0.9\cdot 0.1 + 0 = 0.792.
\end{align*}

\begin{align*}
\mathrm {P}(\text{$b$ is intact})&=\mathrm {P}(\text{$c$ is intact})=0.882,&\mathrm {P}(\text{$d$ is intact})&=0.954.
\end{align*}

For the conditional probabilities we have

\begin{align*}
\mathrm {P}(\text{$a$ is intact}\mid \text{$a$ is well-behaved})&=0.99,\\
\mathrm {P}(\text{$b$ is intact}\mid \text{$b$ is well-behaved})&=0.98,\qquad\mbox{(same for $c$)}\\
\mathrm {P}(\text{$d$ is intact}\mid \text{$d$ is well-behaved})&=0.954.
\end{align*}

Observe that the conditional probability for $a$ to be intact is higher than for the other three nodes. This is because we assume that $a$ is well-behaved and therefore it can only become befouled if at least one of the other nodes is ill-behaved. However, these nodes are more likely to be well-behaved than node $a$.

[continuation of Example <ref>]
For node $1$ there are precisely two DSets $D$ with $D\subseteq V\setminus\{1\}$, namely the sets $\emptyset$ and $\{4,5,6\}$. Then

\begin{align*}
\mathrm {P}(\text{$1$ is intact})&=\textstyle{\sum_{B\subseteq\{4,5,6\}}\prod_{u\in B}p_u\cdot\prod_{u\in V\setminus B}1-p_u}\\&=(1-p_1)\cdot(1-p_2)\cdot(1-p_3)\cdot(1-p_7),
\end{align*}

\begin{align*}
\mathrm {P}(\text{$1$ is intact}\mid \text{$1$ is well-behaved})&=(1-p_2)\cdot(1-p_3)\cdot(1-p_7).
\end{align*}

The computation is similar for the other nodes in $V\setminus\{7\}$.

§.§ Grouping of nodes

Let us generalize the previous case by assuming that the nodes are associated with entities or organizations (as in Example <ref> or Example <ref>) that act independently. Therefore, we can assume that the ill-behavior of different organizations is statistically independent. More precisely, we assume a partitioning $\mathcal O$ of $V$, where every element of the partitioning consists of the nodes of a single organization, and a probability distribution $p_O$ over $\mathcal P(O)$ for every $O\in \mathcal O$. Then we define

\begin{align*}
p(B)=\prod_{O\in \mathcal O} p_O(B\cap O).
\end{align*}

In practice the quorum slices of nodes within one organization will presumably be set up in a way that all nodes of the organization trust each other; equivalently, for every organization there is an SCC of the trust graph containing all nodes of the organization. This implies that every trust cluster of the FBAS is a union of organizations due to Lemma <ref>. In this case we can simplify the computation of the probabilistic intactness of a node within a trust cluster – it is determined completely by the nodes of the trust cluster and independent from the nodes outside the trust cluster.

Suppose that for every organization $O\in \mathcal O$ there is an SCC that contains $O$. Let $Z$ be a trust cluster and $v\in Z$. Then

\begin{align*}
\mathrm P(\text{$v$ is intact})=\sum_{\substack{B\subseteq Z\\ \text{$\exists$ DSet $D$ of $(Z, S|_Z)$: $B\subseteq D\subseteq Z\setminus\{v\}$}}} \prod_{O\in \mathcal O, O\subseteq Z}p_O(B\cap O)\;.
\end{align*}

First observe that Lemma <ref> implies that for every organization $O\in \mathcal O$ either $O\subseteq Z$ or $O\subseteq V\setminus Z$. Let us distinguish between these two kinds of organizations and put $\mathcal O_\mathrm {in}=\{O\in \mathcal O\mid O\subseteq Z\}$ and $\mathcal O_\mathrm {out}=\{O\in \mathcal O\mid O\subseteq V\setminus Z\}$. Then $\mathcal O=\mathcal O_\mathrm{in}\cup \mathcal O_\mathrm{out}$. We derive

\begin{align*}
&\mathrm {P}(\text{$v$ is intact})=\sum_{\substack{B\subseteq V\\ \text{$v$ is $B$-intact in $(V,S)$}}} p(B)\\
&=\sum_{\substack{B\subseteq V\\ \text{$v$ is $B\cap Z$-intact in $(Z,S|_Z)$}}} p(B)\tag{by Theorem~\ref{theo:intact-SCC}}\\
&=\sum_{\substack{B_\mathrm{in}\subseteq Z\\ \text{$v$ is $B_\mathrm{in}$-intact in $(Z,S|_Z)$}}} \sum_{B_\mathrm{out}\subseteq V\setminus Z}p(B_\mathrm{in}\cup B_\mathrm{out})\\
&=\sum_{\substack{B_\mathrm{in}\subseteq Z\\ \text{$v$ is $B_\mathrm{in}$-intact in $(Z,S|_Z)$}}} \sum_{B_\mathrm{out}\subseteq V\setminus Z}\ \ \prod_{O\in \mathcal O} p_O((B_\mathrm{in}\cup B_\mathrm{out})\cap O)\\
&=\sum_{\substack{B_\mathrm{in}\subseteq Z\\ \text{$v$ is $B_\mathrm{in}$-intact in $(Z,S|_Z)$}}} \sum_{B_\mathrm{out}\subseteq V\setminus Z}\Bigl(\prod_{O\in \mathcal O_\mathrm{in}} p_O(B_\mathrm{in}\cap O)\Bigr)\cdot\Bigl(\prod_{O\in \mathcal O_\mathrm{out}} p_O(B_\mathrm{out}\cap O)\Bigr)\\
&=\sum_{\substack{B_\mathrm{in}\subseteq Z\\ \text{$v$ is $B_\mathrm{in}$-intact in $(Z,S|_Z)$}}}\Bigl(\prod_{O\in \mathcal O_\mathrm{in}} p_O(B_\mathrm{in}\cap O)\Bigl)\cdot\sum_{B_\mathrm{out}\subseteq V\setminus Z}\Bigl(\prod_{O\in \mathcal O_\mathrm{out}} p_O(B_\mathrm{out}\cap O)\Bigr)
\end{align*}

It suffices to show that $\sum_{B_\mathrm{out}\subseteq V\setminus Z}\prod_{O\in \mathcal O_\mathrm{out}} p_O(B_\mathrm{out}\cap O)=1$. Let $O_\mathrm{out}=\{O_1, \ldots, O_n\}$ and observe that $\bigcup_{i=1}^n O_i=V\setminus Z$. Then

\begin{align*}
\sum\nolimits_{B_\mathrm{out}\subseteq V\setminus Z}\prod\nolimits_{O\in \mathcal O_\mathrm{out}} p_O(B_\mathrm{out}\cap O)&=\sum\nolimits_{B_1\subseteq O_1, \ldots, B_n\subseteq O_n}\prod\nolimits_{i=1}^n p_{O_i}(B_i)\\
&=\prod\nolimits_{i=1}^n \sum\nolimits_{B_i\subseteq O_i} p_{O_i}(B_i)=1,
\end{align*}

which concludes the proof.

Note that Lemma <ref> also applies to the probability distributions discussed in Section <ref> as they are special cases of the probability distributions in this section.

[continuation of Example <ref>]
Let us study our example for the partitioning $\mathcal O$. For every $O\in\mathcal O$ let $e_O=p_O(\emptyset)$. Then we can reformulate the right hand side of (<ref>) as

\begin{align*}
&\bigl(e_A + p_A(\{a_2\}) + p_A(\{a_3\})\bigr)e_B e_C e_D
+ \sum_{O\in \{B,C,D\}}\ \sum_{\emptyset\not=O'\subseteq O}p_O(O')\prod_{O''\in \mathcal O\setminus \{O\}}e_{O''}\\
&=\bigl(e_A + p_A(\{a_2\}) + p_A(\{a_3\})\bigr)e_B e_C e_D
+ \sum_{O\in \{B,C,D\}}\ (1-e_O)\prod_{O''\in \mathcal O\setminus \{O\}}e_{O''}\tag{$\star$}\\
&=\bigl(e_A + p_A(\{a_2\}) + p_A(\{a_3\})\bigr)e_B e_C e_D\\
&\phantom{=\ }\mbox{}+ (1-e_B)e_A e_C e_D+(1-e_C)e_A e_B e_D + (1-e_D)e_A e_B e_C.
\end{align*}

At ($\star$) we used that fact that $p_O$ is a probability distribution over $\mathcal P(O)$ and therefore $\sum_{\emptyset\not=O'\subseteq O}p_O(O') = 1-e_O$.

Suppose that $e_A=e_B=e_C=e_D$ and let us refer to this value as $e$. Then

\begin{align}
\mathrm P(\text{$a_1$ is intact})=e^3\bigl(p_A(\{a_2\}) + p_A(\{a_3\})+3-2e\bigr).\label{eq:prob_intact3}
\end{align}

§.§ Grouping of nodes with Byzantine failures

Finally, let us consider a specialization of the previous case and assume a simple model of the probability distribution $p_O$ of every element $O\in \mathcal O$. Our model is based on the assumption that nodes within an organization can become ill-behaved for two reasons: (i) random failures that are statistically independent and (ii) the organization experiences a Byzantine fault and all nodes of the organization become ill-behaved.

For every $O\in \mathcal O$ we presuppose the probability $q_O$ (the probability of a single node of the organization to fail randomly) and the probability $r_O$ (the probability of all the nodes of the organization $O$ to become Byzantine). Then for every $B\subseteq O$ we define

\begin{align*}
p_O(B)=\begin{cases}r_O + (1-r_O)\cdot (q_O)^{|O|}\;,&\text{if $B=O$,}\\(1-r_O)\cdot (q_O)^{|B|}\cdot (1-q_O)^{|O|-|B|}\;,&\text{otherwise.}\end{cases}
\end{align*}

Observe that $p_O$ is indeed a probability distribution.

[continuation of Example <ref>]
Let $q_O$ and $r_O$ be the probabilities for organization $O$. Let us suppose that all $q_O$ are identical for each organization and likewise for $r_O$, and let us simply refer to these values as $q$ and $r$. Then $e=p_O(\emptyset)=(1-r)\cdot (1-q)^3$. Furthermore, $p_A(\{a_2\})=p_A(\{a_3\})=(1-r)\cdot q\cdot (1-q)^2$. Then from (<ref>) we derive

\begin{align*}
\mathrm P(\text{$a_1$ is intact})=(1-r)^3 (1-q)^9\bigl(2(1-r) q (1-q)^2+3-2(1-r) (1-q)^3\bigr)\;.
\end{align*}

For example, if $q=0.1$ and $r=0.01$, then $\mathrm P(\text{$a_1$ is intact})\approx 0.65$. By symmetry all nodes have the same probability to be intact.

The FBAS in Example <ref> is not the only way to arrange four organizations with three nodes per organization. We could also lay out the nodes as a symmetric simple FBAS. We will study this FBAS in the following example.

Consider the symmetric simple FBAS $(V, 8)$, where $V=A\cup B\cup C\cup D$ is defined as in Example <ref>. From Lemma <ref> we know that the DSets are $V$ and every subset of $V$ having at most 3 elements. Therefore, for every $v\in V$,

\begin{align*}
\mathrm P(\text{$v$ is intact}) = \sum_{B\subseteq V\setminus\{v\}, |B|\leq 3}p(B).
\end{align*}

This sum is combinatorially more complex than the expression in Example <ref>. However, assuming identical probability values $q$ and $r$ for each organization as in Example <ref>, we can group the sets $B$ into categories as many of them have the same value for $p(B)$. We consider the following five categories of sets $B$: (i) having $0$ members, (ii) having $1$ member, (iii) having $2$ members, (iv) having $3$ members, not all in one organization, and (v) a complete organization. Then we find that there is 1 set in category (i), 11 sets in category (ii), 55 sets in category (iii), 162 sets in category (iv), and 3 sets in category (v). For example, all sets in category (iii) satisfy $p(B)=(1-r)^4\cdot q^2\cdot(1-q)^{10}$, so that we obtain

\begin{align*}
\mathrm P(\text{$v$ is intact}) &= (1-r)^4\cdot(1-q)^{12} + 11\cdot (1-r)^4\cdot q\cdot(1-q)^{11} \\
&\phantom{=\ }\mbox{}+ 55\cdot (1-r)^4\cdot q^2\cdot(1-q)^{10} + 162\cdot (1-r)^4\cdot q^3\cdot(1-q)^{9}\\
&\phantom{=\ }\mbox{}+3\cdot (1-r)^3\cdot(1-q)^{9}\cdot\bigl(r + (1-r)\cdot q^3\bigr).
\end{align*}

For the values $q=0.1$ and $r=0.01$ as in Example <ref> we get $\mathrm P(\text{$v$ is intact})\approx 0.86$ for every $v\in V$. We observe that the probability that a node becomes befouled in case of the symmetric simple FBAS is significantly smaller (by a factor of approximately 2.5) than for the hierarchical FBAS in Example <ref>.

§ CONCLUDING REMARKS

In this paper we have discussed the main concepts of the federated Byzantine agreement system as defined by Mazières <cit.>, in particular quorum and quorum intersection, and intactness of nodes. We have illustrated these concepts with several examples, ranging from small “academic” cases to the greatest strongly connected component of the current Stellar network; see Example <ref>. In our discussion of intactness, we have clarified the relation between Mazières' original definition and the more recent definitions in <cit.>, and we have introduced the subslice property as a condition for equivalence of the two concepts; see Section <ref>.

We have treated the problems of quorum enumeration and quorum intersection as well as the intactness of nodes from an algorithmic point of view. We have shown that the quorum split decision problem is NP-complete even for the special class of simple FBAS, which we introduced in this paper; see Definition <ref>. Based on the work of Lachowski <cit.>, we have derived algorithms for quorum enumeration, checking quorum intersection, and computing intact nodes. Some computed examples with our implementations of these algorithms in the Python package Stellar Observatory[<https://github.com/andrenarchy/stellar-observatory>] are given is this paper; see, e.g., Example <ref> and Figure <ref>. In order to derive the algorithms, prove their correctness and reduce their complexity we have introduced several new concepts including the trust graph and trust clusters of an FBAS; see Section <ref>.

In the final section of this paper we have treated intactness from a probabilistic point of view, and we have studied the probability that a node is intact in different scenarios of ill-behaved nodes. Of particular interest in this context is the intactness probability in hierarchical FBAS settings as the ones in Example <ref>, which we then discussed in Examples <ref>, <ref>, and <ref>.

In Example <ref> we have shown that from the viewpoint of the intactness probability, the symmetric simple FBAS is superior to a hierarchical FBAS. This observation not only holds for the simplified probability distribution we considered, but in fact for every probability distribution $p$, which is immediately clear from the definition of probabilistic intactness in (<ref>): The set of DSets in Example <ref> is a proper subset of the set of DSets in Example <ref>. Therefore, no probabilistic intactness in the hierarchical FBAS exceeds the corresponding probabilistic intactness in the symmetric simple FBAS.

In Sections <ref> and <ref> we have shown that intersection and intactness properties of the greatest SCC (and more generally any trust cluster) of an FBAS are independent from the remainder of the FBAS. Therefore, this component of the FBAS can be studied in isolation, and this property carries over to probabilistic intactness; see Lemma <ref>. A similar argument as in Example <ref> then shows that
the probabilistic intactness of nodes in the hierarchical setup of the greatest SCC of the FBAS in Example <ref>
(with quorum slices containing 11, 12 or 13 nodes) will not be larger than in a symmetric simple FBAS with $k=12$.

§ ACKNOWLEDGEMENT

This work was supported by a grant in the SDF Academic Research Program.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

New York, NY, USA

journaltitleJ. ACM
titleAsynchronous Consensus and Broadcast Protocols

New York, NY, USA

journaltitleACM Trans. Comput. Syst.
titlePractical Byzantine Fault Tolerance and Proactive Recovery

Addison-Wesley Publishing Company

titleDistributed Systems: Concepts and Design

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

booktitle22nd Int. Conf. on Principles of Distributed Systems (OPODIS 2018)
titleFederated Byzantine Quorum Systems

W. H. Freeman
Co., San Francisco, Calif.

titleComputers and Intractability

Plenum Press, New York

booktitleComplexity of Computer Computations
seriesThe IBM Research Symposia Series
titleReducibility Among Combinatorial Problems.

titleComplexity of the quorum intersection property of the Federated Byzantine Agreement System

New York, NY, USA

journaltitleACM Trans. Program. Lang. Syst.
titleThe Byzantine Generals Problem

booktitleProceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP 2019)
titleFast and Secure Global Payments with Stellar

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

booktitle33rd Int. Symp. on Distributed Computing (DISC 2019)
titleStellar Consensus by Instantiation

ACM, New York

booktitleSTOC '97 (El Paso, TX)
titleByzantine quorum systems

journaltitleSIAM J. Comput.
titleThe load and availability of Byzantine quorum systems

noteWhite Paper Draft
titleThe Stellar Consensus Protocol: A Federated Model for Internet-level Consensus

journaltitleCryptography Mailing list at https://metzdowd.com
titleBitcoin: A Peer-to-Peer Electronic Cash System

journaltitleSIAM J. Comput.
titleThe load, capacity, and availability of quorum systems

New York, NY, USA

journaltitleJ. ACM
titleReaching Agreement in the Presence of Faults

journaltitleSIAM J. Comput.
titleDepth-first search and linear graph algorithms

Morgan & Claypool Publishers

seriesSynthesis Lectures on Distributed Computing Theory
titleQuorum Systems: With Applications to Storage and Consensus