BW多方合同签署协议的公平性验证

摘要

N方的合同签署协议包含多个子协议，并允许N-1个缔约方违背协议的规定进行不诚实的操作，其形式化分析遇到了新的挑战。利用Paulson归纳法，给出了BW多方合同签署协议的形式化描述，利用定理证明工具Isabelle／HOL，证明了BW协议的公平性定理。