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

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

【學位級別】：碩士

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


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

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

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



本文編號：3728104