About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
Journal of Computer Security
Paper
Polynomial liveness
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.