Many decentralized systems rely on flooding protocols for message dissemination. In such a protocol, the sender of a message sends it to a randomly selected set of peers. These peers again send the message to their randomly selected peers, until every network participant has received the message. This type of protocols clearly fail in face of an adaptive adversary who can simply corrupt all peers of the sender and thereby prevent the message from being delivered. Nevertheless, flooding protocols are commonly used within protocols that aim to be cryptographically secure, most notably in blockchain protocols. While it is possible to revert to static corruptions, this gives unsatisfactory security guarantees, especially in the setting of a blockchain that is supposed to run for an extended period of time. To be able to provide meaningful security guarantees in such settings, we give precise semantics to what we call $$\delta $$ -delayed adversaries in the Universal Composability (UC) framework. Such adversaries can adaptively corrupt parties, but there is a delay of time $$\delta $$ from when an adversary decides to corrupt a party until they succeed in overtaking control of the party. Within this model, we formally prove the intuitive result that flooding protocols are secure against $$\delta $$ -delayed adversaries when $$\delta $$ is at least the time it takes to send a message from one peer to another plus the time it takes the recipient to resend the message. To this end, we show how to reduce the adaptive setting with a $$\delta $$ -delayed adversary to a static experiment with an Erdős-Rényi graph. Using the established theory of Erdős-Rényi graphs, we provide upper bounds on the propagation time of the flooding functionality for different neighborhood sizes of the gossip network. More concretely, we show the following for security parameter $$\kappa $$ , point-to-point channels with delay at most $$\varDelta $$ , and n parties in total, with a sufficiently delayed adversary that can corrupt any constant fraction of the parties: If all parties send to $$\varOmega (\kappa )$$ parties on average, then we can realize a flooding functionality with maximal delay $$\mathcal {O}\bigl (\varDelta \cdot \log (n) \bigr )$$ ; and if all parties send to $$\varOmega \bigl ( \sqrt{\kappa n} \bigr )$$ parties on average, we can realize a flooding functionality with maximal delay $$\mathcal {O}(\varDelta )$$ .

Fault-tolerant distributed systems move the trust in a single party to a majority of parties participating in the protocol. This makes blockchain based crypto-currencies possible: they allow parties to agree on a total order of transactions without a trusted third party. To trust a distributed system, the security of the protocol and the correctness of the implementation must be indisputable. We present the first machine checked proof that guarantees both safety and liveness for a consensus algorithm. We verify a Proof of Stake (PoS) Nakamoto-style blockchain (NSB) protocol, using the foundational proof assistant Coq. In particular, we consider a PoS NSB in a synchronous network with a static set of corrupted parties. We define execution semantics for this setting and prove chain growth, chain quality, and common prefix which together imply both safety and liveness.