電子商務(wù)協(xié)議形式化分析是電子商務(wù)研究的一個重要方面，電子商務(wù)協(xié)議是面向電子商務(wù)的密碼協(xié)議，安全的電子商務(wù)協(xié)議是保證電子商務(wù)活動正常開展的基礎(chǔ)。進(jìn)行電子商務(wù)協(xié)議的形式化分析研究具有重大理論意義和現(xiàn)實的應(yīng)用價值，是順利開展電子商務(wù)應(yīng)用的技術(shù)保障。 形式化的方法是分析安全協(xié)議的主要方法。目前已經(jīng)有很多研究安全協(xié)議的理論和方法，其中比較著名的有可證明安全理論、BAN類邏輯以及模型檢測和定理證明的方法等。 本文主要對基于邏輯的形式化方法與模型檢測技術(shù)及其在電子商務(wù)協(xié)議形式化分析中的應(yīng)用進(jìn)行了系統(tǒng)研究，重點對SVO邏輯方法在電子商務(wù)協(xié)議時限性形式化分析中的應(yīng)用進(jìn)行了研究�？偟膩碚f，從理論到實踐兩個層面上研究了電子商務(wù)協(xié)議的形式化分析的相關(guān)技術(shù)。本文所做的工作、技術(shù)難點和創(chuàng)新之處如下： （1）首先從電子商務(wù)安全出發(fā)，對電子商務(wù)協(xié)議及其協(xié)議形式化分析的國內(nèi)外研究現(xiàn)狀進(jìn)行了綜述。 （2）研究了BAN邏輯和其相關(guān)形式化協(xié)議分析的方法、步驟，對BAN的公理規(guī)則進(jìn)行了部分?jǐn)U展。同時對SVO邏輯進(jìn)行了部分?jǐn)U展，使該邏輯可以分... 

【文章頁數(shù)】：70 頁

【學(xué)位級別】：碩士

【文章目錄】：
目錄
摘要
Abstract
1 緒論
    1.1 研究背景及意義
    1.2 國內(nèi)外研究現(xiàn)狀
        1.2.1 電子商務(wù)協(xié)議及其發(fā)展現(xiàn)狀
        1.2.2 安全協(xié)議形式化分析研究現(xiàn)狀
    1.3 主要研究內(nèi)容
    1.4 本文的組織結(jié)構(gòu)
2 基于邏輯的電子商務(wù)協(xié)議分析方法
    2.1 BAN邏輯
        2.1.1 BAN邏輯概念
        2.1.2 推理規(guī)則
        2.1.3 BAN邏輯的優(yōu)缺點
        2.1.4 BAN邏輯的應(yīng)用
        2.1.5 BAN邏輯的擴(kuò)展
    2.2 SVO邏輯
        2.2.1 SVO邏輯概念
        2.2.2 推理規(guī)則
        2.2.3 SVO邏輯分析步驟
        2.2.4 SVO邏輯的語義
        2.2.5 SVO邏輯優(yōu)缺點
        2.2.6 SVO邏輯的改進(jìn)
3 模型檢測及模型檢測工具SPIN
    3.1 模型檢測
        3.1.1 模型檢測的過程
        3.1.2 線性時態(tài)邏輯(LTL)
    3.2 SPIN概述
        3.2.1 SPIN的基本結(jié)構(gòu)
        3.2.2 SPIN的特征
    3.3 SPIN建模語言Promela
        3.3.1 簡介
        3.3.2 語句的可執(zhí)行性
        3.3.3 Promela變量和數(shù)據(jù)類型
        3.3.4 進(jìn)程
        3.3.5 消息傳遞
        3.3.6 控制流
        3.3.7 語句類型
        3.3.8 高級操作
    3.4 SPIN的使用
        3.4.1 SPIN的運行時參數(shù)
        3.4.2 pan運行時參數(shù)和編譯時參數(shù)
4 基于公鑰的Kerberos協(xié)議改進(jìn)和證明
    4.1 Kerberos認(rèn)證協(xié)議概述
        4.1.1 工作原理
        4.1.2 Kerberos協(xié)議的局限性
        4.1.3 Kerberos協(xié)議的改進(jìn)方案
    4.2 用擴(kuò)展BAN邏輯證明改進(jìn)的Kerberos認(rèn)證協(xié)議
        4.2.1 協(xié)議理想化
        4.2.2 證明目標(biāo)
        4.2.3 證明步驟
    4.3 改進(jìn)后的特性
5 基于NZG、ISI的電子貨幣支付協(xié)議證明
    5.1 協(xié)議概述
        5.1.1 NZG不可否認(rèn)協(xié)議及其缺陷
        5.1.2 ISI電子支付協(xié)議及其缺陷
        5.1.3 改進(jìn)后的電子貨幣支付協(xié)議
    5.2 使用擴(kuò)展后的SVO邏輯對新協(xié)議進(jìn)行驗證
        5.2.1 協(xié)議初始化
        5.2.2 協(xié)議目標(biāo)
        5.2.3 協(xié)議證明
    5.3 使用SPIN對新協(xié)議進(jìn)行模型檢測
        5.3.1 協(xié)議行為抽象
        5.3.2 協(xié)議的Promela結(jié)構(gòu)
        5.3.3 協(xié)議主體的狀態(tài)及行為描述
        5.3.4 屬性結(jié)果驗證分析
6 結(jié)論與展望
致謝
主要參考文獻(xiàn)
附錄


【參考文獻(xiàn)】：
期刊論文
[1]一個非否認(rèn)協(xié)議ZG的形式化分析[J]. 范紅,馮登國.  電子學(xué)報. 2005(01)
[2]安全協(xié)議20年研究進(jìn)展[J]. 卿斯?jié)h.  軟件學(xué)報. 2003(10)
[3]Kerberos身份認(rèn)證協(xié)議分析及改進(jìn)[J]. 張紅旗,車天偉,李娜.  計算機(jī)應(yīng)用. 2002(12)

博士論文
[1]電子商務(wù)協(xié)議形式化方法及模型檢測技術(shù)的研究與應(yīng)用[D]. 文靜華.貴州大學(xué) 2006

碩士論文
[1]SPIN模型檢測的研究與應(yīng)用[D]. 王巧麗.貴州大學(xué) 2006
[2]網(wǎng)絡(luò)安全協(xié)議的形式化描述與驗證[D]. 代新敏.重慶大學(xué) 2004
[3]安全協(xié)議形式化驗證方法和安全協(xié)議設(shè)計研究[D]. 侯峻峰.清華大學(xué) 2004
[4]安全協(xié)議形式化分析及其應(yīng)用[D]. 劉學(xué)鋒.湘潭大學(xué) 2004
[5]形式化邏輯方法在分析認(rèn)證協(xié)議以及電子商務(wù)協(xié)議中的應(yīng)用[D]. 何加亮.吉林大學(xué) 2004
[6]基于邏輯的電子商務(wù)協(xié)議屬性的分析與研究[D]. 邊培泉.蘭州理工大學(xué) 2004



本文編號：3728104