|
|||||
|
|
| 基于Spin的SET协议模型检测研究 | |
| 引用本文： | 陈道喜,戎玫,张广泉.基于Spin的SET协议模型检测研究[J].计算机工程与科学,2009,31(9). |
| 作者姓名： | 陈道喜 戎玫 张广泉 |
| 作者单位： | 1. 苏州大学计算机科学与技术学院,江苏,苏州,215006;苏州技师学院,江苏,苏州,215009 2. 暨南大学深圳旅游学院,广东,深圳,518053 3. 苏州大学计算机科学与技术学院,江苏,苏州,215006;中国科学院计算机科学国家重点实验室,北京,100080 |
| 基金项目： | 中国科学院计算机科学国家重点实验室开放课题资助项目，江苏省高校自然科学研究资助项目 |
| 摘 要： | 模型检测技术已成功地运用于验证复杂系统的性质。本文提出运用Promela语言对电子商务协议进行建模的方法,对比分析了有无入侵者时简化的SET协议的运行情况。运用Spin模型检测工具,对SET协议的Promela模型进行了检测,对电子商务协议中的关键性质认证性和保密性进行了分析与检测,发现了协议中的缺陷。 |
| 关 键 词： | Spin SET协议 Promela 模型检测 |
Model Checking of the SET Protocol Using Spin |
|
| CHEN Dao-xi,RONG Mei,ZHANG Guang-quan.Model Checking of the SET Protocol Using Spin[J].Computer Engineering & Science,2009,31(9). | |
| Authors: | CHEN Dao-xi RONG Mei ZHANG Guang-quan |
| Abstract: | Model checking has been successfully applied to verify the properties of complex systems.An approach of applying the Promela modeling language is introduced to model e-commerce protocols in this paper.According to the simplified SET protocol,we compare the running statuses with and without an intruder.Through model checking of the SET protocol using the model checker Spin,we analyze the critical properties of e-commerce protocols such as confidentiality and authentication.The verification shows that there are some defects in the protocol. |
| Keywords: | Spin Promela |
| 本文献已被 万方数据 等数据库收录！ | |