Polynomial Fairness and Liveness

Important properties of many protocols are liveness or availability, i.e., that something good happens now and then. In asynchronous scenarios these properties obviously depend on the scheduler, which is usually considered to be fair in this case. Unfortunately, the standard definitions of fairness and liveness based on infinite sequences cannot be applied for most cryptographic protocols since one must restrict the adversary and the runs as a whole to polynomial length. We present the first general definition of polynomial fairness and liveness in asynchronous scenarios which is suited to cope with arbitrary cryptographic protocols. Furthermore, our definitions provide a link to the common approach of simulatability which is used throughout modern cryptography, and we show that polynomial liveness is maintained under simulatability. As an example we present an abstract specification and a secure implementation of secure message transmission with reliable channels, and prove them to fulfill the desired liveness property, i.e., reliability of messages.