基于模型检测的SET协议形式化验证与改进

发布时间：2018-03-13 17:08

本文选题：SET协议　切入点：模型检测　出处：《南昌大学》2014年硕士论文　论文类型：学位论文

【摘要】：随着电子商务的不断发展，，电子商务的安全一直备受人们关注。SET协议作为电子商务中的关键协议，其安全性的重要性不言而喻。形式化方法作为重要的协议安全性分析方法，以其严密性和准确性的特点已成为检验网络安全协议安全性的重要途径。模型检测是形式化方法中非常重要的一种方法，已成功地运用于网络协议的安全性验证。由于协议的安全性问题十分微妙，有些本身并不复杂的协议的安全漏洞在协议使用很长时间后才被发现。进而，分析和研究SET协议的安全性，找出其存在的安全漏洞或者证明其为安全的，对协议的进一步发展及应用有着非常重要的意义。本文主要运用模型检测方法对SET协议进行形式化分析与验证。首先对协议的形式化分析方法、模型检测技术、SPIN验证工具、Promela语言、线性时态逻辑LTL等相关理论进行了介绍；其次对SET协议的工作原理及其支付过程的各个阶段进行了形式化描述和分析，针对该协议的支付过程采用了基于LuSmolka的SET协议简化模型，并运用Promela语言对该协议进行形式化建模，在网络环境被入侵者控制的假设下，运用SPIN发现了攻击；采用atomic、d_step、偏序规约及Bit-state hashing等优化技术来缓解状态空间爆炸、减少存储空间，从而提高验证效率；最后针对协议存在的漏洞对协议进行改进，并再次使用模型检测工具SPIN验证了改进后的SET协议的正确性。
[Abstract]:With the continuous development of electronic commerce, the security of electronic commerce has been concerned by people, as the key protocol in electronic commerce, the importance of security is self-evident. Because of its strictness and accuracy, model checking has become an important way to verify the security of network security protocols, and model checking is a very important method in formal methods, which has been successfully applied to the security verification of network protocols. Because the security problem of the protocol is very delicate, the security vulnerabilities of some protocols which are not complicated by themselves are discovered only after the protocol has been used for a long time. Furthermore, the security of the SET protocol is analyzed and studied. It is of great significance for the further development and application of the protocol to find out the existing security holes or prove them to be secure. In this paper, the formal analysis and verification of SET protocol are mainly carried out by using model checking method. Firstly, the formal analysis method of the protocol, the model checking technology, the promela language, the linear temporal logic LTL and so on, are introduced. Secondly, the working principle of the SET protocol and the various stages of the payment process are described and analyzed. The simplified model of the SET protocol based on LuSmolka is adopted for the payment process of the protocol, and the formal modeling of the protocol is carried out by using the Promela language. Under the assumption that the network environment is controlled by intruders, the attack is discovered by using SPIN, the optimization techniques such as atomic step, partial sequence protocol and Bit-state hashing are used to alleviate the explosion of state space, reduce storage space, and improve the efficiency of verification. Finally, the protocol is improved in view of the flaws in the protocol, and the correctness of the improved SET protocol is verified by using the model checking tool SPIN again.
【学位授予单位】：南昌大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP393.04

【参考文献】