摘要:針對協議復合時需要解決的問題,研究提出一種復合協議驗證邏輯模型,給出了協議描述、邏輯語法、邏輯語義和相應的證明系統,對協議的秘密性和認證性進行建模,將協議復合分為并行復合和順序復合,并提出相應的協議復合定理。最后以IKEv2協議為例進行分析,證明了IKEv2兩個分別安全的階段子協議復合后還是安全的。
關鍵詞:復合協議;形式化分析;邏輯模型;并行復合;順序復合;IKEv2協議
中圖分類號:TP309文獻標志碼:A
文章編號:10013695(2010)01027404
doi:10.3969/j.issn.10013695.2010.01.081