|
|
|---|
|
|
|
|---|
Messages.
We model the network that connects the validators as eventually reliable with authenticated senders, as commonly assumed in the BFT literature. The only kind of network communication that is relevant to our model is the exchange of certificates among validators. Since we model the exchange of proposals and signatures at an abstract level here, there are no explicit proposals, signatures, etc. exchanged in messages. Instead, validators may (nondeterministically) broadcast certificates, as formalized in the state transitions of the system. Those are not immediately delivered to the other validators, so we need to model the situation in which a certificate has been broadcast but not yet delivered, to at least some of the validators (others may have received it already). Thus, we model messages as consisting of certificates, augmented with destination addresses (one per message).