本文選題：SET協(xié)議　切入點(diǎn)：模型檢測　出處：《南昌大學(xué)》2014年碩士論文　論文類型：學(xué)位論文

【摘要】：隨著電子商務(wù)的不斷發(fā)展，，電子商務(wù)的安全一直備受人們關(guān)注。SET協(xié)議作為電子商務(wù)中的關(guān)鍵協(xié)議，其安全性的重要性不言而喻。形式化方法作為重要的協(xié)議安全性分析方法，以其嚴(yán)密性和準(zhǔn)確性的特點(diǎn)已成為檢驗(yàn)網(wǎng)絡(luò)安全協(xié)議安全性的重要途徑。模型檢測是形式化方法中非常重要的一種方法，已成功地運(yùn)用于網(wǎng)絡(luò)協(xié)議的安全性驗(yàn)證。 由于協(xié)議的安全性問題十分微妙，有些本身并不復(fù)雜的協(xié)議的安全漏洞在協(xié)議使用很長時(shí)間后才被發(fā)現(xiàn)。進(jìn)而，分析和研究SET協(xié)議的安全性，找出其存在的安全漏洞或者證明其為安全的，對協(xié)議的進(jìn)一步發(fā)展及應(yīng)用有著非常重要的意義。 本文主要運(yùn)用模型檢測方法對SET協(xié)議進(jìn)行形式化分析與驗(yàn)證。首先對協(xié)議的形式化分析方法、模型檢測技術(shù)、SPIN驗(yàn)證工具、Promela語言、線性時(shí)態(tài)邏輯LTL等相關(guān)理論進(jìn)行了介紹；其次對SET協(xié)議的工作原理及其支付過程的各個(gè)階段進(jìn)行了形式化描述和分析，針對該協(xié)議的支付過程采用了基于LuSmolka的SET協(xié)議簡化模型，并運(yùn)用Promela語言對該協(xié)議進(jìn)行形式化建模，在網(wǎng)絡(luò)環(huán)境被入侵者控制的假設(shè)下，運(yùn)用SPIN發(fā)現(xiàn)了攻擊；采用atomic、d_step、偏序規(guī)約及Bit-state hashing等優(yōu)化技術(shù)來緩解狀態(tài)空間爆炸、減少存儲空間，從而提高驗(yàn)證效率；最后針對協(xié)議存在的漏洞對協(xié)議進(jìn)行改進(jìn)，并再次使用模型檢測工具SPIN驗(yàn)證了改進(jìn)后的SET協(xié)議的正確性。
[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.
【學(xué)位授予單位】：南昌大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2014
【分類號】：TP393.04

【參考文獻(xiàn)】

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

1 林惠民,張文輝;模型檢測:理論、方法與應(yīng)用[J];電子學(xué)報(bào);2002年S1期

2 屈喜龍;;基于數(shù)字證書的數(shù)字簽名系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[J];計(jì)算機(jī)工程與應(yīng)用;2006年15期

3 戎玫;張廣泉;;模型檢測新技術(shù)研究[J];計(jì)算機(jī)科學(xué);2003年05期

4 肖美華;薛錦云;;基于SPIN/Promela的并發(fā)系統(tǒng)驗(yàn)證[J];計(jì)算機(jī)科學(xué);2004年08期

5 郭建;邊明明;韓俊崗;;LTL公式到自動(dòng)機(jī)的轉(zhuǎn)換[J];計(jì)算機(jī)科學(xué);2008年07期

6 張頻;羅貴明;;UML模型檢測方法的研究[J];計(jì)算機(jī)應(yīng)用;2007年10期

7 程瑩;康汶;;基于SPIN的SSL3.0握手協(xié)議模型檢測[J];計(jì)算機(jī)與數(shù)字工程;2010年08期

8 陳春玲;田國良;;安全協(xié)議的SPIN建模與分析[J];南京航空航天大學(xué)學(xué)報(bào);2009年05期

9 王雪莉;高玉良;;RSA公鑰密碼體制及其在SET協(xié)議中的應(yīng)用[J];信息安全與通信保密;2007年08期

10 林松;李舟軍;;基于Petri網(wǎng)的雙重?cái)?shù)字簽名的描述與驗(yàn)證[J];系統(tǒng)仿真學(xué)報(bào);2008年09期

本文編號：1607322