在目前提出的电子合同签订协议中，乐观合同签订协议由于运行效率高而具有应用前景。对于乐观签订协议的设计和验证是一个研究热点，除了常用的理论和方法，人们还提出了一些新的手段。一些典型的协议已经成为各种分析验证方法和工具的试验台。　　 乐观合同签订协议通常包括主协议和子协议，由于主协议消息交换轮次和子协议设计的区别，表现为不同的结构。本文从结构上对协议的各种安全属性进行了分析。提出了一种协议结构的图形表示，直观表现了协议动作之间的关系，以此推出了协议满足安全属性的条件，给出了可能满足安全属性的协议结构，证明了一个可行的乐观合同签订协议至少需要四轮消息交换。　　 由于结构分析忽略了消息的具体内容，而且只能检验一次协议运行的情况，所以在进行协议分析时需要与其它工具相结合。根据结构分析的结果，本文用模型检测工具SPIN对不满足公平性的协议进行了验证，一方面证明了结构分析的正确性，一方面用反例得到了攻击轨迹。对结构分析中没发现问题的协议也进行了验证，发现了用结构分析不能发现的问题。本文详细描述了ASW协议的建模和验证过程，针对所发现的安全隐患提出了改进方案。