特殊環(huán)境下的協(xié)議安全研究.pdf

1、隨著Internet技術(shù)的發(fā)展，安全協(xié)議在電子商務(wù)和電子政務(wù)中的應(yīng)用越來越多。與此相應(yīng)的就是人們對協(xié)議的安全性更加關(guān)注，尤其是在特殊環(huán)境下如何建模和分析安全協(xié)議顯得尤為重要。 本文首先研究和分析了現(xiàn)有的安全協(xié)議的建模和分析方法，找出其中的優(yōu)勢和不足?？紤]環(huán)境的特殊性，選用符合標(biāo)準(zhǔn)的基于事件的GSPML語言對廣義的挑戰(zhàn)-應(yīng)答協(xié)議和TLS握手協(xié)議的簡化版本建立了可視化的模型。 在此基礎(chǔ)上，本文對廣義的挑戰(zhàn)-應(yīng)答協(xié)議的安全條件

2、進(jìn)行了分析，列出了在對稱密碼體制和非對稱密碼體制下挑戰(zhàn)-應(yīng)答協(xié)議需要滿足的安全條件，以及不滿足這些條件將會導(dǎo)致的攻擊和與之相應(yīng)的協(xié)議認(rèn)證性的缺失。值得注意的是，在兩種密碼體制下挑戰(zhàn)-應(yīng)答協(xié)議在最小形式上是有所區(qū)別的。然后，作者對傳統(tǒng)認(rèn)為的三輪認(rèn)證協(xié)議進(jìn)行了分析，認(rèn)為在有主動攻擊者存在的情況下，單純的認(rèn)證協(xié)議無法完全保證認(rèn)證的目的。 此外，本文對四種形式化方法的自動工具進(jìn)行了分析，這些工具涵蓋了形式化分析方法的三大流派。作者主要從