电子商务安全协议及其非单调动态逻辑验证  

The Secure Electronic Transactions Protocol and Its Logical Verification with Non-Monotomic Dynamic Logic

作　　者：陈庆锋[1] 白硕[1] 王驹[2] 张师超[3] 隋立颖 

机构地区：[1]国家智能计算机研究开发中心,北京100080 [2]中国科学院软件研究所,北京100080 [3]广西师范大学数学与计算机科学系,桂林541004

出　　处：《软件学报》2000年第2期240-250,共11页Journal of Software

基　　金：国家 8 6 3高科技项目基金! (No.86 3- 30 6 - ZD- 10 - 0 2 )资助

摘　　要：该文介绍了 SET(secure electronic transactions)的付费业务流程 ,对 NDL (non- monotomic dynamiclogic)的逻辑框架进行了扩展 ,即针对 SET协议 ,增加了新的公理 ,重新给出积累规则的定义 .在此基础上 ,用对 SET中的几个重要的范例进行的逻辑验证 ,说明了 NDL在验证电子商务协议上的重要性 ,并初步提出了积累规则中需要进一步研究的问题 .This paper introduces the payment process of SET (secure electronic transactions) protocol, and extends the logical framework of NDL to fit the purpose of logical verification of SET. This means to add some new axioms about SET protocols and redefine some given inference rules. Based on these, the logical verification for key fragments of SET protocol is given to show the importance of NDL and its extensions in E commerce. Topics for further research on the “Rule of Accumulation” are also proposed.

关 键 词：信息安全 逻辑验证 电子商务 安全协议 

分 类 号：F716[经济管理—产业经济] TP309[自动化与计算机技术—计算机系统结构]