本文關(guān)鍵詞：基于模型檢測的電子商務(wù)交易協(xié)議形式化分析與驗(yàn)證

  更多相關(guān)文章： 形式化方法 Spin 模型檢測 電子商務(wù)交易協(xié)議 Promela

【摘要】：根據(jù)CNNIC(China Internet Network Information Center,中國互聯(lián)網(wǎng)絡(luò)信息中心)發(fā)布的“第37次中國互聯(lián)網(wǎng)絡(luò)發(fā)展?fàn)顩r統(tǒng)計(jì)報(bào)告”,2015年,42.7%的網(wǎng)民遭遇過網(wǎng)絡(luò)安全問題。隨著網(wǎng)絡(luò)購物群體的不斷增大,電子商務(wù)安全問題引起了消費(fèi)者的廣泛關(guān)注。2015年,我國網(wǎng)絡(luò)購物用戶規(guī)模達(dá)到4.13億,同時(shí),16.4%的消費(fèi)者在網(wǎng)購過程中遭遇到過網(wǎng)絡(luò)消費(fèi)欺詐。由此可見,網(wǎng)絡(luò)安全問題和交易安全問題是保證電子商務(wù)進(jìn)一步發(fā)展的關(guān)鍵之所在。交易協(xié)議是交易安全問題的核心。本文從網(wǎng)絡(luò)交易安全問題出發(fā),選取主流電子商務(wù)B2C模式作為研究對象,通過模型檢測方法對基于第三方支付平臺(tái)的交易協(xié)議進(jìn)行了形式化建模、分析和驗(yàn)證,以保證買家和商戶之間完成安全、可靠的交易活動(dòng)。其主要內(nèi)容如下：1.介紹了課題背景、相關(guān)理論基礎(chǔ)和采用形式化方法分析安全協(xié)議的發(fā)展過程以及研究現(xiàn)狀。2.對B2C模式涉及到的電子商務(wù)交易協(xié)議進(jìn)行了簡要的分析,使用Promela語言形式化地描述了電子商務(wù)交易協(xié)議中涉及到的四個(gè)實(shí)體：買家、商戶網(wǎng)站、第三方支付平臺(tái)和銀行。3.使用模型檢測方法對B2C模式交易協(xié)議進(jìn)行形式化驗(yàn)證,對交易協(xié)議進(jìn)行抽象化建模,描述了電子商務(wù)交易協(xié)議的LTL性質(zhì),使用Spin的圖形界面工具XSpin得到交易協(xié)議的運(yùn)行軌跡,在此基礎(chǔ)上分析目前B2C模式交易協(xié)議存在的潛在安全隱患。4.針對分析結(jié)果,提出了一種基于B2C模式的改進(jìn)模型,增加了物流方和第三方隱私服務(wù)器兩個(gè)實(shí)體,用于規(guī)范交易流程和保護(hù)買家隱私。
【學(xué)位授予單位】：寧夏大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號(hào)】：F724.6;TP393.08

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

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

2 肖健宇;張德運(yùn);鄭衛(wèi)斌;;過程提取用于改善程序模型檢測的可伸縮性[J];西安交通大學(xué)學(xué)報(bào);2006年06期

3 袁志斌;徐正權(quán);王能超;;軟件模型檢測中的抽象[J];計(jì)算機(jī)科學(xué);2006年07期

4 劉吉鋒;孫吉貴;;基于抽象-驗(yàn)證-細(xì)化范例的軟件模型檢測[J];計(jì)算機(jī)科學(xué);2006年12期

5 化志章;吳傳孫;揭安全;薛錦云;;軟件模型檢測新技術(shù)研究[J];微計(jì)算機(jī)信息;2007年36期

6 王飛明;胡元闖;董榮勝;;模型檢測研究進(jìn)展[J];廣西科學(xué)院學(xué)報(bào);2008年04期

7 鄺宏斌;羅貴明;;并行軟件模型檢測[J];計(jì)算機(jī)工程;2008年19期

8 何愷鐸;顧明;宋曉宇;李力;李江;;面向源代碼的軟件模型檢測及其實(shí)現(xiàn)[J];計(jì)算機(jī)科學(xué);2009年01期

9 林璇;;模型檢測方法在入侵檢測中的應(yīng)用研究[J];現(xiàn)代計(jì)算機(jī)(專業(yè)版);2009年02期

10 顧濱兵;;一種軟件模型檢測方法及其原型系統(tǒng)[J];微計(jì)算機(jī)應(yīng)用;2010年11期

中國重要會(huì)議論文全文數(shù)據(jù)庫 前5條

1 高靜;曹子寧;;基于空間邏輯和計(jì)算樹邏輯的模型檢測[A];2009年中國高校通信類院系學(xué)術(shù)研討會(huì)論文集[C];2009年

2 許梅;曹子寧;;基于謂詞μ演算和空間邏輯的模型檢測算法研究[A];2009年中國高校通信類院系學(xué)術(shù)研討會(huì)論文集[C];2009年

3 何青;駱翔宇;蘇開樂;;對弈必勝策略的符號(hào)化模型檢測[A];2006年全國理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2006年

4 王飛明;胡元闖;董榮勝;;模型檢測中狀態(tài)爆炸及其優(yōu)化策略研究[A];廣西計(jì)算機(jī)學(xué)會(huì)2008年年會(huì)論文集[C];2008年

5 陳道喜;張廣泉;陳冬火;;NSPK協(xié)議的Spin模型檢測[A];2008年全國開放式分布與并行計(jì)算機(jī)學(xué)術(shù)會(huì)議論文集(下冊)[C];2008年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 奚琪;基于模型檢測的二進(jìn)制代碼惡意行為識(shí)別技術(shù)研究[D];解放軍信息工程大學(xué);2014年

2 黃鎮(zhèn)謹(jǐn);基于模型檢測的時(shí)空性能分析若干問題研究[D];合肥工業(yè)大學(xué);2016年

3 江華;界程演算模型檢測[D];貴州大學(xué);2008年

4 林榮德;移動(dòng)界程演算及模型檢測應(yīng)用的關(guān)鍵問題研究[D];華南理工大學(xué);2010年

5 劉劍;傳值進(jìn)程與移動(dòng)進(jìn)程的模型檢測方法[D];中國科學(xué)院研究生院（軟件研究所）;2005年

6 劉志鋒;模型檢測中關(guān)鍵技術(shù)的研究及其應(yīng)用[D];南京大學(xué);2011年

7 朱維軍;時(shí)間區(qū)間時(shí)序邏輯模型檢測：理論、算法及應(yīng)用[D];西安電子科技大學(xué);2011年

8 尹良澤;基于SAT的組合遷移系統(tǒng)模型檢測技術(shù)研究[D];清華大學(xué);2014年

9 陳冬火;超協(xié)調(diào)時(shí)序邏輯及其模型檢測方法[D];中國科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2006年

10 田聰;命題投影時(shí)序邏輯的判定性、復(fù)雜性、表達(dá)性及模型檢測[D];西安電子科技大學(xué);2010年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 黃延凱;基于圖轉(zhuǎn)換的關(guān)聯(lián)屬性規(guī)約模型檢測及其支撐平臺(tái)研究[D];南京航空航天大學(xué);2015年

2 余鵬;基于模型檢測的網(wǎng)絡(luò)傳播干預(yù)策略問題研究[D];南京航空航天大學(xué);2015年

3 程貝;基于抽象和學(xué)習(xí)的統(tǒng)計(jì)模型檢測研究[D];華東師范大學(xué);2016年

4 何佳;面向復(fù)雜隨機(jī)系統(tǒng)的貝葉斯統(tǒng)計(jì)模型檢測方法[D];華東師范大學(xué);2016年

5 王云云;基于分組壓縮算法的并行程序模型檢測[D];中國科學(xué)技術(shù)大學(xué);2016年

6 段廷銀;基于云計(jì)算平臺(tái)的時(shí)態(tài)邏輯模型檢測算法研究與實(shí)現(xiàn)[D];鄭州大學(xué);2016年

7 許鵬濤;基于模型檢測的入侵檢測基準(zhǔn)測試平臺(tái)研究[D];鄭州大學(xué);2016年

8 李婉璐;基于模型檢測的電子商務(wù)交易協(xié)議形式化分析與驗(yàn)證[D];寧夏大學(xué);2016年

9 張衍志;符號(hào)化模型檢測算法的研究[D];吉林大學(xué);2009年

10 黎吾平;模型檢測在軟件方面的應(yīng)用[D];吉林大學(xué);2008年

，

本文編號(hào)：1204789