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

1、隨著計算機網(wǎng)絡(luò)和電子商務(wù)的普及，網(wǎng)絡(luò)安全問題越來越受到重視，而電子商務(wù)協(xié)議就是解決電子商務(wù)中網(wǎng)絡(luò)安全問題的有效手段之一。雖然電子商務(wù)協(xié)議使用密碼系統(tǒng)來確保其安全性，但是，它們中的漏洞很多時候是由于其設(shè)計中可能的邏輯錯誤所導(dǎo)致的，而不是由于其加密算法不可靠。所以使用邏輯推理的方法來分析電子商務(wù)協(xié)議變得十分重要，而且是研究的熱點。 本文的理論基礎(chǔ)來源于國家自然科學(xué)基金項目(認識邏輯及其在安全協(xié)議設(shè)計、驗證中的應(yīng)用，項目編號：6007

2、3056)所提出的SPV邏輯(Security Protocol Verifier Logic)。這是一種基于邏輯推理，而且高效的驗證邏輯，并且有相應(yīng)的自動驗證工具SPV。 本文首先使用SPV邏輯分析了一類重要的電子商務(wù)協(xié)議——SET支付協(xié)議及其簡化版本Lu-Smolka協(xié)議，指出了其存在漏洞的原因一是沒有對訂購信息OI和支付指令PI進行雙重數(shù)字簽名用以證明消息沒有被篡改，二是沒有對交易的各方進行通信主體的身份認證。然后在此結(jié)果

3、上改進了Lu-Smolka協(xié)議，使用SPV邏輯分析后得出改進的協(xié)議比原協(xié)議滿足更多的安全性質(zhì)。 本文接著從另一個角度對電子商務(wù)協(xié)議的核心基礎(chǔ)協(xié)議：公平非否認性協(xié)議展開研究。在驗證和分析了已有的幾個不同類型的公平非否認性協(xié)議之后，設(shè)計了一個新的基offline TTP的公平非否認性協(xié)議(Fair Non-Repudiation Protocols with Offiine Trusted Third Party)——FNR協(xié)議，然