安全協(xié)議的形式化分析技術(shù)與方法的應(yīng)用研究.pdf

1、安全協(xié)議是用來保證電子商務(wù)等網(wǎng)絡(luò)通信安全的重要工具。形式化方法是當(dāng)今分析安全協(xié)議的一類主流方法，但是不同的形式化方法各有優(yōu)劣，且應(yīng)用形式化方法研究安全協(xié)議在理論和實踐上還不夠充分。 本文對BAN邏輯進(jìn)行了較為全面地介紹，并在此基礎(chǔ)上探討了將其應(yīng)用于協(xié)議認(rèn)證性形式化分析中的優(yōu)勢和具體方法。為分析Yahalom協(xié)議認(rèn)證性，論文給出了Yahalom協(xié)議基于SVO邏輯的模型，并通過詳細(xì)的推理分析了Yahalom協(xié)議的認(rèn)證性質(zhì)。為了進(jìn)一步

2、分析協(xié)議的機(jī)密性等性質(zhì)并對協(xié)議本身進(jìn)行更深入研究，論文引入串空間理論，接著對其中的叢理論、攻擊者行為定義、“理想”和“誠實”等概念作了深入剖析。然后，利用串空間方法建立BAN-Yahalom協(xié)議的形式化模型，并全面分析了其安全性質(zhì)，證明了其中的安全缺陷并找出其原因，隨后提出了積極的修改方案并對協(xié)議進(jìn)行修改。為使對安全協(xié)議的分析能逐漸自動化，論文詳細(xì)介紹了使用模型自動校驗器Spin的基本方法，以及Promela語言的關(guān)鍵技術(shù)。以NSPK協(xié)