安全協議的形式化分析技術方法研究

付浩

摘要：安全協議是解決網絡安全問題最有效的手段之一。然而，由于互聯網的開放性和協議的并發性，安全協議的設計和分析一直是一個復雜而困難的問題。實踐證明，借助形式化的方法或工具分析安全協議是非常必要而且行之有效的。安全協議的形式化分析已有三十多年的歷史，一直存在兩類不同的方法：計算方法和符號方法。符號方法用形式化語言和符號推理對協議進行分析和驗證，更容易實現自動化分析。但是由于對密碼學原語和攻擊者能力的理想建模，使得這類分析方法的肯定性結論往往并不直接具有現實意義，被認為沒有真正建立起密碼學的可靠性。

關鍵詞：安全協議；符號方法；計算方法

隨著信息技術和網絡技術的飛速發展，互聯網的廣泛應用已成為社會進步和發展的重要標志之一。然而，由于網絡的開放性，它給人們的生活帶來極大方便的同時也帶來了許多安全隱患。安全協議是解決網絡安全問題最有效的手段之一，安全協議的正確實施對于保障網絡虛擬世界中各種組織和系統、各種商務和交易的安全運行起著十分關鍵的作用。安全協議”（也稱密碼協議）是建立在密碼體制基礎上的一種通信協議，它運行在計算機網絡或分布式系統中，借助于密碼算法為實現密鑰分配、身份認證、電子商務交易等任務的各方約定一系列執行步驟和執行規則。

由于安全協議中各消息之間存在著復雜的相互作用和制約關系，許多設計并投入實際應用的安全協議在運行時不一定能夠真正實現它所聲明的安全性質?！?br>