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

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

【參考文獻(xiàn)】

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

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

，

本文編號(hào)：1949689