基于Spin的SET协议模型检测研究

作者：陈道喜; 戎玫; 张广泉

来源：计算机工程与科学, 2009, (09): 17-19+22.

• Spin
• SET协议
• Promela
• 模型检测 Spin
• SET protocol
• model checking

模型检测技术已成功地运用于验证复杂系统的性质。本文提出运用Promela语言对电子商务协议进行建模的方法,对比分析了有无入侵者时简化的SET协议的运行情况。运用Spin模型检测工具,对SET协议的Promela模型进行了检测,对电子商务协议中的关键性质认证性和保密性进行了分析与检测,发现了协议中的缺陷。

• 单位
  中国科学院; 计算机科学国家重点实验室; 苏州大学; 暨南大学深圳旅游学院