樂觀公平交換協(xié)議的形式化分析技術(shù)研究.pdf

1、樂觀公平交換協(xié)議是一類典型的安全協(xié)議,用于在兩個(gè)或多個(gè)主體之間安全、高效地進(jìn)行電子交易。與其它安全協(xié)議相比,樂觀公平交換協(xié)議在結(jié)構(gòu)上較為復(fù)雜,從而更容易存在安全缺陷,同時(shí)也為其形式化分析帶來了挑戰(zhàn)。
　　本文主要研究了樂觀公平交換協(xié)議的形式化分析技術(shù),所取得的主要研究結(jié)果有:
　　(1)深入剖析了IETF(Internet Engineering Task Force)的IPSEC工作組提交的IKEv2協(xié)議草案;在對協(xié)議進(jìn)行

2、形式建模,以及應(yīng)用CTL對相應(yīng)的安全性質(zhì)進(jìn)行形式描述的基礎(chǔ)上,借助SMV分析了協(xié)議的認(rèn)證性、秘密性、和完整性,發(fā)現(xiàn)了兩個(gè)攻擊;對這兩個(gè)攻擊所產(chǎn)生的影響進(jìn)行了討論。
　　(2)針對樂觀公平交換協(xié)議,提出了一種基于有限狀態(tài)機(jī)的分析模型;應(yīng)用該模型,借助SMV分析了GJM電子合同簽訂協(xié)議,檢測出由V.Shmatikov首先發(fā)現(xiàn)的缺陷;分析了ASW電子合同簽訂協(xié)議,指出在協(xié)議實(shí)現(xiàn)過程中應(yīng)該注意的問題;分析了FPH掛號電子郵件協(xié)議,發(fā)現(xiàn)該協(xié)