1、隨著電子商務(wù)的飛速發(fā)展和廣泛應(yīng)用，網(wǎng)絡(luò)安全及其形式化分析引起社會的密切關(guān)注，逐步成為計算機科學研究的熱點領(lǐng)域。非否認技術(shù)作為網(wǎng)絡(luò)安全中最具價值的研究問題之一，在避免電子商務(wù)參與主體因事后否認所進行的交易行為，而給對方造成經(jīng)濟損失或推卸己方的責任方面發(fā)揮著重要的作用。非否認協(xié)議是非否認技術(shù)的一種具體實現(xiàn)，它通過協(xié)議設(shè)計使得協(xié)議主體無法否認其交易行為，即達成協(xié)議的非否認性。 本文在已有相關(guān)研究成果的基礎(chǔ)上，系統(tǒng)地研究了非否認協(xié)議的設(shè)

2、計和形式化分析。主要工作內(nèi)容和研究成果有： (1)給出了一種非否認協(xié)議的設(shè)計方法。該方法將非否認協(xié)議分成安全協(xié)議和密碼系統(tǒng)兩部分，在假設(shè)密碼系統(tǒng)是完善的基礎(chǔ)上，分別從認證保密性和非否認性兩部分對安全協(xié)議進行設(shè)計與分析。 (2)在認證保密性的設(shè)計和分析中，指出了A(0)協(xié)議存在的不能抵抗重放和偽冒攻擊的不足，在修改原協(xié)議的消息格式和增加握手確認消息的基礎(chǔ)上，提出了一種A(0)協(xié)議的改進方案，并應(yīng)用SVO邏輯對修改后的協(xié)議進

3、行了形式化分析，驗證了其滿足主體身份的認證性和臨時會話秘鑰的保密性。 (3)在非否認性的設(shè)計和分析中，對ZG協(xié)議及其改進協(xié)議進行了分析，指出了它們的缺陷與不足，提出了NZG協(xié)議，并對NZG協(xié)議的安全性和效率進行了分析。 (4)在SVO邏輯、Kailar邏輯和卿斯?jié)h的形式化分析方法的基礎(chǔ)上，進行了改進和擴充，提出了一種新的非否認協(xié)議形式化分析方法BSFA。新方法不僅能分析非否認協(xié)議的可追究性和公平性，還能對協(xié)議中的時限性問