Strand Spaces的公平交换
Fair Exchange in Strand Spaces
摘要：
许多加密协议旨在协调主体之间的状态更改。交换协议协调向参与者提供新的价值，例如，增加他们拥有的价值。交换协议是公平的，如果它确保新价值的传递是平衡的：如果一个参与者通过协议获得了新的所有权，那么所有其他参与者也会这样做。公平交换需要进度假设，不像其他一些协议属性。串空间模型是密码协议设计和验证的框架。串是协议的单个会话中单个主体的本地行为。捆绑是从协议链和对手活动构建的部分有序的全局执行。对于公平交换协议，串空间模型需要两个补充。首先，我们将状态视为事实的多重集合，并且我们允许链通过多重集合重写来引起这种状态的变化。第二，进度假设规定某些通道是顺从的，并保证传递消息，而某些主体被假设不会在某些关键步骤停止。这种方法导致的正确性证明，干净地分离协议属性，如认证和机密性，从管理状态演化的不变量。G.王的最近的公平交换协议说明了这种方法。
英文摘要：
Many cryptographic protocols are intended to coordinate state changes among principals. Exchange protocols coordinate delivery of new values to the participants, e.g. 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. Fair exchange requires progress assumptions, unlike some other protocol properties. The strand space model is a framework for design and verification of cryptographic protocols. A strand is a local behavior of a single principal in a single session of a protocol. A bundle is a partially ordered global execution built from protocol strands and adversary activities. The strand space model needs two additions for fair exchange protocols. First, we regard the state as a multiset of facts, and we allow strands to cause changes in this state via multiset rewriting. Second, progress assumptions stipulate that some channels are resilient-and guaranteed to deliver messages-and some principals are assumed not to stop at certain critical steps. This method leads to proofs of correctness that cleanly separate protocol properties, such as authentication and confidentiality, from invariants governing state evolution. G. Wang's recent fair exchange protocol illustrates the approach.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
