` 10 D. Mazieres well-behaved / Local property of nodes, independent of other nodes (except for ill-behaved the validity of slice selection). intact / Property of nodes given their quorum slices and a particular set befouled of ill-behaved nodes. Befouled nodes are ill-behaved or depend, possibly indirectly, on too many ill-behaved nodes. correct / Property of nodes given their quorum slices, a concrete protocol, failed and actual network behavior. The goal of a consensus protocol is to guarantee correctness for all intact nodes. Fig. 8. Keyproperties of FBAS nodes greater overlap, meaning fewer failed node sets B will undermine quorum intersection whendeleted. On the other hand, bigger slices are more likely to contain failed nodes, endangering quorum availability. The smallest DSet containing all ill-behaved nodes may encompass well-behaved nodes as well, reflecting the fact that a sufficiently large set of ill-behaved nodes can cause well-behaved nodes to fail. For instance, in Figure 3, the smallest DSet contain- ing v and v is {v ,v ,v ,v }. The set of all nodes, V, is always a DSet, as an FBAS 5 6 5 6 9 10 ⟨V,Q⟩vacuouslyenjoysquorumintersectiondespiteVand,byspecialcase,alsoenjoys quorum availability despite V. The motivation for the special case is that given suffi- ciently many ill-behaved nodes, V may be the smallest DSet to contain all ill-behaved ones, indicating a scenario under which no protocol can guarantee anything better than complete system failure. The DSets in an FBAS are determined a priori by the quorum function Q. Which nodesarewell-andill-behaveddependsonruntimebehavior,suchasmachinesgetting compromised.TheDSetswecareaboutarethosethatencompassallill-behavednodes, as they help us distinguish nodes that should be guaranteed correct from ones for which such a guarantee is impossible. To this end, we introduce the following terms: Definition (intact). A node v in an FBAS is intact iff there exists a DSet B containing all ill-behaved nodes and such that v ∉ B. Definition (befouled). A node v in an FBAS is befouled iff it is not intact. Abefouled node v is surrounded by enough failed nodes to block its progress or poi- sonitsstate, even if v itself is well-behaved. No FBAS can guarantee the correctness of abefoulednode.However,anoptimalFBASguaranteesthateveryintactnoderemains correct. Figure 8 summarizes the key properties of nodes. The following theorems fa- cilitate analysis by showing that the set of befouled nodes is always a DSet in an FBAS with quorum intersection. THEOREM1. LetU beaquoruminFBAS⟨V,Q⟩,letB ⊆Vbeasetofnodes,andlet ¨ ¨ ¨ B U =U⧵B.IfU ≠çthenU isaquorumin⟨V,Q⟩ . PROOF. Because U is a quorum, every node v ∈ U has a q ∈ Q(v) such that q ⊆ U. SinceU¨ ⊆ U,itfollowsthateveryv ∈ U¨ hasaq ∈ Q(v)suchthatq⧵B ⊆ U¨.Rewriting with deletion notation yields ∀v ∈ U¨,∃q ∈ QB(v) such that q ⊆ U¨, which, because U¨ ⊆ V⧵B,meansthatU¨ isaquorumin⟨V,Q⟩B. THEOREM2. If B and B are DSets in an FBAS ⟨V,Q⟩ enjoying quorum intersec- 1 2 tion, then B = B ∩B is a DSet, too. 1 2 PROOF. LetU =V⧵B andU =V⧵B .IfU =ç,thenB =VandB=B (aDSet), 1 1 2 2 1 1 2 so we are done. Similarly, if U = ç, then B = B , and we are done. Otherwise, note 2 1