State and Progress in Strand Spaces: Proving Fair Exchange
Many cryptographic protocols are intended to coordinate state changes among principals. Exchange protocols, for instance, coordinate delivery of new values to the participants, i.e., additions to the set of values they possess. An exchange protocol is fair if it ensures that delivery of new values is balanced: If one participant obtains a new possession via the protocol, then all other participants will, too. Understanding this balanced coordination of different principals in a distributed system requires relating (long-term) state to (short-term) protocol activities. Fair exchange also requires progress assumptions. In this paper, the authors adapt the strand space framework to protocols, such as fair exchange, that coordinate state changes.