论文部分内容阅读
与密钥分发和认证协议相比，电子合同签订协议的形式化分析遇到了新的挑战。以Asokan、Shoup和Waidner提出的乐观合同签订协议为例，在对协议进行建模以及对相应的安全性质进行形式化描述的基础上，用符号模型检验器SMV对公平性、适对性和无滥用性进行了分析，检测出了相关的缺陷。表明了用SMV对电子合同签订协议进行符号模型分析的有效性。