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

【Abstract】 The optimistic electronic contract signing protocol is a kind of typical security protocols for fair electronic contracts exchange,which is more complicated,and brings more challenges for its formal analysis.Model checking is an efficient way to analyze security protocols,where modeling the protocol and its running environment exactly and comprehensively is the key issue and starting point.In this paper,a novel model is presented,and illustrated by Garays’ protocol,where the honest principals,dishonest principals,and different kinds of communication channels are modeled as finite automata respectively.更多还原