实例化空间逻辑下的SET支付协议验证及改进  

Verification and improvement of SET payment protocols under instantiation space logic

作　　者：肖茵茵[1,2] 苏开乐[2] 马震远[1] 胡若[1] 

机构地区：[1]广东技术师范学院计算机科学学院,广东广州510665 [2]中山大学信息科学与技术学院,广东广州510275

出　　处：《华中科技大学学报（自然科学版）》2013年第7期97-102,共6页Journal of Huazhong University of Science and Technology(Natural Science Edition)

基　　金：国家杰出青年科学基金资助项目(60725207);国家重点基础研究发展计划资助项目(2010CB328103);国家自然科学基金资助项目(60903054);广东省高校优秀青年创新人才培育项目(LYM11085;LYM11084)

摘　　要：使用基于知识推理的实例化空间逻辑及其自动化验证工具SPV对SET支付协议的重要安全性质进行验证,并对协议进行改进.与模型检测法相比,可以验证协议在任意会话中的正确性;与定理证明等方法相比,验证过程是完全自动化的.在不影响原SET支付协议安全性的前提下,使用实例化空间逻辑简化协议的复杂消息,并合理选择协议分支,建立比以往研究更贴近原协议的模型.给出了该模型及其秘密性、认证性在SPV下的形式化描述,并展示验证结果,分析验证效率.针对验证结果中不被满足的认知规范,给出协议的改进方案,解决了持卡人和支付网关之间的认证问题.The important properties of SET（secure electronic transaction）payment protocols were verified and improved by a knowledge reasoning method ISL（instantiation space logic）and its tool SPV（security protocol verifier）.The method could verify the correctness of protocols in unbounded number of sessions compared with model checking method.By comparison with theorems or proved methods,the method was testified fully automatically.A model more closed to the original protocols was proposed by simplifying complex messages of protocols under the ISL and choosing the protocol steps rationally,without affecting the important security properties.The SPV formal description of the model and its properties（secrecy and authentication） was given,and the verification results and effectiveness were showed.The protocols were improved according to the unsatisfied epistemic specifications,and the improvement resolved the authentication problem between the cardholder and pay-gate in the protocols.

关 键 词：知识推理 安全电子交易支付协议 形式化方法 实例化空间逻辑 自动化验证 

分 类 号：TN918[电子电信—通信与信息系统]