电子商务安全协议的逻辑验证  

Logical Verification of Secure Electronic Transactions Protocol

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

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

出　　处：《软件学报》2000年第3期346-362,共17页Journal of Software

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

摘　　要：作者在以前所做的工作中 ,已对电子商务安全 (secure electronic transactions,简称 SET)中抽取的片段进行了证明 ,也对 SET中可能存在的问题进行了初步探讨 .该文在此基础上 ,对 SET的整个业务流程进行了严格的逻辑验证 ,通过形式化逻辑方法的验证 ,发现了 SET协议中存在的一些问题 ,并对如何解决这些问题进行了初步的探讨 .In the previous work, some segments of secure electronic transactions (SET) are verified, and some potential problems in SET are also discussed. Based on these, all transactions in SET are strictly logically verified in this paper. Though this formal logic verification, certain problems are found to do exist in SET. Solutions to these problems are also discussed.

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

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