-
题名电子商务支付协议认证性的SVO逻辑验证
被引量：7
- 1
-
-
作者
肖茵茵
苏开乐
-
机构
广东技术师范学院计算机学院
中山大学信息科学与技术学院广东省信息安全重点实验室
北京大学信息科学技术学院教育部高可信软件技术重点实验室
-
出处
《计算机工程与应用》
CSCD
2014年第8期6-10,共5页
-
基金
国家自然科学基金(No.60903054)
国家重点基础研究发展规划(973)(No.2010CB328103)
+1 种基金
广东高校优秀青年创新人才培育项目(No.LYM11085
No.LYM11084)
-
文摘
与证伪法(如模型检测)相比,采用证真法(如定理证明和逻辑推理)能验证协议在任意会话中的正确性,但分析难度较高,验证过程较为复杂。使用SVO逻辑方法,以Netbill微支付协议为例,对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集;在不影响Netbill协议安全性的前提下,为其建立了简化模型;针对协议特点,修正和补充了其验证目标;给出了比之前更合理的协议假设,展示了具体的推理过程,分析了验证结果。结果表明,Netbill协议基本满足认证性。最后对相关研究工作进行了比较。
-
关键词
SVO逻辑
电子商务支付
Netbill协议
认证性
-
Keywords
SVO logic
e-commerce payment
Netbill protocol
authentication properties
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
-
题名SET证书申请协议在SPV下的自动化验证及改进
被引量：3
- 2
-
-
作者
肖茵茵
苏开乐
岳伟亚
陈清亮
吕关锋
杨晋吉
-
机构
中山大学信息科学与技术学院广东省信息安全重点实验室
暨南大学计算机科学系
北京工业大学计算机学院
-
出处
《计算机学报》
EI
CSCD
北大核心
2008年第6期1035-1045,共11页
-
基金
国家“九七三”重点基础研究发展规划项目基金(2005CB321902)
国家自然科学基金(60496327,10410638,60473004)
+1 种基金
广东省自然科学基金(06023195)
广东省自然科学基金团队项目(04205407)资助~~
-
文摘
基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.
-
关键词
SET证书申请协议
自动化验证
SPV
认证性
秘密性
-
Keywords
SET certificate registration protocols
automatic verification
SPV
authentication
secrecy
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
-
题名协议组合逻辑在实例化空间模型中的语义解释
- 3
-
-
作者
肖茵茵
苏开乐
-
机构
广东技术师范学院计算机学院
中山大学信息科学与技术学院广东省信息安全重点实验室
浙江师范大学数理与信息工程学院
-
出处
《广东技术师范学院学报》
2016年第2期8-19,共12页
-
基金
国家自然科学基金(60903054
61379019)
+3 种基金
国家"973"重点基础研究发展计划资助项目(2010CB328103)
中国博士后科学基金面上项目(2013M540704)
广东高校优秀青年创新人才培育项目(LYM11085
LYM11084)资助
-
文摘
安全协议的验证是个不可判问题.为了对实例化空间逻辑ISL的语义表达能力给出理论上的衡量与评价,选择另一种实用的协议组合逻辑PCL,分析了ISL和PCL之间的关系.在此基础上,将PCL的索状空间语义模型转换为ISL的实例化空间语义模型,在实例化空间下对PCL的主要公式、定理、推导规则做了语义解释.研究表明,实例化空间能够完全表示PCL的语义,且ISL的语义表达能力强于PCL.新的模型解释使PCL更易于扩展,且使得用PCL理论验证的协议能够利用ISL的自动化验证工具SPV进行分析.
-
关键词
安全协议验证
实例化空间
协议组合逻辑
索状空间
语义解释
-
Keywords
Security protocols analyzing
Instantiation space
Protocol compositional logic
Cord space
Semantic interpretation
-
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
-
