樂觀太平交換協(xié)議形式化邏輯及其自動證明技術(shù).pdf

1、隨著Internet的日益發(fā)展與普及,電子信息交換已成為現(xiàn)代經(jīng)濟生活的主要形式之一,它是在任意兩個互不信任的主體之間以一種公平的方式來交換電子數(shù)據(jù)。實現(xiàn)公平電子信息交換的協(xié)議被稱為公平交換協(xié)議,公平性成為這類型協(xié)議的基本安全屬性,目標(biāo)是實現(xiàn)數(shù)據(jù)交換而又不會使一方比另一方有獲取更多信息的優(yōu)勢,促使互不信任的合作伙伴公平完成交換。
　　 公平交換協(xié)議是一類重要的安全協(xié)議,而其設(shè)計是一個眾所周知的難題,常常因為一些細微的問題產(chǎn)生安全缺

2、陷。目前已有一些分析公平交換協(xié)議的形式化方法,最典型和得到廣泛應(yīng)用的是信任邏輯方法。許多研究者采用擴展的信任邏輯方法成功分析了在線可信第三方公平交換協(xié)議的不可否認(rèn)性。由于信任邏輯方法自身固有的缺陷,難以用于分析樂觀型公平交換協(xié)議的公平性和時限性等性質(zhì)。
　　 樂觀型公平交換協(xié)議是目前公平交換協(xié)議研究領(lǐng)域的熱點之一,是一種兼顧公平和效率的公平交換協(xié)議形式。在樂觀型公平交換協(xié)議中,可信第三方不再直接參與數(shù)據(jù)交換,只需要扮演爭端解決者

3、的角色。交易過程中對可信第三方的請求次數(shù)遠遠低于其它類型的公平交換協(xié)議,避免了針對可信第三方的拒絕服務(wù)攻擊。但是,樂觀型公平交換協(xié)議引入了分支協(xié)議結(jié)構(gòu),協(xié)議執(zhí)行存在多種可能結(jié)果,使得對該類型協(xié)議的形式化分析更加復(fù)雜和困難。
　　 本文研究工作圍繞樂觀型公平交換協(xié)議及其形式化分析技術(shù)展開,主要包括三方面內(nèi)容:第一,對公平交換協(xié)議及其形式化技術(shù)進行研究綜述;第二,研究樂觀公平交換協(xié)議形式化模型、邏輯及其自動證明技術(shù);第三,研究樂觀公

4、平交換協(xié)議在電子商務(wù)中的應(yīng)用和實現(xiàn)技術(shù)。論文主要工作和創(chuàng)新性成果如下:
　　 1.對公平交換協(xié)議的基本理論和基本性質(zhì)進行綜述和分析,對其中一些重要性質(zhì)進行重新定義,如公平性等。
　　 2.對主要的公平交換協(xié)議形式化分析方法進行綜述性研究,討論各種方法的優(yōu)缺點及其存在的問題。
　　 3.提出一種新的樂觀公平交換協(xié)議形式化模型,將信道錯誤轉(zhuǎn)化為攻擊行為,將協(xié)議參與者分為誠實與不誠實兩類,將入侵者與不誠實參與者的共謀歸

5、結(jié)為兩類Dolev-Yao入侵者。新模型不再單獨考慮信道錯誤,簡化了問題空間。
　　 4.提出一種樂觀公平交換協(xié)議形式化邏輯。新邏輯采用信任邏輯的句法結(jié)構(gòu),定義樂觀公平交換協(xié)議為具有Kxipke語義結(jié)構(gòu)的演化系統(tǒng)。案例分析顯示,新邏輯被成功用于分析樂觀型公平交換協(xié)議的公平性和時限性。
　　 5.基于自動定理證明器Isabelle,研究實現(xiàn)本文模型和邏輯的自動定理證明技術(shù)。采用Paulson歸納法實現(xiàn)更為主動的攻擊者,將攻

6、擊者主動獲取知識的能力描述為對消息進行解析和組合的歸納函數(shù)。將信道假設(shè)對應(yīng)為不誠實參與者的行為,以降低協(xié)議模擬的復(fù)雜度。
　　 6.提出雙授權(quán)部分盲簽名概念,解決電子支付中銀行經(jīng)理濫用職權(quán)惡意簽發(fā)電子錢幣的問題。設(shè)計實現(xiàn)采用雙授權(quán)的部分盲簽名機制,在隨機預(yù)言機模型下證明新簽名機制是安全的。對比分析表明,新機制具有較高的計算性能。
　　 7.提出新的樂觀型電子支付協(xié)議。新協(xié)議采用雙授權(quán)部分盲簽名機制,同時實現(xiàn)電子現(xiàn)金離線支