基于小系统理论的简化 SET 协议

摘要：

基于Lu＆Smolka的SET协议支付过程简化模型，在小系统理论的基础上，运用Promela语言对协议进行形式化建模，采用线性时态逻辑LTL公式对协议的认证性进行形式化描述。在网络环境被入侵者控制的假设下，运用SPIN发现攻击；采用atomic和Bit-state hashing等优化策略，降低模型检测的复杂性，提高验证效率；最后针对协议存在的漏洞提出协议改进方案。

关键词：小系统理论、SET协议、模型检测、SPIN、认证性

分类号：TP393(计算技术、计算机技术)

资助基金：江西省科技计划项目20123 BBE50106

在线出版日期：2015-01-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：97-102