一種復合協議驗證邏輯模型

摘要:針對協議復合時需要解決的問題，研究提出一種復合協議驗證邏輯模型，給出了協議描述、邏輯語法、邏輯語義和相應的證明系統，對協議的秘密性和認證性進行建模，將協議復合分為并行復合和順序復合，并提出相應的協議復合定理。最后以IKEv2協議為例進行分析，證明了IKEv2兩個分別安全的階段子協議復合后還是安全的。

關鍵詞:復合協議;形式化分析;邏輯模型;并行復合;順序復合;IKEv2協議

中圖分類號:TP309文獻標志碼:A

文章編號:10013695(2010)01027404

doi:10.3969/j.issn.10013695.2010.01.081