| 乐观电子合同签订协议的一种有限状态机模型 |
| |
| 引用本文： | 缪裕青,常亮. 乐观电子合同签订协议的一种有限状态机模型[J]. 桂林电子科技大学学报, 2004, 24(5): 27-31 |
| |
| 作者姓名： | 缪裕青 常亮 |
| |
| 作者单位： | 桂林电子工业学院,计算机系,广西,桂林,541004;桂林电子工业学院,计算机系,广西,桂林,541004 |
| |
| 摘 要： | 乐观电子合同签订协议是一类典型的安全协议,用于在两个或多个主体之间公平高效地实现电子合同签订。与其它类型的安全协议相比,乐观电子合同签订协议更为复杂,从而为其形式化分析带来了一定困难。模型检验是一类有效的形式化分析方法,应用模型检测方法分析安全协议时,前提和关键是对协议及其执行环境进行准确和全面的建模。
|
| 关 键 词： | 电子合同签订协议 乐观公平交换 模型 有限状态机 |
| 文章编号： | 1001-7437(2004)05-27-05 |
| 修稿时间： | 2004-09-15 |
A Finite Automata Model for Optimistic Contract Signing Protocols |
| |
| MIAO Yu-qing,CHANG Liang. A Finite Automata Model for Optimistic Contract Signing Protocols[J]. Journal of Guilin University of Electronic Technology, 2004, 24(5): 27-31 |
| |
| Authors: | MIAO Yu-qing CHANG Liang |
| |
| 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. |
| |
| Keywords: | electronic contract signing protocol optimistic fair exchange modeling finite automata |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
