電子商務協(xié)議形式化方法及模型檢測技術的研究與應用.pdf

1、電子商務協(xié)議形式化分析是電子商務研究的一個重要方面，電子商務協(xié)議是面向電子商務的密碼協(xié)議，安全的電子商務協(xié)議是保證電子商務活動正常開展的基礎，其基本屬性包括安全性、保密性、完整性、可認證性、非否認性及公平性等。進行電子商務協(xié)議的形式化分析研究具有重大理論意義和現(xiàn)實的應用價值，是順利開展電子商務應用的技術保障。 目前國內(nèi)外對電子商務協(xié)議的分析驗證手段主要有以下幾種： (1)實際攻擊驗證方法； (2)從表面上進行直觀

2、檢測； (3)形式化邏輯分析方法。 前兩種方法存在較多缺點，如：屬于事后檢測，需在協(xié)議建立實施之后才能進行檢測、檢測手段不夠嚴密等。而形式化邏輯分析方法可以在協(xié)議實施之前就用嚴格可靠的方法對其進行分析驗證，是一個最有前途的研究方法。目前在各種電子商務協(xié)議形式化分析方法研究中，有影響的方法主要有BAN邏輯方法、Kailar邏輯方法、串空間方法、進程代數(shù)方法及基于時序邏輯的方法等。其中，時序邏輯方法能夠通過建立數(shù)學模型來描述

3、協(xié)議系統(tǒng)，可提供相應的模型檢測工具對協(xié)議性質進行自動驗證，對狀態(tài)空間有限的并發(fā)協(xié)議系統(tǒng)分析尤為成功，已成為對電子商務協(xié)議進行形式化分析的主要工具之一。 本文主要對基于邏輯的形式化方法與模型檢測技術及其在電子商務協(xié)議形式化分析中的應用進行了系統(tǒng)研究，重點對ATL邏輯方法及其在電子商務協(xié)議并形式化分析中的應用進行了研究?？偟膩碚f，從理論到實踐兩個層面上研究了電子商務協(xié)議的形式化分析的相關技術，其工作主要有以下幾個方面： 1.

4、對電子商務協(xié)議的基本理論和基本性質進行了分析和討論，包括：安全性、保密性、完整性、可認證性、非否認性、公平性、時效性等，并對其中一些重要性質做新的定義，提出電子商務協(xié)議設計的基本準則。 2.對當前流行的基于邏輯的電子商務協(xié)議形式化分析方法進行重點研究，包括BAN邏輯、Kailar邏輯及周—卿方法。采用這些較新的形式化分析方法對幾個典型協(xié)議進行分析，找出設計缺陷并提出新的公平非否認性協(xié)議。 結合Needham-Schroe

5、der與Otway-Rees兩個協(xié)議的優(yōu)點，提出了一個新的密鑰分配方案，克服了協(xié)議都是只有一個主體與認證服務器S有直接聯(lián)系的缺陷，減少了冗余。經(jīng)過用BAN邏輯對這個協(xié)議進行了形式化分析，找出了可能的攻擊方法并作出了相應修改。 分別研究借鑒NCP協(xié)議、CMP1協(xié)議，在此基礎上提出2種新的公平可追究協(xié)議NCP’、CMP1’。經(jīng)過使用改進的Kailor邏輯分析驗證，新的協(xié)議滿足可追究和公平性原則，且可以工作在不安全和不可靠的信道上。

6、 3.研究了電子商務協(xié)議的形式化建模方法：有限自動機、Petri網(wǎng)、Kripke結構等，分別對幾個典型電子商務協(xié)議進行分析建模。 4.提出利用模型檢測工具SMV分析驗證電子商務協(xié)議的安全性、公平性和可追究性等重要特性的基本框架，對幾個典型協(xié)議ISI、CMP1等進行了分析驗證。 建立了認證電子郵件協(xié)議CMP1和網(wǎng)絡支付協(xié)議ISI的有限狀態(tài)機模型，并用SMV檢驗工具對其兩個重要特性——非否認性與公平性進行了分析檢驗，發(fā)

7、現(xiàn)了兩個協(xié)議不滿足公平性并對其進行了相應修改。 5.研究基于博弈的ATL邏輯及其在電子商務協(xié)議形式化分析中的應用，進一步擴展了前人的方法使之在考慮公平性等特性的同時能夠分析協(xié)議的安全性。同時利用擴展的方法對幾個著名電子商務協(xié)議進行全面的形式化分析，找出了它們存在的問題并分析了其形成原因。 對Zhou-Gollmann協(xié)議(1999)進行分析，發(fā)現(xiàn)該協(xié)議存在不滿足保密性、公平性及適時終止性的缺陷；對ZDB協(xié)議(1999)進