本文關鍵詞：顏色Petri網(wǎng)的電子商務協(xié)議形式化分析方法研究，由筆耕文化傳播整理發(fā)布。

【摘要】：隨著Internet的迅猛發(fā)展，電子商務已經(jīng)深入到了社會的各個角落。如何確定電子商務交易的安全可靠，成為了一門重要的研究課題。電子商務協(xié)議是一種保證電子商務交易正常展開的協(xié)議，在滿足安全協(xié)議的性質(zhì)的同時，還要保證滿足可追究性、公平性和時限性等特殊性質(zhì)。對電子商務協(xié)議的形式化分析，是發(fā)現(xiàn)電子商務協(xié)議缺陷的有效工具。本文使用顏色Petri網(wǎng)形式化分析工具，提出了可追究性、公平性和時限性三者兼顧的形式化建模方法，并對電子商務協(xié)議中存在的攻擊進行了建模分析。 首先，在高級網(wǎng)顏色Petri網(wǎng)的基礎上，提出一種對電子商務協(xié)議的可追究性、公平性和時限性建模的顏色Petri網(wǎng)方法。在協(xié)議的可追究性和公平性Petri網(wǎng)模型基礎上，加入了復雜多變的時限性因素，形成了三者兼顧的模型。利用Petri網(wǎng)中逆向狀態(tài)分析方法對該模型進行分析，驗證協(xié)議是否滿足三個性質(zhì)。以改進的ZG協(xié)議KZG協(xié)議為例，，用所提建模方法建立了KZG協(xié)議的顏色Petri網(wǎng)模型，經(jīng)過逆向狀態(tài)分析，驗證了該協(xié)議滿足可追究性、公平性和時限性。 其次，研究了電子商務協(xié)議中存在的不安全狀態(tài)。提出從電子商務協(xié)議的發(fā)送方非否認證據(jù)EOO(Evidence Of Origin)和接收方非否認證據(jù)EOR(Evidence Of Recipt)中提取不安全狀態(tài)并定義不安全狀態(tài)的方法，解決了不同電子商務協(xié)議不安全狀態(tài)難以確定的難題。提出了建立帶攻擊者的顏色Petri網(wǎng)建模方法并利用逆向分析方法分析不安全狀態(tài)是否可達。以CMP1為例，建立了帶攻擊者的CMP1顏色Petri網(wǎng)模型，進過分析發(fā)現(xiàn)該協(xié)議存在的不安全狀態(tài)可達，該協(xié)議存在漏洞。 最后，利用顏色Petri網(wǎng)的仿真工具CPN Tools對所建立的KZG協(xié)議以及CMP1協(xié)議的顏色Petri網(wǎng)模型進行了仿真實驗。運行狀態(tài)空間分析工具，建立ML查詢函數(shù)，查詢協(xié)議的相關性質(zhì)是否滿足，進一步驗證所提方法的正確有效。
【關鍵詞】：電子商務協(xié)議 形式化分析 顏色Petri網(wǎng) CPN Tools KZG CMP1
【學位授予單位】：燕山大學
【學位級別】：碩士
【學位授予年份】：2012
【分類號】：TP301.1;TP393.04
【目錄】：

• 摘要5-6
• Abstract6-9
• 第1章 緒論9-15
• 1.1 研究背景和意義9-10
• 1.2 國內(nèi)外研究現(xiàn)狀10-12
• 1.2.1 Petri 網(wǎng)的研究現(xiàn)狀及分析10-11
• 1.2.2 高級網(wǎng)顏色 Petri 網(wǎng)的研究現(xiàn)狀及分析11-12
• 1.2.3 國內(nèi)外研究現(xiàn)狀的總結(jié)12
• 1.3 本文主要內(nèi)容12-13
• 1.4 本文組織結(jié)構(gòu)13-15
• 第2章 電子商務協(xié)議及顏色 Petri 網(wǎng)分析方法15-23
• 2.1 電子商務協(xié)議的相關概念15-17
• 2.1.1 電子商務協(xié)議的語義15-16
• 2.1.2 電子商務協(xié)議的安全性質(zhì)16-17
• 2.2 顏色 Petri 網(wǎng)的相關知識17-20
• 2.2.1 顏色 Petri 網(wǎng)的基本定義18
• 2.2.2 顏色 Petri 網(wǎng)的特征及引發(fā)規(guī)則18-19
• 2.2.3 顏色 Petri 網(wǎng)的性質(zhì)19-20
• 2.3 顏色 Petri 網(wǎng)的主要分析方法和工具20-22
• 2.4 顏色 Petri 網(wǎng)的方法的總結(jié)22
• 2.5 本章小結(jié)22-23
• 第3章 一種顏色 Petri 網(wǎng)的電子商務協(xié)議建模方法23-35
• 3.1 引言23
• 3.2 一種顏色 Petri 網(wǎng)的電子商務協(xié)議建模方法23-27
• 3.2.1 電子商務協(xié)議消息的抽象24
• 3.2.2 具體建模步驟24-26
• 3.2.3 協(xié)議的分析26-27
• 3.3 實例分析27-34
• 3.3.1 協(xié)議的描述28
• 3.3.2 協(xié)議的建模28-31
• 3.3.3 協(xié)議的分析31-33
• 3.3.4 本文方法與相關方法的比較33-34
• 3.4 本章小結(jié)34-35
• 第4章 一種顏色 Petri 網(wǎng)的電子商務協(xié)議攻擊建模方法35-47
• 4.1 引言35-36
• 4.2 攻擊者模型及攻擊目標和手段36-37
• 4.2.1 Dolev-Yao 模型36
• 4.2.2 安全協(xié)議中的攻擊目標和手段36-37
• 4.3 一種顏色 Petri 網(wǎng)的電子商務協(xié)議攻擊建模方法37-40
• 4.3.1 協(xié)議的建模及分析過程37-38
• 4.3.2 協(xié)議的建模步驟38-39
• 4.3.3 協(xié)議的不安全狀態(tài)的定義39-40
• 4.3.4 協(xié)議的攻擊的結(jié)果分析40
• 4.4 實例分析40-46
• 4.4.1 CMP1 協(xié)議40
• 4.4.2 帶有攻擊者的 CMP1 協(xié)議流程40-41
• 4.4.3 帶有攻擊者的 CMP1 協(xié)議的顏色 Petri 網(wǎng)模型41-44
• 4.4.4 帶有攻擊者的 CMP1 協(xié)議的顏色 Petri 網(wǎng)模型的分析44-46
• 4.5 本章小結(jié)46-47
• 第5章 實驗分析47-54
• 5.1 實驗工具47-49
• 5.1.1 CPN Tools 中的 ML 語法47-48
• 5.1.2 CPN Tools 中顏色 Petri 網(wǎng)的編輯及運行48-49
• 5.2 實驗驗證49-53
• 5.2.1 KZG 協(xié)議的驗證49-52
• 5.2.2 CMP1 協(xié)議的驗證52-53
• 5.3 本章小結(jié)53-54
• 結(jié)論54-55
• 參考文獻55-59
• 攻讀碩士學位期間承擔的科研任務與主要成果59-60
• 致謝60-61
• 作者簡介61

【參考文獻】

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

1 王志強;;著色Petri網(wǎng)應用研究[J];電腦與信息技術(shù);2010年05期

2 劉道斌,郭莉,白碩;基于Petri網(wǎng)的安全協(xié)議形式化分析[J];電子學報;2004年11期

3 劉文琦;顧宏;;基于分層時間有色Petri網(wǎng)的支付協(xié)議公平性分析[J];電子與信息學報;2009年06期

4 劉道斌,郭莉,白碩;一種新的安全協(xié)議驗證方法[J];計算機研究與發(fā)展;2003年10期

5 黎波濤,羅軍舟;不可否認協(xié)議的Petri網(wǎng)建模與分析[J];計算機研究與發(fā)展;2005年09期

6 劉雪艷;吳慧欣;張強;王彩芬;;基于面向?qū)ο髸r間Petri網(wǎng)的密碼協(xié)議分析[J];計算機工程;2009年13期

7 王劍;唐朝京;張權(quán);張森強;;基于Petri網(wǎng)的密碼協(xié)議分析[J];計算機工程與科學;2006年02期

8 龍士工,李祥;基于著色Petri網(wǎng)仿真模型的安全協(xié)議分析[J];計算機仿真;2005年06期

9 周典萃,卿斯?jié)h,周展飛;Kailar邏輯的缺陷[J];軟件學報;1999年12期

10 王貴林,卿斯?jié)h,周展飛;認證協(xié)議的一些新攻擊方法[J];軟件學報;2001年06期

  本文關鍵詞：顏色Petri網(wǎng)的電子商務協(xié)議形式化分析方法研究，由筆耕文化傳播整理發(fā)布。

本文編號：318596