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

摘要

与证伪法（如模型检测）相比，采用证真法（如定理证明和逻辑推理）能验证协议在任意会话中的正确性，但分析难度较高，验证过程较为复杂。使用SVO逻辑方法，以Netbill微支付协议为例，对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集；在不影响Netbill协议安全性的前提下，为其建立了简化模型；针对协议特点，修正和补充了其验证目标；给出了比之前更合理的协议假设，展示了具体的推理过程，分析了验证结果。结果表明，Netbill协议基本满足认证性。最后对相关研究工作进行了比较。%Compared with the falsification-oriented approaches(such as model checking), the justification-oriented approaches (such as theorem proof and logic reasoning)can verify the correctness of protocols in unbounded number of sessions. However, those approaches are difficult and the verification process is complicated. Based on the SVO logic, this paper chooses the Netbill micropayment protocol to formally analyze the authentication properties of E-commerce payment pro-tocol. First, the axiom set of SVO is extended. Then, a simplified model of Netbill protocol is proposed without affecting the original security properties. According to the protocol’s characteristic, the verifying goals are improved. Moreover, the more reasonable protocol assumptions than before are given, the detailed reasoning process is showed, and the result is analyzed. The result shows that Netbill protocol satisfies the authentication properties. In the end, a comparison with other related research works is showed.