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

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