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

A Finite Automata Model for Optimistic Contract Signing Protocols

作　　者：缪裕青[1] 常亮[1] 

机构地区：[1]桂林电子工业学院计算机系,广西桂林541004

出　　处：《桂林电子工业学院学报》2004年第5期27-31,共5页Journal of Guilin Institute of Electronic Technology

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

关 键 词：电子合同签订协议 乐观公平交换 模型 有限状态机 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]