一種新的形式化模型對安全認證協議的分析
2010-12-31 00:00:00胡曉輝曾雪娜姜浩
計算機應用研究 2010年12期
摘 要：針對形式化建模方法在進行網絡協議分析時遇到建立模型過程復雜、狀態空間龐大等問題，提出在Pe—tri網的基礎上，引入融合庫所建立一種新的形式化模型。利用該方法對Otway—Rees協議建立模型，并從可達性和仿真兩方面進行分析。實驗結果表明，該方法適合應用在協議分析中，不僅使協議建立模型更加簡便，而且在一定程度上縮小了其狀態空間。關鍵詞：形式化模型；Petri網；協議分析；融合庫所；狀態空間
