基于SVO邏輯的電子商務(wù)協(xié)議形式化分析與研究.pdf

1、電子商務(wù)協(xié)議形式化分析是電子商務(wù)研究的一個(gè)重要方面，電子商務(wù)協(xié)議是面向電子商務(wù)的密碼協(xié)議，安全的電子商務(wù)協(xié)議是保證電子商務(wù)活動(dòng)正常開展的基礎(chǔ)。進(jìn)行電子商務(wù)協(xié)議的形式化分析研究具有重大理論意義和現(xiàn)實(shí)的應(yīng)用價(jià)值，是順利開展電子商務(wù)應(yīng)用的技術(shù)保障。 形式化的方法是分析安全協(xié)議的主要方法。目前己經(jīng)有很多研究安全協(xié)議的理論和方法，其中比較著名的有可證明安全理論、BAN類邏輯以及模型檢測和定理證明的方法等。 本文主要對基于邏輯的形式

2、化方法與模型檢測技術(shù)及其在電子商務(wù)協(xié)議形式化分析中的應(yīng)用進(jìn)行了系統(tǒng)研究，重點(diǎn)對SVO邏輯方法在電子商務(wù)協(xié)議時(shí)限性形式化分析中的應(yīng)用進(jìn)行了研究?？偟膩碚f，從理論到實(shí)踐兩個(gè)層面上研究了電子商務(wù)協(xié)議的形式化分析的相關(guān)技術(shù)。本文所做的工作、技術(shù)難點(diǎn)和創(chuàng)新之處如下： (1)首先從電子商務(wù)安全出發(fā)，對電子商務(wù)協(xié)議及其協(xié)議形式化分析的國內(nèi)外研究現(xiàn)狀進(jìn)行了綜述。 (2)研究了BAN邏輯和其相關(guān)形式化協(xié)議分析的方法、步驟，對BAN的公理規(guī)

3、則進(jìn)行了部分?jǐn)U展。同時(shí)對SVO邏輯進(jìn)行了部分?jǐn)U展，使該邏輯可以分析電子商務(wù)協(xié)議的時(shí)限性。 (3)對模型檢測工具SPIN進(jìn)行了詳細(xì)的介紹，通過研究Promela語言，發(fā)現(xiàn)該語言對時(shí)間段的模擬依然比較困難，但是通過編程技巧，可以模擬時(shí)間段的一些特性，從而模擬檢測協(xié)議的時(shí)間特性。 (4)利用公鑰密碼機(jī)制對Kerberos身份認(rèn)證協(xié)議進(jìn)行了改進(jìn)，并利用擴(kuò)展的BAN邏輯準(zhǔn)確地描述并證明了改進(jìn)后的Kerberos身份認(rèn)證協(xié)議的安全性