本文關(guān)鍵詞：電子商務(wù)協(xié)議的形式化分析與漏洞檢測

  更多相關(guān)文章： 電子商務(wù) 協(xié)議漏洞 CSP 形式化分析 匿名性

【摘要】：電子商務(wù)安全協(xié)議,為電子商務(wù)活動提供一系列的安全保護(hù)工作,是整個系統(tǒng)安全體系的核心。電子商務(wù)安全協(xié)議除需要提供保密性、認(rèn)證性等一般安全性質(zhì)外,通常還需要滿足原子性、匿名性以及不可否認(rèn)性等多種特性。因此,電子商務(wù)安全協(xié)議的設(shè)計與安全檢測是目前的研究熱點(diǎn)與難點(diǎn)。研究某種方法能準(zhǔn)確高效的發(fā)現(xiàn)協(xié)議中的安全問題,并對檢測出的漏洞進(jìn)行有效的分析和修復(fù),對于電子商務(wù)協(xié)議的安全運(yùn)行至關(guān)重要。本文圍繞電子商務(wù)安全協(xié)議的形式化分析與協(xié)議漏洞檢測開展研究工作,主要工作與創(chuàng)新點(diǎn)為：1.在介紹基于CSP的模型檢測工具FDR以及建模工具Casper的基礎(chǔ)上,對Caper/FDR中攻擊者的能力以及系統(tǒng)中產(chǎn)生的攻擊者模型進(jìn)行了描述和分析；2.將Casper/FDR2模型檢測方法運(yùn)用到電子商務(wù)領(lǐng)域的研究分析中,找到了多個電子商務(wù)協(xié)議的漏洞,并提出了具體的改進(jìn)方案；3.在給出電子商務(wù)協(xié)議原子性的兩個擴(kuò)展特性的基礎(chǔ)上,提出了運(yùn)用CSP建模方式對交易協(xié)議的擴(kuò)展原子性進(jìn)行形式化分析方法,建立了非常規(guī)狀態(tài)的系統(tǒng)模型,并運(yùn)用FDR對建立的CSP模型進(jìn)行檢測,對于實(shí)驗(yàn)中發(fā)現(xiàn)的協(xié)議漏洞,提出了改進(jìn)方案；4.在基于CSP的安全協(xié)議匿名性理論基礎(chǔ)上,提出了一套對于電子商務(wù)協(xié)議匿名性的形式化分析方法,給出了適用于CSP/FDR模型檢測技術(shù)的建模框架,并通過對一個電子商務(wù)協(xié)議進(jìn)行實(shí)驗(yàn)描述了具體的建模分析過程。本文研究成果表明：以CSP理論框架為基礎(chǔ),運(yùn)用相應(yīng)的模型檢測工具Casper和FDR2,通過有限自動機(jī)結(jié)構(gòu)對電子商務(wù)協(xié)議中的所有狀態(tài)集合進(jìn)行檢測,可有效測試與發(fā)現(xiàn)電子商務(wù)協(xié)議中保密性、認(rèn)證性和匿名性等重要特性的滿足情況,對保障電子商務(wù)系統(tǒng)的安全高效運(yùn)行具有重要意義。
【關(guān)鍵詞】：電子商務(wù) 協(xié)議漏洞 CSP 形式化分析 匿名性
【學(xué)位授予單位】：福州大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2013
【分類號】：TP393.08
【目錄】：

• 中文摘要3-4
• Abstract4-8
• 第一章 緒論8-12
• 1.1 研究背景與意義8-10
• 1.1.1 電子商務(wù)發(fā)展現(xiàn)狀8-9
• 1.1.2 對電子商務(wù)協(xié)議分析的意義9-10
• 1.1.3 國內(nèi)外研究現(xiàn)狀10
• 1.2 主要工作10-11
• 1.3 本文章節(jié)安排11
• 1.4 小結(jié)11-12
• 第二章 電子商務(wù)協(xié)議簡介12-20
• 2.1 安全電子商務(wù)協(xié)議概述12-16
• 2.1.1 電子商務(wù)協(xié)議運(yùn)行環(huán)境中的主要角色12-13
• 2.1.2 安全電子商務(wù)協(xié)議的主要特性13-14
• 2.1.3 Digicash電子商務(wù)協(xié)議14-16
• 2.2 安全電子商務(wù)協(xié)議的缺陷16-18
• 2.2.1 常見攻擊手段16-17
• 2.2.2 利用協(xié)議設(shè)計漏洞的攻擊17-18
• 2.3 新的潛在安全威脅18-19
• 2.4 小結(jié)19-20
• 第三章 基于CSP方法的模型檢測技術(shù)20-33
• 3.1 安全協(xié)議的形式化分析基礎(chǔ)20-22
• 3.1.1 模態(tài)邏輯技術(shù)20-21
• 3.1.2 模型檢測技術(shù)21-22
• 3.1.3 定理證明技術(shù)22
• 3.2 CSP簡介22-27
• 3.2.1 CSP中常用操作符23-24
• 3.2.2 進(jìn)程24
• 3.2.3 CSP中的跡模型24-26
• 3.2.4 一個簡單的CSP系統(tǒng)模型26-27
• 3.3 基于CSP的模型檢測工具27-30
• 3.3.1 FDR27-28
• 3.3.2 Casper28-30
• 3.4 Casper/FDR中的攻擊者模型30-32
• 3.4.1 攻擊者能力分析30-31
• 3.4.2 具有攻擊者的系統(tǒng)模型31
• 3.4.3 入侵者建模31-32
• 3.5 小結(jié)32-33
• 第四章 基于CASPER/FDR2的電子商務(wù)協(xié)議形式化分析研究33-44
• 4.1 協(xié)議背景33-34
• 4.2 注冊協(xié)議建模和分析34-41
• 4.2.1 注冊協(xié)議34-36
• 4.2.2 注冊協(xié)議的Casper建模36-38
• 4.2.3 檢測結(jié)果及分析38-41
• 4.3 對注冊協(xié)議的改進(jìn)41-43
• 4.4 小結(jié)43-44
• 第五章 電子商務(wù)協(xié)議擴(kuò)展原子性的分析驗(yàn)證44-61
• 5.1 電子商務(wù)協(xié)議原子性的擴(kuò)展44-46
• 5.1.1 接收驗(yàn)證原子性44-45
• 5.1.2 撤銷交易原子性45-46
• 5.2 建立協(xié)議的CSP模型46-53
• 5.2.1 交易協(xié)議46-47
• 5.2.2 定義協(xié)議的運(yùn)行環(huán)境47-48
• 5.2.3 定義協(xié)議數(shù)據(jù)、通信信道和進(jìn)程48
• 5.2.4 對交易實(shí)體及系統(tǒng)整體進(jìn)行建模48-50
• 5.2.5 建立協(xié)議目標(biāo)聲明50-51
• 5.2.6 協(xié)議的非常規(guī)狀態(tài)模型51-53
• 5.3 FDR模型檢測53-55
• 5.3.1 FDR檢測53-54
• 5.3.2 檢測結(jié)果調(diào)試54-55
• 5.4 協(xié)議原子性目標(biāo)分析55-58
• 5.4.1 接收驗(yàn)證原子性分析55-57
• 5.4.2 撤銷交易原子性分析57-58
• 5.5 協(xié)議改進(jìn)58-60
• 5.6 小結(jié)60-61
• 第六章 電子商務(wù)協(xié)議強(qiáng)匿名性分析驗(yàn)證61-76
• 6.1 基于CSP模型的協(xié)議匿名性分析理論基礎(chǔ)61-63
• 6.1.1 匿名性定義61-62
• 6.1.2 觀察者模型62-63
• 6.2 改進(jìn)的電子商務(wù)協(xié)議匿名性形式化分析框架63-66
• 6.2.1 電子商務(wù)協(xié)議匿名性要求63-64
• 6.2.2 電子商務(wù)協(xié)議匿名性模型框架64-66
• 6.3 電子商務(wù)協(xié)議的匿名性模型建立66-71
• 6.3.1 協(xié)議環(huán)境建模67-68
• 6.3.2 參與實(shí)體建模68-69
• 6.3.3 匿名性目標(biāo)建模69-71
• 6.4 結(jié)果驗(yàn)證和分析71-75
• 6.4.1 協(xié)議觀察者71-72
• 6.4.2 模型檢測結(jié)果和分析72
• 6.4.3 內(nèi)部觀察者模型檢測和分析72-75
• 6.5 小結(jié)75-76
• 第七章 總結(jié)和展望76-78
• 7.1 總結(jié)76
• 7.2 展望76-78
• 參考文獻(xiàn)78-82
• 致謝82-83
• 個人簡歷、在讀期間研究成果以及發(fā)表的學(xué)術(shù)論文83

【相似文獻(xiàn)】

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

1 范紅,馮登國;安全協(xié)議形式化分析方法綜述之二——基于攻擊結(jié)構(gòu)性方法[J];網(wǎng)絡(luò)安全技術(shù)與應(yīng)用;2003年06期

2 郭宇燕;;安全協(xié)議的形式化分析方法初探[J];內(nèi)江科技;2007年11期

3 范紅,馮登國;一種混合的安全協(xié)議形式化分析技術(shù)[J];中國科學(xué)院研究生院學(xué)報;2002年03期

4 范紅,馮登國,鄒良惠;安全協(xié)議形式化分析方法綜述之一:基于推理結(jié)構(gòu)性方法[J];網(wǎng)絡(luò)安全技術(shù)與應(yīng)用;2003年05期

5 常亮;古天龍;;安全協(xié)議及其形式化分析研究[J];桂林電子工業(yè)學(xué)院學(xué)報;2006年04期

6 蔡永泉;朱勇;;一種改進(jìn)的A(0)協(xié)議及其形式化分析[J];計算機(jī)工程與應(yīng)用;2006年34期

7 亓文華;張其善;劉建偉;;關(guān)于安全協(xié)議的形式化分析方法的研究[J];遙測遙控;2007年02期

8 文靜華;張梅;張煥國;;電子支付協(xié)議的博弈邏輯模型與形式化分析[J];微電子學(xué)與計算機(jī);2007年09期

9 陸陽;肖軍模;劉晶;;一種新的安全協(xié)議形式化分析方法——證據(jù)邏輯[J];計算機(jī)工程;2008年02期

10 卜奎昊;;安全協(xié)議形式化分析方法的融合性研究[J];西北師范大學(xué)學(xué)報(自然科學(xué)版);2010年05期

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

1 文靜華;張梅;張煥國;;電子支付協(xié)議的博弈邏輯模型與形式化分析[A];2007年全國開放式分布與并行計算機(jī)學(xué)術(shù)會議論文集(上冊)[C];2007年

2 顧永跟;傅育熙;朱涵;呂銀華;;基于進(jìn)程演算的安全協(xié)議形式化分析[A];2005年全國理論計算機(jī)科學(xué)學(xué)術(shù)年會論文集[C];2005年

3 肖美華;鄧宸芳;馬小薏;薛錦云;江耘;;網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析[A];第二十次全國計算機(jī)安全學(xué)術(shù)交流會論文集[C];2005年

4 崔楠;汪學(xué)明;;基于SVO邏輯的電子商務(wù)協(xié)議非否認(rèn)性形式化分析[A];邏輯學(xué)及其應(yīng)用研究——第四屆全國邏輯系統(tǒng)、智能科學(xué)與信息科學(xué)學(xué)術(shù)會議論文集[C];2008年

5 張梅;文靜華;張煥國;;基于ATL的電子商務(wù)協(xié)議建模與形式化分析[A];2009年全國開放式分布與并行計算機(jī)學(xué)術(shù)會議論文集(上冊)[C];2009年

6 李秋山;胡游君;;低成本RFID系統(tǒng)安全協(xié)議設(shè)計及其形式化分析[A];2006北京地區(qū)高校研究生學(xué)術(shù)交流會——通信與信息技術(shù)會議論文集（上）[C];2006年

7 謝鴻波;周明天;;安全協(xié)議的形式化技術(shù):述評[A];’2004計算機(jī)應(yīng)用技術(shù)交流會議論文集[C];2004年

8 徐銳;;設(shè)計安全協(xié)議[A];第十八次全國計算機(jī)安全學(xué)術(shù)交流會論文集[C];2003年

9 劉忠;王成道;;基于漢語語意形式系統(tǒng)的符號化研究[A];第六屆全國計算機(jī)應(yīng)用聯(lián)合學(xué)術(shù)會議論文集[C];2002年

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

1 范紅;安全協(xié)議形式化分析理論與方法[D];中國人民解放軍信息工程大學(xué);2003年

2 張帆;無線網(wǎng)絡(luò)安全協(xié)議的形式化分析方法[D];西安電子科技大學(xué);2007年

3 陳俊清;可信普適服務(wù)的形式化分析與驗(yàn)證[D];上海交通大學(xué);2012年

4 汪學(xué)明;多方安全協(xié)議的形式化分析方法研究與應(yīng)用[D];貴州大學(xué);2008年

5 楊超;無線網(wǎng)絡(luò)協(xié)議的形式化分析與設(shè)計[D];西安電子科技大學(xué);2008年

6 魯來鳳;安全協(xié)議形式化分析理論與應(yīng)用研究[D];西安電子科技大學(xué);2012年

7 朱薏;數(shù)據(jù)庫管理系統(tǒng)安全性形式化分析研究[D];華中科技大學(xué);2014年

8 趙輝;安全協(xié)議形式化分析技術(shù)的研究[D];大連理工大學(xué);2010年

9 何安平;基于層次模型的混合系統(tǒng)形式化分析與驗(yàn)證[D];蘭州大學(xué);2011年

10 李云峰;電子商務(wù)協(xié)議安全性的形式化分析方法研究[D];西南交通大學(xué);2009年

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

1 張玲玲;物聯(lián)網(wǎng)安全協(xié)議形式化分析與驗(yàn)證[D];聊城大學(xué);2015年

2 王煥孝;基于SAT的安全協(xié)議形式化分析方法研究與應(yīng)用[D];解放軍信息工程大學(xué);2014年

3 常寅龍;電子商務(wù)協(xié)議的形式化分析與漏洞檢測[D];福州大學(xué);2013年

4 王潔;公平不可否認(rèn)協(xié)議設(shè)計及其形式化分析[D];重慶大學(xué);2008年

5 成敏盈;電力系統(tǒng)安全協(xié)議形式化分析技術(shù)研究[D];廣東工業(yè)大學(xué);2008年

6 李軼，

本文編號：813117