乐观电子合同签订协议的一种有限状态机模型

乐观电子合同签订协议是一类典型的安全协议，用于在两个或多个主体之间公平高效地实现电子合同签订。与其它类型的安全协议相比，乐观电子合同签订协议更为复杂，从而为其形式化分析带来了一定困难。模型检验是一类有效的形式化分析方法，应用模型检测方法分析安全协议时，前提和关键是对协议及其执行环境进行准确和全面的建模。