版權(quán)說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請進(jìn)行舉報或認(rèn)領(lǐng)
文檔簡介
1、隨著電子商務(wù)的發(fā)展,認(rèn)證郵件協(xié)議作為一種能夠使協(xié)議的參與方都滿足公平性的郵件協(xié)議,越來越受到人們的關(guān)注。認(rèn)證郵件協(xié)議是公平交換協(xié)議的一種,它是指一個發(fā)送方需要將郵件的內(nèi)容與接收方收到郵件的證據(jù)進(jìn)行公平交換的協(xié)議。
本論文首先研究了Cerderquist等人提出的基于密鑰鏈的認(rèn)證郵件協(xié)議,該協(xié)議采用密鑰鏈來減少對可信第三方TTP(Trusted Third Party)的存儲要求,并滿足公平性、有效性和有限等待,但是并不能滿
2、足TTP透明性。TTP透明性是指任何人都無法判斷TTP是否參與過郵件協(xié)議的執(zhí)行過程,因此能保護(hù)TTP免于惡意曝光。鑒于TTP透明性在安全的認(rèn)證郵件協(xié)議中的重要性,本課題采用一種基于雙線性對的可驗(yàn)證加密簽名機(jī)制將該協(xié)議進(jìn)行擴(kuò)展,使其在滿足原有屬性的基礎(chǔ)上,能夠滿足可信第三方透明性。實(shí)驗(yàn)結(jié)果表明,擴(kuò)展后的協(xié)議是滿足屬性最多,并且最高效的認(rèn)證郵件協(xié)議之一。
為了驗(yàn)證上述擴(kuò)展協(xié)議的正確性,本課題采用了形式化驗(yàn)證方法對協(xié)議進(jìn)行屬性驗(yàn)
3、證。形式化驗(yàn)證是指能夠利用某一工具來自動的檢測某一系統(tǒng)的模型是否能夠滿足所需屬性的技術(shù)。該方法具有自動檢測功能,因此檢測比較全面,但是對系統(tǒng)建模和屬性描述的精確性及技巧性要求極高。在驗(yàn)證擴(kuò)展認(rèn)證郵件協(xié)議的過程中,本課題首先選用模型檢測工具M(jìn)ocha來完成對公平性、有效性和有限等待這三種屬性的形式化驗(yàn)證。Mocha允許的輸入?yún)f(xié)議模型使用守衛(wèi)命令語言來描述,需要檢驗(yàn)的屬性也均用轉(zhuǎn)換時態(tài)邏輯ATL來描述。利用Mocha所建立的協(xié)議模型具有博弈
4、屬性,其參與方被模擬成不同的玩家,并且協(xié)議的屬性也是用具有博弈性的語義邏輯來描述,因此,利用Mocha對認(rèn)證郵件協(xié)議進(jìn)行驗(yàn)證的過程就相當(dāng)于博弈論中對獲勝戰(zhàn)略的計算過程。該方法能比較好的驗(yàn)證郵件協(xié)議是否滿足公平性、有限等待和有效性。
此外,對于可信第三方的透明性驗(yàn)證,本文的主要思路采用一種代數(shù)形式的語言μCRL來為協(xié)議建模,并在CADP工具的支持下得到獲取證據(jù)的路徑蹤跡,然后進(jìn)行比較。通過對這些路徑蹤跡的比較,最終得到了對透
溫馨提示
- 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
- 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
- 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會有圖紙預(yù)覽,若沒有圖紙預(yù)覽就沒有圖紙。
- 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
- 5. 眾賞文庫僅提供信息存儲空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負(fù)責(zé)。
- 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請與我們聯(lián)系,我們立即糾正。
- 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時也不承擔(dān)用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。
最新文檔
- 口令認(rèn)證與密鑰協(xié)商協(xié)議及形式化驗(yàn)證研究.pdf
- 基于知識理論的安全協(xié)議形式化驗(yàn)證方法的應(yīng)用——驗(yàn)證對稱密鑰交換協(xié)議.pdf
- 安全協(xié)議形式化驗(yàn)證方法的研究.pdf
- 帶參協(xié)議形式化驗(yàn)證的研究.pdf
- 基于模型檢測的SET協(xié)議形式化驗(yàn)證與改進(jìn).pdf
- 安全協(xié)議的形式化驗(yàn)證技術(shù)研究.pdf
- 可信信道協(xié)議的設(shè)計與形式化驗(yàn)證.pdf
- 基于π演算的WSN路由協(xié)議形式化驗(yàn)證的方法研究.pdf
- 混合系統(tǒng)的形式化驗(yàn)證.pdf
- 非否認(rèn)協(xié)議的UC可靠的形式化驗(yàn)證.pdf
- IPv6鄰居發(fā)現(xiàn)協(xié)議的形式化驗(yàn)證.pdf
- 基于NuSMV的AUML模型形式化驗(yàn)證.pdf
- 802.11i中安全協(xié)議的形式化驗(yàn)證
- Statecharts及其時間擴(kuò)展的形式化驗(yàn)證技術(shù)研究.pdf
- 基于串空間模型的安全協(xié)議形式化驗(yàn)證方法的研究.pdf
- 模型檢測在安全協(xié)議形式化驗(yàn)證中的應(yīng)用
- ATS系統(tǒng)內(nèi)部通信協(xié)議的設(shè)計及形式化驗(yàn)證.pdf
- 基于Color Petri Nets的HMIPv6協(xié)議形式化驗(yàn)證研究.pdf
- 基于時間自動機(jī)的移動支付協(xié)議的形式化驗(yàn)證及實(shí)例.pdf
- 形式化驗(yàn)證安全協(xié)議Java代碼的安全性.pdf
評論
0/150
提交評論