《基於進程代數的複雜安全協定的形式化分析與驗證》是依託中國人民解放軍國防科技大學，由李舟軍擔任項目負責人的面上項目。
基本介紹
- 中文名：基於進程代數的複雜安全協定的形式化分析與驗證
- 項目類別：面上項目
- 項目負責人：李舟軍
- 依託單位：中國人民解放軍國防科技大學
- 負責人職稱：教授
- 批准號：60473057
- 研究期限：2005-01-01 至 2007-12-31
- 申請代碼：F0203
- 支持經費：23（萬元）
中文摘要
安全協定的缺陷是導致網路安全問題的重要原因之一.安全協定的形式化分析與驗證技術能全面深入地檢測安全協定中的細微漏洞,被實踐證明是一條確保協定正確性的重要途徑.複雜安全協定指被廣泛實用於Internet的大型安全協定,如Kerberos5協定、TLS協定、IPSec協定及電子商務協定等.本課題以複雜安全協定作為研究對象,以進程代數作為基本工具,研究適合於對複雜安全協定進行驗證的安全協定建模方法、安全性質的刻畫方法、安全協定的驗證方法及驗證的最佳化方法、基於構件的複雜安全協定的設計和分析方法,以及實現一個能夠對複雜安全協定進行自動分析和驗證的工具.本課題的研究有助於提高和保證包括電子商務在內的各種網上套用的安全性.
