安全交换协议模型检测平台的设计与实现

发布时间：2018-05-29 05:33

本文选题：安全交换协议 + 公平性　；参考：《天津大学》2014年硕士论文

【摘要】：随着计算机网络技术的发展和电子商务的普及,电子数据交换变得越来越重要,但是,伴随而来的安全性、公平性及不可否认性等问题也困扰着电子商务的供应商及消费者。作为电子商务的基石,安全交换协议为数据交换问题提供了一种有效的解决方案。由于安全交换协议地位的重要性,结构的不对称性及复杂性,对其安全分析是近几年来信息安全领域的一个研究热点与难点。目前,国内外已有一些安全交换协议分析方法,包括Paulson归纳法,CSP形式化建模法,及串空间模型法等,但是这些方法往往具有无法对密码原语建模,无法自动生成攻击者模型,无法形式化描述协议性质等缺点。本文对安全交换协议及其形式化分析方法进行了研究,基于可对密码原语建模的应用Pi演算以及线性时序逻辑提出了一种新的安全交换协议的分析方法,并利用Antlr和C#语言实现了安全交换协议模型检测平台。主要研究包括如下几个方面:首先以Proverif建模语言Pi演算为基础,扩展选择算子,用于安全协议交换协议的形式化描述;然后给出公平性及不可否认性定义,使用线性时序逻辑语言(Linear Temporal Logic,LTL)形式化描述公式,并将LTL描述的性质转化为Bu?chi自动机;接着基于弹性信道理论,改进Dolve-Yao攻击者模型库,使其更符合安全交换协议攻击者行为,实现根据协议自动生成攻击者,然后将添加了攻击者的协议Pi演算模型转换为标号转移系统(Labelled Transition System,LTS);最后,利用Tarjan算法,结合MoveOneStep方法,实现On-The-Fly思想,寻找协议安全性与不可否认性攻击路径。本文结合若干个安全交换协议对提出的分析方法及检测平台做了详细的说明,实验结果显示该平台能够有效检测协议潜在的攻击路径,对提高电子商务安全性、公平性及不可否认性的有一定的理论和实用意义。
[Abstract]:With the development of computer network technology and the popularization of electronic commerce, electronic data exchange (EDI) becomes more and more important. However, the problems of security, fairness and non-repudiation are also puzzling the suppliers and consumers of E-commerce. As the cornerstone of e-commerce, security exchange protocol provides an effective solution for data exchange. Because of the importance of the security exchange protocol, the asymmetry and complexity of the structure, the security analysis of the security protocol is a hot and difficult point in the field of information security in recent years. At present, there are some security exchange protocol analysis methods at home and abroad, including Paulson induction method and string space model method, etc. However, these methods are often unable to model cryptographic primitives and can not automatically generate the attacker model. It is impossible to formalize the nature of the protocol. In this paper, the security switching protocol and its formal analysis method are studied. A new security switching protocol analysis method is proposed based on Pi calculus and linear temporal logic, which can be used to model cryptographic primitives. The security exchange protocol model checking platform is implemented by using Antlr and C # language. The main research includes the following aspects: firstly, based on the Proverif modeling language Pi calculus, the selection operator is extended to describe the security protocol exchange protocol, and then the definition of fairness and non-repudiation is given. In this paper, linear Temporal logic language (LTL) is used to formalize the description formula, and the nature of LTL description is transformed into Bu?chi automata, and then, based on the elastic channel theory, the Dolve-Yao attacker model base is improved to make it more consistent with the behavior of secure exchange protocol attacker. The protocol Pi calculus model added by the attacker is transformed into label transfer system (Labelled Transition system). Finally, the idea of On-The-Fly is realized by using Tarjan algorithm and MoveOneStep method. Search for protocol security and non-repudiation attack path. This paper gives a detailed description of the analysis method and detection platform combined with several security exchange protocols. The experimental results show that the platform can effectively detect the potential attack path of the protocol and improve the security of electronic commerce. Fairness and non-repudiation have certain theoretical and practical significance.
【学位授予单位】：天津大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP393.04;TP311.52

【参考文献】