Synchrony amplification

Various protocols in the cryptography and distributed systems literature assume some notion of time: One major (but not the only) example are “synchronous” models which assume that a protocol is executed in a well-defined sequence of rounds with round switches that occur (almost) simultaneously at the parties. In many of the considered models, the notion of time is either implicit, or it is closely interweaved with other mechanics of the model such that formally proving even simple statements becomes a tedious task. In this work, we develop an abstract formal model that captures exactly how the availability of clocks with “weak” synchrony guarantees can benefit parties; in particular, we show how - and at what cost - the “synchrony” of clocks can be improved. Proofs in this model are simple and the statements transfer to all models that satisfy the abstraction. The main contribution of this paper is not the actual statements we prove (which mostly verify folklore beliefs), but the formal model that follows the construction paradigm of abstract cryptography and allows to state these proofs in a simple yet rigorous manner. Indeed, the paper is a step towards a treatment of synchronous cryptographic protocols in this constructive sense.