电子商务支付协议认证性的SVO逻辑验证

摘要：

与证伪法（如模型检测）相比，采用证真法（如定理证明和逻辑推理）能验证协议在任意会话中的正确性，但分析难度较高，验证过程较为复杂。使用SVO逻辑方法，以Netbill微支付协议为例，对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集；在不影响Netbill协议安全性的前提下，为其建立了简化模型；针对协议特点，修正和补充了其验证目标；给出了比之前更合理的协议假设，展示了具体的推理过程，分析了验证结果。结果表明，Netbill协议基本满足认证性。最后对相关研究工作进行了比较。

关键词：SVO逻辑、电子商务支付、Netbill协议、认证性

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

资助基金：国家自然科学基金No.60903054；国家重点基础研究发展规划973No.2010CB328103；广东高校优秀青年创新人才培育项目No.LYM11085，No.LYM11084。

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

页数：共5页

页码：6-10