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

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

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

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

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

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

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