本文選題：安全交換協(xié)議 + 公平性�。� 參考：《天津大學(xué)》2014年碩士論文

【摘要】：隨著計算機網(wǎng)絡(luò)技術(shù)的發(fā)展和電子商務(wù)的普及,電子數(shù)據(jù)交換變得越來越重要,但是,伴隨而來的安全性、公平性及不可否認性等問題也困擾著電子商務(wù)的供應(yīng)商及消費者。作為電子商務(wù)的基石,安全交換協(xié)議為數(shù)據(jù)交換問題提供了一種有效的解決方案。由于安全交換協(xié)議地位的重要性,結(jié)構(gòu)的不對稱性及復(fù)雜性,對其安全分析是近幾年來信息安全領(lǐng)域的一個研究熱點與難點。目前,國內(nèi)外已有一些安全交換協(xié)議分析方法,包括Paulson歸納法,CSP形式化建模法,及串空間模型法等,但是這些方法往往具有無法對密碼原語建模,無法自動生成攻擊者模型,無法形式化描述協(xié)議性質(zhì)等缺點。本文對安全交換協(xié)議及其形式化分析方法進行了研究,基于可對密碼原語建模的應(yīng)用Pi演算以及線性時序邏輯提出了一種新的安全交換協(xié)議的分析方法,并利用Antlr和C#語言實現(xiàn)了安全交換協(xié)議模型檢測平臺。主要研究包括如下幾個方面:首先以Proverif建模語言Pi演算為基礎(chǔ),擴展選擇算子,用于安全協(xié)議交換協(xié)議的形式化描述;然后給出公平性及不可否認性定義,使用線性時序邏輯語言(Linear Temporal Logic,LTL)形式化描述公式,并將LTL描述的性質(zhì)轉(zhuǎn)化為Bu?chi自動機;接著基于彈性信道理論,改進Dolve-Yao攻擊者模型庫,使其更符合安全交換協(xié)議攻擊者行為,實現(xiàn)根據(jù)協(xié)議自動生成攻擊者,然后將添加了攻擊者的協(xié)議Pi演算模型轉(zhuǎn)換為標號轉(zhuǎn)移系統(tǒng)(Labelled Transition System,LTS);最后,利用Tarjan算法,結(jié)合MoveOneStep方法,實現(xiàn)On-The-Fly思想,尋找協(xié)議安全性與不可否認性攻擊路徑。本文結(jié)合若干個安全交換協(xié)議對提出的分析方法及檢測平臺做了詳細的說明,實驗結(jié)果顯示該平臺能夠有效檢測協(xié)議潛在的攻擊路徑,對提高電子商務(wù)安全性、公平性及不可否認性的有一定的理論和實用意義。
[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.
【學(xué)位授予單位】：天津大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2014
【分類號】：TP393.04;TP311.52

【參考文獻】

相關(guān)期刊論文 前1條

1 高悅翔;彭代淵;閆麗麗;;認證郵件協(xié)議的安全性分析與改進[J];電子科技大學(xué)學(xué)報;2013年02期

，

本文編號：1949689