非否認(rèn)協(xié)議設(shè)計(jì)與形式化分析的研究.pdf

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

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

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