Note: [*] A preliminary version of this article appeared in the Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW), pp. 160–174.
Abstract: Important properties of many protocols are liveness or availability, i.e., that something good happens now and then. In asynchronous scenarios, these properties depend on the scheduler, which is usually considered to be fair in this case. The standard definitions of fairness and liveness are based on infinite sequences. Unfortunately, this cannot be applied to most cryptographic protocols since one must restrict the adversary and the runs as a whole to length polynomial in the security parameter. We present the first general definition of polynomial fairness and liveness in asynchronous scenarios which can cope with cryptographic protocols. Furthermore, our definitions provide a link to the common approach of simulatability which is used throughout modern cryptography: 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.
