Polynomial fairness and liveness
- 25 June 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
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.Keywords
This publication has 4 references indexed in Scilit:
- A model for asynchronous reactive systems and its application to secure message transmissionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Automatic verification of pipelined microprocessor controlPublished by Springer Nature ,1994
- Defining livenessInformation Processing Letters, 1985
- Protocols for secure computationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982